Path: utzoo!attcan!uunet!snorkelwacker!apple!agate!agate!hughes
From: hughes@tempest.Berkeley.EDU (Eric Hughes)
Newsgroups: comp.software-eng
Subject: Re: "Program Proving"
Message-ID: <HUGHES.90Mar19065317@tempest.Berkeley.EDU>
Date: 19 Mar 90 14:53:17 GMT
References: <52044@microsoft.UUCP> <2480006@hpcuhc.HP.COM>
Sender: usenet@agate.berkeley.edu (USENET Administrator;;;;ZU44)
Organization: ucb
Lines: 11
In-reply-to: runyan@hpcuhc.HP.COM's message of 13 Mar 90 19:36:56 GMT

In article <2480006@hpcuhc.HP.COM> runyan@hpcuhc.HP.COM (Mark Runyan) writes:
>   As an alternative, someone could post a non-trivial program and ask the
>   program provers to prove it either correct or incorrect...

This really isn't the way it's done.  The idea is to develop the
program and its proof simultaneously.  The generation of invariants
and assertions is more difficult (at least now, since there is not
as much cultural experience) than writing the code.

Eric Hughes
hughes@ocf.berkeley.edu