Debuggers, Static Debuggers, and Algebraic Steppers 
Author Message
 Debuggers, Static Debuggers, and Algebraic Steppers

Quote:



> > > Point #2 makes sense for dynamically-typed languages such as Scheme.
> > > However, it doesn't make as much sense for a manifestly-typed language
> > > such as SML, because the compiler itself does the job.

> > Oh yes? It's news to me that  the SML  compiler  solved the
> > halting problem. Great. Congratulations.  I always knew these
> > SML guys were up to good stuff.

> When I peel away the sarcasm, it seems that what you're saying is that

Excuse the sarcasm please.

De{*filter*}: inspect some representation of machine state during program execution

I believe that if you write functional programs,  you probably  don't need a
de{*filter*}.
If you use the How to Design Programs principles, this is true for Scheme. It's
certainly
true for SML.

If you write highly imperative code in a mostly functional language,  you do
need
some form of de{*filter*} because the reasoning becomes highly temp{*filter*}and if
anything, experience with C and even mostly safe imperative languages has shown
that people aren't all that good about that. (It's intuitive at first but
complex for anything
but toy programs). If you then add  event-based or concurrent programming to the

mix, you are even more in need of tools for inspecting intermediate states.

                                ---------------

Static De{*filter*}:  analyze the program text *and* present analysis results in an
interactive
 fashion to the programmer.

Why is it needed? Even in a safe language,  programs may raise exceptions due to
invariant
violations by program operations (application, if, primitives, etc).  If we have
tools that analyze
programs for all possible safety violations, and present their reasoning to the
programmers,
we can eliminate many of those potential safety violations. That woudl begreat
because it
makes *programs* and not just the *programming language* safe.

Since the goal of this phase is to discover potential bugs and to eliminate them
or to program
so that we can  analyze them away, the terminology "static de{*filter*}" is more
than appropriate.

One could think of SML's type system as a primitive static de{*filter*}. Its
obnoxious error messages
and lack of explanatory capabilities though, make it an extremely ugly and
stupid static de{*filter*}.

A good static de{*filter*} can explain its reasoning.  MrSpidey for example, can
draw a data flow
graph over a Scheme program and can explain why a particular expression
(argument) may
produce values that are inappriopriate for  the program operation.

One could also argue that every analysis is a type system. But that's as
fruitless as arguing that
all languages are equally powerful computing media. I haven't seen any insight
from this research
direction.

                               ---------------

Algebraic Stepper: use the laws of algebra (and my dissertation) to explain how
programs are
 executed by rewriting programs and never using any machine-based notion to
explain intermediate
 states.

Based on pretty substantial teaching experience,  I believe that an algebraic
de{*filter*}/stepper
is a highly useful tool for teaching how programs are executed. It relieves us
of the machine
oriented explanations and is accessible to anyone with 8th grade algebra. It
also appeals to
a much broader audience than "now shove this byte into this register"
explanations.
I would never use a regular de{*filter*} for teaching purposes.

-- Matthias



Sun, 03 Nov 2002 03:00:00 GMT  
 Debuggers, Static Debuggers, and Algebraic Steppers

Matthias> One could think of SML's type system as a primitive static
Matthias> de{*filter*}. Its obnoxious error messages and lack of
Matthias> explanatory capabilities though, make it an extremely ugly
Matthias> and stupid static de{*filter*}.

Especially as I tend to use SML's "static de{*filter*}" to deal with
*exactly* the same kinds of problems I use dynamic de{*filter*}s in Scheme
for.  

The only pragmatic difference for me is that SML's static de{*filter*}
often does not give me the slightest cue about where the problem
actually is.  In a dynamic de{*filter*}, I usually find the error really,
really fast because I have control over what it tells me.  (I'm sorry
to say that MrSpidey mostly does not agree with my programming style,
so it doesn't solve my problem.)

Therefore, the notion that SML programming obviates debugging
seems totally ridiculous to me: I merely do the debugging during a
different phase in programming development.  It's not clear to me why
it's obvious that doing it in one phase is preferable to doing it in
another phase.

--
Cheers =8-} Mike
Friede, V?lkerverst?ndigung und berhaupt blabla



Sun, 03 Nov 2002 03:00:00 GMT  
 Debuggers, Static Debuggers, and Algebraic Steppers

