A calculus of refinements for program derivations
type: Item
instance of: scholarly article
title: A calculus of refinements for program derivations
zbMATH Open document ID: 0658.68018
DOI: 10.1007/BF00291051
published in: Acta Informatica
publication date: 1988-01-01T00:00:00Z
review text: This paper presents a semantic formalization of the stepwise refinement programming method. It extends earlier work of the same author, but it is selfexplanatory. The basic notion of the author's refinement calculus is the relation of correct refinement between programs: A program S is said to be correctly refined by another program S' if S' satisfies any specification that S satisfies. Specifications are treated as (non- executable) program statements, which determine a well-defined effect on the program state. Since a specification may be restricted to some of the properties, it acts like a nondeterministic statement. The approach is based on predicate transformers (Section 2) and is illustrated using a simple programming language (Section 3). In Section 4, the precise definition of a correct refinement is given. Then, the author shows that sequential and conditional composition, iteration and recursion are monotonic with respect to the refinement relation. (In an appendix, the author proves monotonicity in the case of unbounded nondeterminism.) The main result is a characterization of a correct refinement by reducing it to a specific pre-/\(post\)-condition formula that depends only on the statement being refined. Section 7 analyses the special case that the refinement does not introduce new variables. Finally, context-dependent refinements are considered. A small example rounds off this clearly written paper.
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 68N01
zbMATH DE Number: 4076587
zbMATH Keywords: program development
zbMATH Keywords: program transformation
zbMATH Keywords: correctness
zbMATH Keywords: semantics
author: Ralph-Johan Back
reviewed by: H. J. Schneider
describes a project that uses: Find
MaRDI profile type: Publication
cites work: Countable nondeterminism and random assignment
cites work: Q3898009
cites work: Proving total correctness of nondeterministic programs in infinitary logic
cites work: On correct refinement of programs
cites work: Q4184269
cites work: Q3783489
cites work: A Weaker Precondition for Loops
cites work: Q3875322
cites work: A Transformation System for Developing Recursive Programs
cites work: Q4144755
cites work: A simple fixpoint argument without the restriction to continuity
cites work: Q3925859
cites work: Predicative programming Part I
cites work: An axiomatic basis for computer programming
cites work: Proof of a program
cites work: The specification statement
cites work: A theoretical basis for stepwise refinement and the programming calculus
cites work: General correctness: A unification of partial and total correctness
cites work: A Powerdomain Construction
cites work: Q3932278
cites work: Q5551146
cites work: Power domains
cites work: Program development by stepwise refinement
full work available at URL: https://doi.org/10.1007/bf00291051
OpenAlex ID: W2038814435
description: scientific article; zbMATH DE number 4076587