An Intensional Semantics for Elementary Program Transformations

摘要

This paper is a contribution to the formal study and analysis of vernacular forms of program derivation. Specifically, in this paper, our vernacular derivations are elementary program transformations over the natural numbers. We provide an intensional semantics for these transformations within the derivations of the elementary theory of operations and numbers,ɛON. This semantics is intensional in the sense that the computational content of a derivation associated with a transformation is equal, up to the intensional equality underlying the theoryɛON, to the computational content of the transformation itself. The interpretation enables us to underwrite the correctness of the program transformations and, further, provides an analysis of correctness by classifying, via schema, the operations available by these transformation