Re: alternative to "trashed"


> This seems to me exactly the reason for *not* mixing up the
> specification of the storage state with the effects of constructors
> and destructors; they really are complete separate in C++.  

That makes a lot of sense to me (but I'm not a C++ expert.)

> An abstract pointer value <loc, inHeap, objectId> with inHeap TRUE is
> valid iff validMap[loc] = objectId.

Of course, one ramification of this approach is that the pre-condition of
each procedure must require that any abstract pointer (object) that the
implementation might dereference is valid.  Here's a simple example:

	DeepCopyList = proc (l1: list) returns (l2: list)
	    requires ValidPointers(reach(l1,pre))
	    modifies --
	    ensures  similar(l1^,l2',post) & New(reach(t2,post))

Such pre-conditions can be a nuisance to write and to discharge.
Unfortunately, they are probably unavoidable if the source language lacks
garbage collection.  (BTW, post-conditions will also need to specify which
pointers are valid upon return.  In the example, this is part of the
semantics of New.)

However, if the source language does have garbage collection, an *implicit*
pre-condition is that every pointer accessible to the procedure (e.g., every
pointer reachable from the arguments) must be valid.  Because the
pre-condition is implicit, it costs nothing to write.  (There is also an
implicit post-condition.)

Of course, the proof obligations must still be discharged.  My personal
opinion is that it's more natural (and easier) to place the burden of proof
on the caller of the deallocation routine, rather than placing the burden of
proof on each procedure and expression that dereferences a pointer.  I don't
have a semantics worked out, but I think it could be done without too much
difficulty.  Maybe some day after graduation . . .


Follow-Up(s): Reference(s):