[Prev][Next][Index]

valid pointers



Mark,

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.

	Gary


Reference(s):