Re: valid pointers


> This makes sense, because if you never deallocate, then there is nothing
> to prove.  

Even in a garbage-collected languageg, one might want to prove that an object
can be reclaimed, e.g., to substitute mutation for allocation.  In fact, I
became interested in this problem for this reason.

>           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.

Yes, but the implicit pre- and post-conditions may be stronger than some
would want in a language with explicit deallocation.  For example, if
allocation routines return memory containing meaningless pointers, one needs
initialization routines whose pre-conditions allow them to initialize such
memory.  My default pre-condition does not.


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