A calculus for predicative programming

Abstract

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’, non-deterministic choice by ‘demonic disjunction’, and iteration by fixed points. Laws are derived which allow proving equivalence and refinement of specifications and programs by a series of steps. The weakest precondition calculus is also included. The approach is compared to the predicative programming approach of E. Hehner and to other refinement calculi.