Re: Super Lint

[Jeff Dike]

[e-mail] said:
> It can, however, verify the rest of the program and tell you that
> all's   fine except for these lines, where it can't prove the
> postconditions from   the preconditions. 

Right.  Those messages will call attention to pieces of code that you need to 
pay special attention to, or which are more complicated than they need to be.

99.9% of the theorems that need to be proved are completely trivial.  The only 
ones that are at all complicated as a group are the ones involved in ruling 
out infinite loops.

> This should be enough in praxis. And for testing, you can often add an
>   assertion. 

If you're serious about this, you'll prove them by hand, or simplify them to 
that they can be proved automatically.

				Jeff