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