The present discussion proposes a mathematical theory for modeling pointerrich object structures and proving their properties.
The model has two principal applications:
 The coarsegrained version of the model,considering only the existence or not
of a reference between an object and another,gives a basis for discussing overall properties of the object structure,defining as a result the correctness
constraints of memory management and especially garbage collection,full or
incremental. Mathematically,this model uses a binary relation.
 The finegrained version,based on functions which together make up the
relation of the coarsegrained version,integrates the properties of individual
object fields. As a result,it allows proving the correctness of classes
describing structures with luxurious pointer foliage,from linked lists and
graphs to Btrees and doubleended queues.
Makes for interesting reading, though I am not sure if these papers contain new results.
As you might expect, Meyer uses an Eiffel like notation, and the preconditions, postconditions and invariants are used extensively...
Thanks Jussi!
Posted to theory by Ehud Lamm on 1/31/03; 3:00:15 AM