Let me bring up my own pet peeve and complain about the terminology being
used.  The term "de{*filter*}" whether it's static or dynamic is
misleading. Neither de{*filter*} "removes bugs" only the programmer can remove
bugs. Both these tools are "program understanding aids". Dynamic "de{*filter*}s"
are program state inspectors/manipulators. Static de{*filter*}s are literally
"program theorem provers."

Both are useful tools to help the programmer understand the program so that
the programmer can remove the bugs. My particular peeve about naming, I
think actually suggests an unexploited synergy between the dynamic and
static debugging tools. I'd like to see "program state inspectors" that help
me understand *how* my program is misbehaving by letting me observer it.
Once I understand *how* my program is misbehaving, I'd like a tool to help
me figure out *why*.

Here's an example of what I mean. Once I get an unhandled exception error,
I'd like enough dynamic "state inspection support" to what exception got
raised. I'd like a program theorem prover to tell me all parts of the
program could have raised the exception and under what conditions. Then
hopefully, I can stare at this code figure out where things went wrong and
fix all the code that I think is broken and then ask the theorem prover if
that exception is still unhandled.

I actually, don't know of a system that does something like this
currently. It be really cool. If someone built a completely general systems
that let me both observer non-trivial properties about my program, and prove
non-trivial/useful theorems that are perhaps a bit more expressive then
simple type safety.

This sort of *how* and *why* approach, has some potential benefits. Current
static techniques try to prove non-trivial theorems about entire
programs. If you're just trying to get rid of a particular bug you many not
need to examine the entire program. One could easily also play a game where
my static theorem prover does useful, like figure a minimal set of
preconditions that must hold for a particular property to be true,
automatically insert assertion checking code in my program run the program
for me until it fails at some assertion and then ask me what I want to do
next.



Sun, 03 Nov 2002 03:00:00 GMT  
 Debuggers, Static Debuggers, and Algebraic Steppers

Quote:

> Matthias> One could think of SML's type system as a primitive static
> Matthias> de{*filter*}. Its obnoxious error messages and lack of
> Matthias> explanatory capabilities though, make it an extremely ugly
> Matthias> and stupid static de{*filter*}.
> MrSpidey mostly does not agree with my programming style,
> so it doesn't solve my problem.)

MrSpidey was a prototype and I know that it disagrees with some
coding styles. I also know your coding style. (Perhaps you should
translate those funny German words into English, MrSpidey would
do a better  job :-) MrSpidey also didn't keep up enough with
MzScheme's development.

There are other static de{*filter*}s. The ESC project at DEC SRC started
around the same time. It requires more interaction (in the form of assertions)
but for that it is better on independent units of code.

Quote:
> Therefore, the notion that SML programming obviates debugging
> seems totally ridiculous to me: I merely do the debugging during a
> different phase in programming development.  It's not clear to me why
> it's obvious that doing it in one phase is preferable to doing it in
> another phase.

Here is why. Suppose your program is a function  from

  S-expression -> int

If you run a bunch of dynamic tests and you debug them, you know
that your program works on those tests. Period. You have no other
guarantees.

In contrast, if you run a static de{*filter*} or even a poor type system,
you get  the following guarantee

  FOR ALL s in S-expression. the function produces an int
  without mishandling any data.

  assuming the underlying language is safe.

Well the second part is not quite true. You might get a small
number of  exceptions but  a good static de{*filter*} will flag those.
MrSpidey does, the SML type system doesn't. (It assumes you
do this job yourself.)

So you get quite a bit more. But you still have to do some dynamic
debugging because you might just get the wrong int.

Many Schemers choose good tests and discover the type erros
at the same time as they discover dynamic errors.  But weak minds
also program with Scheme, and they don't get the  FOR ALL
guarantee.

;; ---

Of course, in a typed but  unsafe language such as C o C++
you  may see an int but it really is just some header tag of a
struct.  Typed and unsafe is the most insidious combintation of
qualities I have encountered.

-- Matthias



Sun, 03 Nov 2002 03:00:00 GMT  
 Debuggers, Static Debuggers, and Algebraic Steppers

Quote:

> Especially as I tend to use SML's "static de{*filter*}" to deal with
> *exactly* the same kinds of problems I use dynamic de{*filter*}s in Scheme
> for.  

