Skip site navigation (1)Skip section navigation (2)
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-chat" 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>