[Prev][Next][Index]

alternative to "trashed"


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.

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.  

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.
Although such specifications may sometimes be costly or complicated, they can
be used in other ways, too.  For example, if the interface language allows
partial specifications, reachability can be used to make conservative
estimates for missing "modifies" clauses.  I've found such estimates to be
particularly useful in Speckle.

 -Mark

P.S. I stole the phrase "last_use" from Andy Hisgen's thesis.
Follow-Up(s):