Local Variables and Non-Interference in Algol-like Languages

Abstract

Finding a suitably abstract semantics for the stack-implementable local variables in Algol-like languages has proved to be a difficult problem [7]. In the traditional denotational-semantic approach, each state records which storage variables are in use. This approach is operationally adequate, but does not capture many of the abstract properties of the local-storage discipline and is inadequate for reasoning about programs with local-variable declarations. To address this problem, researchers [?,?] have shown how to define the "storage support" of semantical entities by induction on types. Then the storage variable chosen to be the meaning of a locally declared variable identifier can be any variable outside the support of the block body, and the meaning of the block is independent of which such variable is chosen. However, this approach is technically very intricate. J. C. Reynolds [7] and F. J. Oles [?,?] proposed the use of a categorytheoretic form of possible-world semantics to capture the local-storage discipline more directly: types and type assignments are interpreted as functors from a suitable category of "worlds" (e.g., a world is a set of states) to a category of domains, and phrases are then interpreted as natural transformations of these functors. Local-variable declarations are easily treated in this framework by allowing changes of world that "expand" the set of states; e.g., a change from some set S to a set of the form S x V, where V is the set of values that a new variable might contain. The author and P. O'Hearn [?,?,?] have since used this functor-category framework to interpret the concept of non-interference used by Reynolds [?, 7] in his "specification logic," a version of Hoare's logic that allows modular reasoning about programs in Algol-like languages with higher-order procedures.

Topics

0 Figures and Tables

    Download Full PDF Version (Non-Commercial Use)