A Calculus for Predicative Programming

A calculus for developing programs from specifications written as predicates that describe the relationship between the initial and final state is proposed. Such specifications are well known from the specification language Z. All elements of a simple sequential programming notation are defined in terms of predicates. Hence programs form a subset of specifications. In particular, sequential composition is defined by 'demonic composition', nondeterministic choice by 'demonic disjunction', and iteration by fixed points. Laws are derived which allow proving equivalence and refinement of specifications and programs. The weakest precondition is expressed by sequential composition. The approach is compared to the predicative programming approach of E. Hehner and to other refinement calculi.

• Type: Conference
• Year: 1992
• Where: MPC
• Authors: Emil Sekerinski
• Keywords: Mathematics, MPC 1992, Sequential Composition, Sequential Programming Notation, Specifications