[Prev][Next][Index]

Semantics of trashed

I've been thinking about the semantics of destructors in Larch/C++ and
would like your opinions---especially if you are involved in Larch/C.

Consider the Larch/C++ specification of the destructor for the class Stack.

We have been writing it...
  
   ~Stack() {  // destructor
      modifies self;
      ensures trashed(self); 
   }

(The ~ is part of the C++ syntax that tells you it's a destructor.)

But what does "trashed(self)" mean?

The semantics of C++ are such that if you have a variable
	Stack * my_stack;
and you execute the statement
	delete my_stack;
then the storage (presumably on the heap) for my_stack has been deallocated.
The programmer's responsibility in implementing the destructor is to deallocate
any contained objects (by deleting them).  But that's not really client
visible.   So if I think about the proof rule for the delete statement,
it's something like:

	wp(delete my_stack, Q) = Q, provided Q does not
                                    have free refs to my_stack.

Does that seem right?
If so, it makes no connection whatsoever to the post-condition
of the destructor.  Perhasps it should at least say that it calls the
destructor (so if it loops forever the delete doesn't terminate,
but this seems close enough.)
So why not avoid the complications of trying to
say what "trashed(self)" means and let the destructor be specified by:

   ~Stack() {  // destructor
      modifies self;
      ensures true;
   }

Which seems to say, quite elegantly, that you don't know anything about
the abstract value of self after calling the destructor, and that the
destructor terminates.


The other thing you want to say with a destructor is that contained objects
are deallocated.  You might write that as follows
(perhaps with self\obj instead of self?):

   ~Stack() {  // destructor
      modifies self, reach(self);
      ensures trashed(self) /\ trashed(reach(self)); 
   }

But then why not just say the following?

   ~Stack() {  // destructor
      modifies self, reach(self);
      ensures true; 
   }

Opinions?

	Gary

	229 Atanasoff Hall, Department of Computer Science
	Iowa State University, Ames, Iowa 50011-1040, USA
	phone: (515) 294-1580  fax: (515) 294-0258

P.S. Can you tell I have a bit of time to work on Larch/C++ tonight?