Path: utzoo!utgpu!jarvis.csri.toronto.edu!clyde.concordia.ca!uunet!cs.utexas.edu!sun-barr!decwrl!ucbvax!CALSTATE.BITNET!PAAAAAR
From: PAAAAAR@CALSTATE.BITNET
Newsgroups: comp.theory
Subject: Re: PD theorem prover
Message-ID: <C-256.THEORYNT@ibm.com>
Date: 5 Jan 90 21:54:53 GMT
Sender: daemon@ucbvax.BERKELEY.EDU
Reply-To: PAAAAAR%CALSTATE.BITNET@VM1.NoDak.EDU
Lines: 14

Steven K. Roggenkamp, skr@uncle.UUCP,
wrote
>My own personal interest in this area is using a theorem prover as an
>aid for formal program specifications
[...]
> It seems a theorem prover should be
> useful for this purpose

Woodcock (of the Z group at Oxford University (Engleand))
wrote a paper on this recently. He/it claimed that a program by Abrial
was a great help  in the construction of proofs.

Woodcock 89b, JCP Woodcock, Calculating Properties of Z
Specifications, ACM SIGSOFT Software Engineering Notes, v14n5(Jul 89)pp43-54