[Home] [CV] [Publications]


Minus 1a5aa4f1c08b567c9107cba729de26bc87c17ab2b2f690eb45059193a1d6f587 References, Local Variables and Operational Reasoning
Mason, I. A. and Talcott, C. L. - 1992

In the well known paper Meyer and Sieber give a series of examples of programs that are operationally equivalent (according to the intended semantics of block-structured Algol-like programs) but which are not given equivalent denotations in traditional denotational semantics. Since numerous proof systems for Algol are sound for the denotational models in question, these equivalences, if expressible, must be independent of these systems. In this paper we accomplish two goals. Firstly, we present the first-order part of a new logic for reasoning about programs. Secondly, we use this logic to prove the equivalence of the Meyer-Sieber examples. Our style of operational semantics naturally provides for the symbolic evaluation of contexts. This allows us to define the semantics of \it contextual assertions. Contextual assertions allows us to express that a property holds at the point in the program text where the hole appears. Contextual assertions generalize Hoare’s triples in that they can be nested, used as assumptions, and their free variables may be quantified. Our atomic formulas express the (operational or observational) equivalence of programs. Neither Hoare’s logic nor Dynamic logic incorporate this ability, or make use of such equivalences (for example by replacing one piece of program text by an equivalent one). In this paper we only describe the first order part of the logic. The full logic, a variable type theory of individuals and classes, is based on the systems of Feferman \citefeferman-explicit-75,feferman-poly-90 and Talcott \citetalcott-90disco.