default qualification in Larch/C?

To: larch-interest
Subject: default qualification in Larch/C?
From: leavens@cs.iastate.edu (Gary Leavens)
Date: Thu, 4 Mar 93 23:16:37 CST
Cc: leavens@cs.iastate.edu
Kevin Jones brought the following possible incompatibility between
Larch/C and Larch/C++ to my attention.  I wanted to ask if it was so
and if it should be so...

In Larch/C and Larch/C++, the name of a loc (object), say x,
can be qualified with ^ (or \pre), ' (or \post), and \obj.
	x^ means the abstract value of x in the pre-state
	x' means the abstract value of x in the post-state, and
	x\obj means the object itself (the address if you will).
An example of such an object is a formal argument of type int & in C++.

What should be the default qualification for x if it is unadorned?

We had been planning to follow LM3 and make x mean x^ (in pre- and post-
conditions) if it is unqualified.
(The default is x\obj in the modifies clause.)
However, since "result" has no value in the pre-state,
Larch/C++ does make an exception.  Thus "result"
has a default qualification of \obj when it is an object.
(This exception is irregular, so perhaps makes the rule suspect.)

But Kevin says that Larch/C has x\obj as the default (in pre- and post-
conditions only?) if it is unqualified.

Is that right?  If so what are the motivating examples?

Perhaps C++ is different enough in this to warrant a distinction,
but it's hard to believe.

Here's an example where I think (in Larch/C++) it's good to have the
defaults the way I noted above.

//  WITH CURRENT LARCH/C++ DEFAULT QUALIFICATION: ^
template <class Elem>
class Stack {

uses StackTrait(Stack for S, Elem for E);

public:
   Stack() {  // constructor
      modifies self;
      ensures self' \eq empty;
   }
  
   ~Stack() {  // destructor
      modifies self;
      ensures trashed(self); 
   }
  
   Stack<Elem>& push(Elem e) {
      modifies self;
      ensures self' \eq push(self,e) /\ result = self\obj;
   }

   Stack<Elem>& pop() {
      requires ~isEmpty(self);
      modifies self;
      ensures self' \eq pop(self) /\ result = self\obj;
   }

   Elem top() {
      requires ~isEmpty(self);
      ensures result = top(self);
   }

   int isEmpty() const {
      ensures result = int(isEmpty(self));
   }
};


Now try looking at the following with what Kevin tells me is the Larch/C
default.


//  WITH LARCH/C DEFAULT QUALIFICATION: \obj
template <class Elem>
class Stack {

uses StackTrait(Stack for S, Elem for E);

public:
   Stack() {  // constructor
      modifies self;
      ensures self' \eq empty;
   }
  
   ~Stack() {  // destructor
      modifies self;
      ensures trashed(self); 
   }
  
   Stack<Elem>& push(Elem e) {
      modifies self;
      ensures self' \eq push(self^,e) /\ result = self;
   }

   Stack<Elem>& pop() {
      requires ~isEmpty(self^);
      modifies self;
      ensures self' \eq pop(self^) /\ result = self;
   }

   Elem top() {
      requires ~isEmpty(self^);
      ensures result = top(self^);
   }

   int isEmpty() const {
      ensures result = int(isEmpty(self^));
   }
};


Perhaps it's what you're used to, but by my count there are 8 explicit
qualifications in the Larch/C style, and 5 in the (current) Larch/C++ style.
Furthermore, having to write a qualification on self in top and isEmpty
seems especially painful, since it brings to the fore the notion of state,
which is not of the essence for observers.

Opinions?  I'd like to track Larch/C, but I'd also like to do what's best...

	Gary