Date: Sun, 16 May 1999 01:31:20 +0900 From: "Daniel C. Sobral" <dcs@newsguy.com> To: Dag-Erling Smorgrav <des@flood.ping.uio.no> Cc: chat@FreeBSD.ORG, Wes Peters <wes@softweyr.com>, hackers@FreeBSD.ORG Subject: Formal methods Message-ID: <373DA158.62F01B6B@newsguy.com> References: <199905131530.LAA04222@etinc.com> <xlxso8z2w76.fsf@gold.cis.ohio-state.edu> <373CB22B.4843BD45@softweyr.com> <19990515014823.A82329@catkin.nothing-going-on.org> <xzpiu9u39kq.fsf@localhost.ping.uio.no> <373D5F5C.4D19831F@newsguy.com> <xzpwvyasevy.fsf@localhost.ping.uio.no>
next in thread | previous in thread | raw e-mail | index | archive | help
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) dcs@newsguy.com dcs@freebsd.org "Proof of Trotsky's farsightedness is that _none_ of his predictions have come true yet." To Unsubscribe: send mail to majordomo@FreeBSD.org with "unsubscribe freebsd-hackers" in the body of the message
Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?373DA158.62F01B6B>