Sorry to be so long in responding. I've been getting a cold.
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.
You are right. I hadn't thought of that.
> 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.
I see. I think the best way to handle this is with something like the
"terminates unless" idea. We could have this kind of implicit pre- and post-
condition, but allow the user to specify that the default isn't wanted.
The syntax might be something like:
pointers defined unless P
and omitting the clause means P is false. Perhaps something finer controlled
is needed, but this is just off the cuff.