Hoare, C. A. R.; He, Jifeng The weakest prespecification. (English) Zbl 0622.68025 Inf. Process. Lett. 24, 127-132 (1987). 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. Cited in 23 Documents MSC: 68Q60 Specification and verification (program logics, model checking, etc.) 68P05 Data structures Keywords:weakest prespecification; relational calculus; weakest precondition; guarded command; general recursion PDF BibTeX XML Cite \textit{C. A. R. Hoare} and \textit{J. He}, Inf. Process. Lett. 24, 127--132 (1987; Zbl 0622.68025) Full Text: DOI References: [1] Abrial, J. R., The mathematical construction of a program, Sci. Comput. Programm., 4, 45-86 (1984) · Zbl 0543.68004 [2] Dijkstra, E. W., Guarded commands, nondeterminacy and the formal derivation of programs, Comm. ACM, 18, 453-457 (1975) · Zbl 0308.68017 [3] Jones, C., Software Development: A Rigorous Approach (1980), Prentice-Hall: Prentice-Hall Englewood Cliffs, NJ · Zbl 0424.68019 [4] Sufrin, B., Mathematics for system specification, (Lecture Notes 1983/1984 (1983), Programming Research Group: Programming Research Group Oxford) [5] Tarski, A., A lattice-theoretical fixpoint theorem and its applications, Bull. Amer. Math. Soc., 55, 1192 (1949) [6] Tarski, A., On the calculus of relations, J. Symb. Logic, 6, 73-89 (1941) · JFM 67.0973.02 This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.