Lambda the Ultimate

inactiveTopic Bertrand Meyer: Proving Program Pointer Properties
started 1/31/2003; 2:54:46 AM - last post 2/4/2003; 5:31:46 AM
Ehud Lamm - Bertrand Meyer: Proving Program Pointer Properties  blueArrow
1/31/2003; 2:54:46 AM (reads: 1564, responses: 1)
Bertrand Meyer: Proving Program Pointer Properties
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

Jussi Santti - Re: Bertrand Meyer: Proving Program Pointer Properties  blueArrow
2/4/2003; 5:31:46 AM (reads: 472, responses: 0)
I do not know, what is new, but I was able to read 40 pages of proofs! Would say it is readable.

Even though your objects have pointers to other objects but -pointers in objects only -no pointers to stack -no pointers to subobjects -no globals -no assignment to foreign objects x.a : = b -garbage collection Then the compiler writer can prove his/her memory management. When you also have specifications of your classes, you can prove (many of) them one at a time: -using simple set theory -mechanically?

Will have a compiler with prover?