> The only pragmatic difference for me is that SML's static de{*filter*}
> often does not give me the slightest cue about where the problem
> actually is.  In a dynamic de{*filter*}, I usually find the error really,
> really fast because I have control over what it tells me.  (I'm sorry
> to say that MrSpidey mostly does not agree with my programming style,
> so it doesn't solve my problem.)

This is one of the two fundamental problems that some of us have
always had with ML-type type systems (*).

The error messages that I've seen from SML are so unreadable, that
they are useless, and would leave me very few techniques to resolve
them.  I'd rather read unformatted TECO, and have.

I'll take a runtime error any day -- it is a signal that the system
has materialized an instance of the problematic data/situation for me
to inspect and increase my understanding.

Machine cycles are cheap and abundant.  A great way to use them is to
help me along in my thinking by generating counter-examples to my
current mental state (which is an assertion of its own).

Yes, this methodology does not prove that you have a correct answer.
But neither does merely thinking that you have a correct answer, no
matter how meticulous, careful, and thorough you may be in your
reasoning.

Neither obviates the other.

Quote:
> Therefore, the notion that SML programming obviates debugging
> seems totally ridiculous to me: I merely do the debugging during a
> different phase in programming development.  It's not clear to me why
> it's obvious that doing it in one phase is preferable to doing it in
> another phase.

As I said earlier, we can argue this 'til the end of time because it
is a matter of taste and not science or engineering.

There is a continuum and few people at either extreme, but two bumps
near the extremes.

Quote:

> --
> Cheers =8-} Mike
> Friede, V?lkerverst?ndigung und berhaupt blabla

(*) The other is that they add artificial constraints into your
programs.  You end up programming to bypass the type system and have
to take it into account when thinking about a problem -- something
that I'd rather avoid as being unnecessary.  Good computer languages
should free me from artificial constraints, and not add more for me to
have to manage.


Mon, 04 Nov 2002 03:00:00 GMT  
 Debuggers, Static Debuggers, and Algebraic Steppers

Quote:

> Here is why. Suppose your program is a function  from

>   S-expression -> int

> If you run a bunch of dynamic tests and you debug them, you know
> that your program works on those tests. Period. You have no other
> guarantees.

Ah, this is not true.  You can analyze your program and come up with
test vectors such that working on all of them guarantees (with very
high confidence, which is what we are talking about) that you will
work on any input.  Viewed another way, each test vector (particular
input) guarantees a neighborhood/dimension around itself.  The
neighborhood/dimension may be small if you are careless in choosing
your vector, but can be large.  If you understand the
neighborhood/dimension, and design your test vectors with
exhaustively-covering neighborhood/dimensions, you can get a lot of
mileage out of a finite (and rather small) set of test vectors.  Funny
that they are called vectors -- you are looking for a basis (although
it need not be a minimal, but it is desirable).

Hardware designers don't test 64-bit ALUs or other structures by
running all 64-bit inputs across all 64-bit inputs.  Believe me, they
have good formal evidence that their logic is correct, but they also
generate careful test vectors that give them very high confidence that
they work.  The test vectors tend to be small in number because time
on a tester is precious.  They know what they are doing.

Good verification work is no easier than good programming work, but it
is doable, and often the only solution because static tools are
unavailable or break down due to complexity.

Quote:

> In contrast, if you run a static de{*filter*} or even a poor type system,
> you get  the following guarantee

>   FOR ALL s in S-expression. the function produces an int
>   without mishandling any data.

>   assuming the underlying language is safe.

> Well the second part is not quite true. You might get a small
> number of  exceptions but  a good static de{*filter*} will flag those.
> MrSpidey does, the SML type system doesn't. (It assumes you
> do this job yourself.)

> So you get quite a bit more. But you still have to do some dynamic
> debugging because you might just get the wrong int.

Right.  For me, the latter is the real issue.  The typing stuff is
just trivia, but I agree that other people need different crutches
from the ones that I need.  Unfortunately, if they are built into the
language, someone is forcing me to use their crutches (and I still
need my own), so they end up slowing me down.

Of course, you and I agree on this issue.

- Show quoted text -

Quote:

> Many Schemers choose good tests and discover the type erros
> at the same time as they discover dynamic errors.  But weak minds
> also program with Scheme, and they don't get the  FOR ALL
> guarantee.

