Program construction by refinements preserving correctness

This paper deals with the problem of constructing the final version Pt of a flowchart program through successive refinements P2, …, Pt−1 that preserve correctness proved on its first version P1. Correctness conditions are associated with P1 in the frame of Manna's formalism. With each refinement Pi a relational (data) structure Si is associated, and given representation functions τi relate structures Si, Si+1 of refinements Pi, Pi+1. Construction of Pi+1 from Pi proceeds as follows: (a) every block of Pi is considered as an elementary program over Si and its correctness conditions are expressed with terms of Si; (b) these correctness conditions are translated by using the representation function τi; (c) the translated correctness conditions are transformed into expansion conditions, expressed with terms of Si+1 only, for every block of Pi; (d) by means of these expansion conditions, expansions of blocks are constructed and connected to obtain Pi+1. The constructive character of the above process is emphasised with a detailed example. In the appendix a discussion relates this paper to other works connecting constructivism and program theory.