Skip to main content

DEVELOPMENT METHODS FOR COMPUTER PROGRAMS INCLUDING A NOTION OF INTERFERENCE

C.B.Jones

Abstract

A relational basis is used for the systematic development of programs. Abstract data types are defined by models and a proof method of data refinement is given. Proof rules for various sequential control constructs (e.g. if, while) are given and proved valid with respect to a denotational semantics for the non-deterministic language. Monotonicity in the semantics is linked to the needs of a stepwise development procedure. Interference from parallel tasks which can change shared variables is also covered in the development process. The appropriate proof rule is related to an operational semantics.

Institution
OUCL
Month
June
Number
PRG25
Pages
257
Year
1981