The weakest prespecification
type: Item
instance of: scholarly article
title: The weakest prespecification
zbMATH Open document ID: 0622.68025
DOI: 10.1016/0020-0190(87)90106-2
author: Jifeng He
author: Tony Hoare
published in: Information Processing Letters
publication date: 1987-01-01T00:00:00Z
review text: 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.
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 68P05
zbMATH DE Number: 4009801
zbMATH Keywords: weakest prespecification
zbMATH Keywords: relational calculus
zbMATH Keywords: weakest precondition
zbMATH Keywords: guarded command
zbMATH Keywords: general recursion
MaRDI profile type: Publication
full work available at URL: 0020-0190(87)90106-2
OpenAlex ID: W2163008980
cites work: The mathematical construction of a program
cites work: Guarded commands, nondeterminacy and formal derivation of programs
cites work: Q3859249
description: scientific article; zbMATH DE number 4009801