Pointers and Records in the Unifying Theories of Programming

摘要

We present a theory of pointers and records that provides a representation for objects and sharing in languages like Java and C++. Our approach to pointers is based on Paige's entity groups, which give an abstract view of storage as equivalence classes of variables that share the same memory location. We first define our theory as a restriction of the general theory of relations, and, as a consequence, it does not distinguish between terminating and non-terminating programs. Therefore, we link it with the theory of designs, providing a foundation for reasoning about total correctness of pointer-based sequential programs. Our work is a step towards the semantics of an object-oriented language that also integrates constructs for specifying state-rich and concurrent systems.