valid pointers


   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.

This makes sense, because if you never deallocate, then there is nothing
to prove.  But this seems to be a verification issue.  Can't we verify against
specifications written with "trashed" and use a verification logic that
talks about "last_used"?

I would think it possible (perhaps naively) to do *specification* in C++
in the same way as CLU.  That is, to have an implicit pre-condition that
every pointer accessible is valid.  The pre-condition you note seems to
be automatically derivable, and it would be a burden to have all C++
specifications have to mention it explicitly.


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