×

The weakest prespecification. I. (English) Zbl 0603.68009

In Dijkstra’s calculus of weakest preconditions a program is generally specified by a predicate R describing the desired properties of the values of the program’s variables when the program successfully terminates. If Q is a program, the weakest precondition \(S = wp(Q,R)\) gives a predicate S which can be used as the most general specification of a program P which is to be executed before Q in order to guarantee that the combination P;Q will meet the original specification R.
The weakest prespecification of program Q and specification R will be written \(Q\setminus R\). It serves the same purpose as Dijkstra’s weakest precondition, but generalizes 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.
(2) The parameter Q may be a program, or it 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 sub-tasks Q and \(Q\setminus R\); then any implementation of \(Q\setminus R\), when composed sequentially with any implementation of Q, is guaranteed to meet the original requirement R.
(3) A partial relation R is taken as the specification of a guarded command, whose guard must be contained in the domain of R. 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, of which iteration is a simple special case.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68N01 General topics in the theory of software
68W99 Algorithms in computer science
PDFBibTeX XMLCite