[Prev][Next][Index]
valid pointers
Mark
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.
Gary
Follow-Up(s):
Reference(s):