From owner-freebsd-chat Sat May 15 5:21: 8 1999 Delivered-To: freebsd-chat@freebsd.org Received: from flood.ping.uio.no (flood.ping.uio.no [129.240.78.31]) by hub.freebsd.org (Postfix) with ESMTP id AA29914FA7; Sat, 15 May 1999 05:21:03 -0700 (PDT) (envelope-from des@flood.ping.uio.no) Received: (from des@localhost) by flood.ping.uio.no (8.9.3/8.9.1) id OAA48888; Sat, 15 May 1999 14:20:50 +0200 (CEST) (envelope-from des) To: "Daniel C. Sobral" Cc: Dag-Erling Smorgrav , chat@FreeBSD.ORG, Wes Peters , hackers@FreeBSD.ORG Subject: Re: BSD, GPL, the world today. References: <199905131530.LAA04222@etinc.com> <373CB22B.4843BD45@softweyr.com> <19990515014823.A82329@catkin.nothing-going-on.org> <373D5F5C.4D19831F@newsguy.com> From: Dag-Erling Smorgrav Date: 15 May 1999 14:20:49 +0200 In-Reply-To: "Daniel C. Sobral"'s message of "Sat, 15 May 1999 20:49:48 +0900" Message-ID: Lines: 38 X-Mailer: Gnus v5.5/Emacs 19.34 Sender: owner-freebsd-chat@FreeBSD.ORG Precedence: bulk X-Loop: FreeBSD.org "Daniel C. Sobral" 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-chat" in the body of the message