> ;; ---

> Of course, in a typed but  unsafe language such as C o C++
> you  may see an int but it really is just some header tag of a
> struct.  Typed and unsafe is the most insidious combintation of
> qualities I have encountered.

> -- Matthias



Mon, 04 Nov 2002 03:00:00 GMT  
 Debuggers, Static Debuggers, and Algebraic Steppers

Hi there, long time no see ...

(1) Please see  my original message.  Did you see the forall quantifier for
       the static de{*filter*}?

Quote:

> (*) The other is that they add artificial constraints into your
> programs.  You end up programming to bypass the type system and have
> to take it into account when thinking about a problem -- something
> that I'd rather avoid as being unnecessary.  Good computer languages
> should free me from artificial constraints, and not add more for me to
> have to manage.

(2) That's why you want a static de{*filter*} not a type system, though
       you should be able to express constraints via comments

-- Matthias



Mon, 04 Nov 2002 03:00:00 GMT  
 Debuggers, Static Debuggers, and Algebraic Steppers

Quote:

> On error messages from SML vs MrSpidey --

> I just wrote a program (for How to Design Programs) and changed one
> of the functions a bit (returning the graph rather than void now).
> The test suite signaled an error, so I ran MrSpidey ... and I got
> the wonderful picture that I attach.

> At Shriram's suggestion, I wrote it up in SML and got the following error
> message. You be the judge.

> -- Matthias

The SML version has two bugs, while the Scheme version only has one.
Thus the comparison is inherently somewhat skewed.

However, I can provide further anecdotal evidence about the usefulness
of SML/NJ's error messages: I had overlooked the second bug in the SML
version when skimming over it, but SML/NJ's error message called my
attention to it.

I assume you wouldn't try intentionally skewing the evidence by
inserting a second bug in the SML version.  So I have to conclude it
happened by accident.  The interesting question then is, why didn't
you too notice it based on SML/NJ's error message?  The error message
is slightly cryptic, I'll agree(*), but I think it would have sufficed
to point a smart man like you at the problem, had you read it and
thought about it even a little.  So I find myself wondering how much
attention you gave to these SML error messages that you compare to
your "wonderful picture"?

 -max

(*) On the other hand, the "slightly cryptic" nature of the error
message you overlooked is the result of trivial engineering details in
SML/NJ, not the overall H./M. type inference algorithm.  SML/NJ echoed
the offending expression other than verbatim as it appeared in your
source code (with the redundant parentheses removed) and gave a
over-broad range of source code positions.  These same trivial
engineering issues also affect the more difficult error message coming
from the type class of returning void in one case and a list in
another.  Had SML/NJ echoed the source code "if" expression back out
to you as an "if", rather than as a "case" with two rules (the second
having "false" as its pattern), the type clash wouldn't have been
cryptic either.



Tue, 05 Nov 2002 03:00:00 GMT  
 Debuggers, Static Debuggers, and Algebraic Steppers

Quote:

> The SML version has two bugs, while the Scheme version only has one.
> Thus the comparison is inherently somewhat skewed.
> So I find myself wondering how much
> attention you gave to these SML error messages that you compare to
> your "wonderful picture"?

>  -max

> (*) On the other hand, the "slightly cryptic" nature of the error
> message you overlooked is the result of trivial engineering details in
> SML/NJ, not the overall H./M. type inference algorithm.  SML/NJ echoed
> the offending expression other than verbatim as it appeared in your
> source code (with the redundant parentheses removed) and gave a
> over-broad range of source code positions.  These same trivial
> engineering issues also affect the more difficult error message coming
> from the type class of returning void in one case and a list in
> another.  Had SML/NJ echoed the source code "if" expression back out
> to you as an "if", rather than as a "case" with two rules (the second
> having "false" as its pattern), the type clash wouldn't have been
> cryptic either.

With due apologies, let me re-send the proper error message:

     /home/matthias/reachable.sml:7.9-10.23 Error: types of rules don't
     agree [tycon mismatch]
       earlier rule(s): bool -> unit
       this rule: bool -> 'Z list
       in rule:
         false => (foo := true; reachable next)
     /home/matthias/reachable.sml:5.9-10.23 Error: right-hand-side of
     clause doesn't
     agree with function result type [tycon mismatch]
       expression:  unit
       result type:  'Z list
       in declaration:
         reachable =
           (fn end_node => graph
             | a_node (<pat>,<pat>,<pat>) =>
                 (case (! <exp>)
                   of <pat> => <exp>

               | <pat> => <exp>))

