Hoare, C. A. R.; He, Jifeng The weakest prespecification. I. (English) Zbl 0603.68009 Ann. Soc. Math. Pol., Ser. IV, Fundam. Inf. 9, 51-84 (1986). 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. Cited in 4 ReviewsCited in 18 Documents MSC: 68Q60 Specification and verification (program logics, model checking, etc.) 68N01 General topics in the theory of software 68W99 Algorithms in computer science Keywords:formal methods; program development; software engineering; Dijkstra’s calculus of weakest preconditions; weakest prespecification; general recursion PDFBibTeX XMLCite \textit{C. A. R. Hoare} and \textit{J. He}, Ann. Soc. Math. Pol., Ser. IV, Fundam. Inf. 9, 51--84 (1986; Zbl 0603.68009)