Date: 15 May 1999 14:20:49 +0200 From: Dag-Erling Smorgrav <des@flood.ping.uio.no> To: "Daniel C. Sobral" <dcs@newsguy.com> Cc: Dag-Erling Smorgrav <des@flood.ping.uio.no>, chat@FreeBSD.ORG, Wes Peters <wes@softweyr.com>, hackers@FreeBSD.ORG Subject: Re: BSD, GPL, the world today. Message-ID: <xzpwvyasevy.fsf@localhost.ping.uio.no> In-Reply-To: "Daniel C. Sobral"'s message of "Sat, 15 May 1999 20:49:48 %2B0900" 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>
next in thread | previous in thread | raw e-mail | index | archive | help
"Daniel C. Sobral" <dcs@newsguy.com> writes:
> Dag-Erling Smorgrav wrote:
> > [...] but the hardest
> > part of the job - finding loop and type invariants and post- and
> > pre-conditions which the prover can use as starting points - must
> > still be done manually.
> Things like SPIN goes a long, long way to make such proofs more
> viable. Take, for instance, correctness proofs of Fluke IPC
> subsystem.
Invariants and pre- and post-conditions (aka internal documentation)
must still be written by humans. The computer can prove that a
subroutine fulfills its purpose, but it can't guess at that purpose.
The best it can do is start with type invariants ("this function
receives one integer parameter, and integers range from -2^31 to
2^31-1"), and use forward construction to generate a post-invariant
for the function, but such machine-generated post-invariants are
mostly useless. Inference rules which rely on right consequence and
right-constructive axiom schemas tend to produce complicated
expressions riddled with icky quantifiers (in other words, garbage -
provably correct garbage, but garbage nonetheless). For a useful
proof, you need either a very restrictive precondition, or a
postcondition which accurately describes the intended result. The
latter is preferred, since left construction is much easier to handle
than right construction.
As long as programs are written by humans, making human assumptions,
humans will be required to document their assumptions.
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...
DES
--
Dag-Erling Smorgrav - des@flood.ping.uio.no
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?xzpwvyasevy.fsf>