The weakest prespecification (Q1091121): Difference between revisions

This paper introduces the concept of the weakest prespecification of program Q with respect to specification R, written \(Q\setminus R\), and explores its basic properties within the framework of the relational calculus. The weakest prespecification serves the same purpose as Dijkstra's weakest precondition, but generalises it in four ways. (1) The specification R describes not only the desired properties of the final values of the variables, but also their desired relationship with the initial values; such specifications are normal in specification languages like VDM and Z. (2) The program Q may be just the specification of a program still to be written. Consequently, the weakest prespecification can assist in splitting a task R into two subtasks Q and \(Q\setminus R\). (3) A partial relation R is taken as the specification of a guarded command, thus guarded commands can be specified and implemented independently, before being collected into a set with if or do. (4) The programming language is extended to include general recursion.