Programming Research Group Technical Monograph PRG-44

C A R Hoare and He Jifeng

June 1985, 60 pages, ISBN 0-902928-26-0

The Weakest Prespecification (written Q \ R) is a generalisation of Dijkstra's weakest precondition, wp(Q,R) in the following ways:

1. The specification R can be given (as in Z or VDM) by a desired relationship between the initial and final values of the program variables.
2. The parameter Q may be not only a command, but also the specification of a command yet to be written. This is useful in top-down methods of program design.
3. The specification R may be a partial relation, which can be implemented by a single guarded command, which will later be combined into a guarded command set.
4. The weakest prespecification is defined for a language permitting general recursion, not just iteration.

Section 1 of the paper proves the basic properties of the weakest prespecification within the framework of the relational calculus. Section 2 defines an extended version of Dijkstra's programming language; programs are a particular inductively defined subset of all relations, which are total; they enjoy a number of useful additional properties, including computability. Section 3 shows how weakest prespecifications and Dijkstra's programming language can be treated within the framework of VDM, in which a specification or a program is expressed in terms of a precondition as well as a relation. The more elaborate proofs are relegated to the appendix, where they are treated entirely within the framework of the relational calculus.