And yes, I am perfectly aware that this error message is presented in terms of
the
elaborated SML tree rather than the source.

Do you think we didn't face the same obstacle? What do you think the elaborate
source of MzScheme looks like? You know perfectly well from working with our
system that even define's and lambda's are elaboated into quite different forms.

Do you think we have had the manpower of the SML of NJ team working on
MzScheme? We started in 1996.  MrSpidey is a two or three year prototype?
SML is a 15 year product of who-knows-how-many people?

Perhaps macro-elaboration is relevant to ML, too, though of course not in the
obvious manner.

What's the real difference? We explored H-M as the basis of a theorem prover
and eventually decided it didn't provide the feedback that a user needed. Why?
Because inference engines based on equallities let information flow in all kinds

of directions, in an uncontrolled manner.  They also work badly with some
natural Scheme programming styles.

Then  we started a third dissertation and explored inequations (Heintze's SBA)
as the basis of static debugging. Inequations naturally lead to graphs people
can understand. The path-to-source option didn't just produce the result

  "mismatch between two branches"

but it pinpointed the exact source expression from where the ill-typed value
flows (and how it flows into the map operation).

-- Matthias



Tue, 05 Nov 2002 03:00:00 GMT  
 Debuggers, Static Debuggers, and Algebraic Steppers

Quote:

> Suppose your program is a function  from

>   S-expression -> int

Unfortunately, very few of my programs have such simple constraints.
Most are along the lines of

<set of objects that satisfy some unspecified predicate> ->
   <different set of objects that satisfy some other unspecified predicate>

Where the predicate is unspecified because of one of three reasons:

   1.  The type system in not sufficiently powerful enough to express
       it.

   2.  The predicate is statically undecideable.

   3.  The predicate is not easy to formally express.



Tue, 05 Nov 2002 03:00:00 GMT  
 Debuggers, Static Debuggers, and Algebraic Steppers

{stuff deleted}

Quote:
> Do you think we have had the manpower of the SML of NJ team working on
> MzScheme? We started in 1996.  MrSpidey is a two or three year prototype?
> SML is a 15 year product of who-knows-how-many people?

SML/NJ has been a research vehicle for *compilation technology*. Little
effort (unfortunately) has been spent on the frontend and UI related
issues. So I think this is an unfair comparison. I personally would love to
see some of the ideas of MrSpidey applied to something like ML.


Tue, 05 Nov 2002 03:00:00 GMT  
 Debuggers, Static Debuggers, and Algebraic Steppers

Quote:

> And yes, I am perfectly aware that this error message is presented
> in terms of the elaborated SML tree rather than the source.

> Do you think we didn't face the same obstacle? ...

Of course you faced the same obstacle.  And you solved it, and the
SML/NJ team didn't.  They were busy solving other problems.  But I
really don't care in any case whether they didn't solve it because
they were otherwise busy or because they were incompetent (not that
they were).  That isn't relevant.  What is relevant is that they
*could* have solved it without abandoning the basic type-checking
mechanism.  It is orthogonal.  Therefore, it should be discounted if
one is comparing the underlying typing mechanisms.

Quote:
> Do you think we have had the manpower of the SML of NJ team working on
> MzScheme? We started in 1996.  MrSpidey is a two or three year prototype?
> SML is a 15 year product of who-knows-how-many people?

Again, I don't see this as relevant, other than to the personality you
project to other members of this newsgroup, and hence how credible
they are likely to find your technical arguments.

Quote:
> What's the real difference? We explored H-M ...
>  and explored inequations ...Inequations naturally lead to graphs people
> can understand. ...

Now we are finally getting to the relevant part.  And the answer I
have is simple: this may well be true, but you picked a bad example to
illustrate it with.  Aside from the superficial presentation, the
SML/NJ type-checker localized the error as well or better than
MrSpidey.  (Better, because SML typing rules don't allow a procedure
to sometimes return void and sometimes a list, independent of the
procedure's call sites, whereas in Scheme the union type is fine from
the perspective of the procedure and only an error in the context of
the call site.)  If you want to show equational type inference
propagating information all over the place and producing a clash far
from the actual error, you are going to have to use a different
example. -max


Tue, 05 Nov 2002 03:00:00 GMT  
 Debuggers, Static Debuggers, and Algebraic Steppers

|
| Here is why. Suppose your program is a function  from
|
|   S-expression -> int
|

The trouble is, most of the programs I use aren't functions.  The
return values of Microsoft Word or Roller Coaster Tycoon are of type
int, but it's irrelevant to users.  What's important is the side
effects (mostly on screen, but also on paper, over the network,
through the sound card, and so on), and that's when I have to give up
the nice world of functional programming and return to time-step based
debugging. :(

   - Amit
--
--
Amit J Patel, Computer Science Department, Stanford University
http://www-cs-students.stanford.edu/~amitp/



Thu, 14 Nov 2002 03:00:00 GMT  
 Debuggers, Static Debuggers, and Algebraic Steppers

Quote:


> |
> | Here is why. Suppose your program is a function  from
> |
> |   S-expression -> int
> |

> The trouble is, most of the programs I use aren't functions.  The
> return values of Microsoft Word or Roller Coaster Tycoon are of type
> int, but it's irrelevant to users.  What's important is the side
> effects (mostly on screen, but also on paper, over the network,
> through the sound card, and so on), and that's when I have to give up
> the nice world of functional programming and return to time-step based
> debugging. :(

Not if you had learned to program functionally :-)
  [I have to admiit here that I tried to teach Amit something many years
    ago when he was a Rice undergraduate. One of us failed .... ]

Every interesting  system  has value flow. The question is how to reason
about the flow of values and how to express it.  The latter concerns both
the programming style and the way tools report about your program. The
former is an eternal truth that's always hidden in the imperative languages
that you prefer to use (though some are redeemable but you fail to see it).

Of course, as a PhD student you should feel challenged that one can build
Spidey-like tools for imperative languages with similarly nice interfaces.
ESC doesnt' count.

-- Matthias



Fri, 15 Nov 2002 03:00:00 GMT  
 Debuggers, Static Debuggers, and Algebraic Steppers

Quote:



> > |
> > | Here is why. Suppose your program is a function  from
> > |
> > |   S-expression -> int
> > |

> > The trouble is, most of the programs I use aren't functions.  The
> > return values of Microsoft Word or Roller Coaster Tycoon are of type
> > int, but it's irrelevant to users.  What's important is the side
> > effects (mostly on screen, but also on paper, over the network,
> > through the sound card, and so on), and that's when I have to give up
> > the nice world of functional programming and return to time-step based
> > debugging. :(

> Not if you had learned to program functionally :-)
>   [I have to admiit here that I tried to teach Amit something many years
>     ago when he was a Rice undergraduate. One of us failed .... ]

> Every interesting  system  has value flow. The question is how to reason
> about the flow of values and how to express it.  The latter concerns both
> the programming style and the way tools report about your program. The
> former is an eternal truth that's always hidden in the imperative languages
> that you prefer to use (though some are redeemable but you fail to see it).

If I understand your sentence correctly, by "former" you refer to "how
to reason about the flow of values" , and by "latter" you refer to "how
to express the flow of values".

In what way are the flow of values hidden in imperative languages, and
"not hidden" in functional?

Quote:

> Of course, as a PhD student you should feel challenged that one can build
> Spidey-like tools for imperative languages with similarly nice interfaces.
> ESC doesnt' count.

> -- Matthias

What is ESC?

Thanks,
John



Fri, 15 Nov 2002 03:00:00 GMT  
 
 [ 20 post ]  Go to page: [1] [2]

 Relevant Pages 

1. ML debugger / stepper

2. Stepper/Debugger for Common Lisp...

3. using python debugger (pdb) inside emacs debugger mode ...

4. How to use Clarion Debugger (c4dbx.exe) how the system debugger in Windows95?

5. Announce: v 1.1 SICStus Source debugger & Emacs debugger interface

6. Silencing the Debugger

7. J debugger

8. Debugger>>toggleBreakpoint not implemented

9. StepView debugger

10. Information about Debugger for APL*PLUS (Jim Weigang)

11. Debugger bug ?

12. debuggers

 

 
Powered by phpBB® Forum Software