kaih@khms.westfalen.de 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
-
To unsubscribe from this list: send the line "unsubscribe linux-kernel" in
the body of a message to majordomo@vger.rutgers.edu
Please read the FAQ at http://www.tux.org/lkml/
This archive was generated by hypermail 2b29 : Fri Jan 07 2000 - 21:00:09 EST