[Prev][Next][Index]

alternative to "trashed"

Mark,

Sorry to take a while to continue this thread of discussion.  I'm
back from giving a talk and have been swamped with reading and grading...

   I view destructor operations as no-ops with a requirement.  E.g.,

     ~Stack() { // destructor
       requires last_use(self)
       modifies nothing
     }

   Informally, "requires last_use(self)" means that upon return, self will never
   be referenced.

Note that the omitted ensures clause would be "ensures true" (I guess).

   Of course, giving a formal semantics for "last_use" is no easier than for
   "trashed".  However, it does suggest a different style for proving that a
   program satisfies its specification.  Instead of proving that an object
   (location) was not deallocated prior to a point of reference, one proves that
   an object being deallocated will never again be referenced.  

This is intriging, but let me point out one potential problem.
Usually, we state requirements that can be checked at the point of a call.
It is not clear how to interpret last_use at the point of the call.
At an arbitrary point later in the program, the last_use may be invalidated,
which seems funny.

   I believe that any semantics for "last_use" (or "trashed") will require that
   data types specify which objects are reachable from an instance of the type.

I suppose that these would be user-visible objects.

I'm sure that one could give a semantics to destructors (although perhaps not
to "trashed") by explicitly modelling the store (or set of) active objects.
After destruction, the deallocated object would no longer be active.
As Jim Horning said, this would be a lot to add to the semantics for trashed.
However, one could imagine a separate semantics (orthogonal to the usual one)
that only deals with object allocation and deallocation.  (It would be a
kind of abstract interpretation of the specs.)

   P.S. I stole the phrase "last_use" from Andy Hisgen's thesis.

Where's that thesis from?

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