Proof-oriented and applicative valuations in definitions of algorithms
Michel Sintzoff · 1981
Our aim is to investigate means for expressing programs and their design, in such a way that the logical consistency of each expression be ensured constructively, and that the structure of the expressions be general and elegant. It is more and more apparent that the latter requirement is better ensured by functional constructs, viz. by pure expressions; indeed much attention is nowadays being paid to this aspect. But the treatment of the logic of the expressions is much less studied; as a rule, properties are proved by using an algebra of expressions [1,2] or by explicitly applying a powerful induction rule such as Scott's. The approach we propose is as follows, roughly speaking. To each expression we shall ascribe a pair of logical expressions, viz. the precondition and the postcondition. Then, in principle, the compatibility of an expression with a proposed input-ouput assertion is verified in three steps: to ascribe correct input-output assertions to the basic component expressions, to 'evaluate' the expression, and finally to check the resulting input-output assertion validates the proposed one. Thus neither preconditions nor postconditions should be privileged: both together are parameters and results of the valuations. 'Backwards', 'forward' are operational concepts we want to abstract from.