Proving Pointer Program Properties. Part 2: The Overall Object Structure.
Bertrand Meyer · The Journal of Object Technology · 2003
The run-time object structure of object-oriented programs typically relies on extensive use of references (or pointers).This second part of a general mathematical framework for reasoning about references handles the overall properties of the structure, not distinguishing between individual links but only considering whether any reference exists between two objects.It provides a basis for dealing with memory management and especially garbage collection.This is part of a series of articles. See here for part 1. BASICS OF THE RELATION MODELThe coarse-grained model of object structures developed here will rely on a relation between objects.For this reason we call it the relation model; the finer-grained models of the subsequent articles, which take into account individual attributes of classes, and hence individual fields of objects, will expand this relation into a set of functions.