[comp.theory] PD theorem prover

PAAAAAR@CALSTATE.BITNET (01/06/90)

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