DEVELOPMENT METHODS FOR COMPUTER PROGRAMS INCLUDING A NOTION OF INTERFERENCE

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.