[Prev][Next][Index]

Re: Semantics of trashed

Gary,

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 
existing storage). 

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. 

Jim H.
Follow-Up(s):