Abstract: The validity of C.A.R. Hoare's well-known method for verifying data refinements was described by him as ``a fairly obvious theorem''; but a rigorous proof of this for realistic programming languages has not been possible due to the surprising reason that there has not been a satisfactory semantics for local-variable declarations in the context of higher-order procedures. This problem is addressed by a new model of Algol which incorporates Hoare's ideas on verifying data representations into the semantic interpretation of local variables.
This report is not available electronically. It has subsequently been published in ``A Classical Mind, Essays in Honour of C. A. R. Hoare'', Editor W. Roscoe, Prentice-Hall International, 1994.
LFCS report ECS-LFCS-93-267, May 1993.Previous | Index | Next