|
The present discussion proposes a mathematical theory for modeling pointer-rich object structures and proving their properties.
The model has two principal applications:
- The coarse-grained 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 fine-grained version,based on functions which together make up the
relation of the coarse-grained 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 B-trees and double-ended 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
|
|
Bertrand Meyer: Proving Program Pointer Properties
