Re: Semantics of trashed
To: email@example.com (Gary Leavens)
Subject: Re: Semantics of trashed
Date: Fri, 05 Mar 93 12:18:44 -0800
In-Reply-To: Message of Thu, 4 Mar 93 23:36:18 CST
I'm glad that you are finding time to work on Larch/C++.
You are right about trashed. Given a programming-language-level
model of state, trashed has no formal semantics. It is a stylized
comment. On reflection, it is perhaps more akin to the modifies
clause than to the ensures clause. It was put in the ensures clause
by analogy with fresh, which does have a semantics (no aliasing with
If there is a language construct, such as "// destructor", that conveys
the same information, perhaps it should be used in preference to trashed.
Note, however, that "modifies self ensures true" makes quite a different
statement. It says that the value of the Stack isn't known on return
from ~Stack(). The difference between an object with an unknown
value and one that has been deallocated is enormous. The former,
for example, can be reinitialized by assignment. Assignment to the
latter can cause arbitrary damage that CANNOT BE DESCRIBED AT THE
PROGRAMMING LANGUAGE LEVEL, because it is implementation-dependent.
In fact, in perverse cases, even an attempt to reference a deallocated
variable can cause a program to crash or behave arbitrarily badly.
The stylized comment means "You REALLY don't want to access this
object ever again." We could, of course, develop a more complex
model of the program state that records enough information about
objects to know when deallocated objects are referenced and give
a completely formal account of trashed. However, it doesn't seem
very attractive to do so when the extra complexity would serve only
to formalize this one construct.