-------- Original Message -------- Subject: Re: Source Code Date: Wed, 15 Sep 2004 10:01:23 -0700 From: Sriram Sankaranarayanan <srirams@CS.Stanford.EDU> To: Roberto Bagnara <bagnara@cs.unipr.it> Dear Roberto, Thanks for the fix! I fixed the problem in my version and it compiles fine. I am assuming you have already removed the offending brackets in yours.

...

it will print a message prefixed by the word ERROR on the stderr stream if something breaks (i.e, the computed invariant fails the inductive check.. which is finally all we care about :-)

Hey, but you proved it correct, didn't you? :-)

Yes.. but to quote Don Knuth, "Beware of bugs in the above code; I have only proved it correct, not tried it." Sriram -- Prof. Roberto Bagnara Computer Science Group Department of Mathematics, University of Parma, Italy http://www.cs.unipr.it/~bagnara/ mailto:bagnara@cs.unipr.it