Dag-Erling Smorgrav wrote: > [invariants, pre-conditions, post-conditions] > > As long as programs are written by humans, making human assumptions, > humans will be required to document their assumptions.
Such as in modern structured languages. :-) (No, Perl and Python do not qualify! :) Anyway, SPIN does not avoid this, just make it more practical. > One other problem is proof of termination. A computerized proof system > may be able to prove termination of simple loops and some cases of > recursion, but anything more than that gets dangerously close to the > halting problem, which is unsolvable by a deterministic computer. Ghod > knows termination is hard enough to prove for humans... But one can use progress states to determine liveness properties, instead of proving termination. This is a much easier proof, and all that is really needed in most cases. That does not cover all cases, to be sure, and still requires you to know what you are doing, but does not make it unpractical. Finally, there are the partial exaustive searches. A partial exaustive search can cover much more states than a full exaustive search, as it can be restricted to as little as one or two bits of storage for each state. While they do not result in proofs, they do, in practice, find out the bugs. :-) -- Daniel C. Sobral (8-DCS) d...@newsguy.com d...@freebsd.org "Proof of Trotsky's farsightedness is that _none_ of his predictions have come true yet." To Unsubscribe: send mail to majord...@freebsd.org with "unsubscribe freebsd-hackers" in the body of the message