[Prev][Next][Index]

Re: default qualification in Larch/C?

Gary,

Good questions.  We've grappled with this issue several times, trying 
to either make the LM3 model like the LCL model or vice versa.  We 
keep being driven back to the conclusion that "objects" are just 
semantically different in C and in in Modula-3, and that to force 
a superficial correspondence leads to problems with one language 
or the other.

    *    *    *

There are many ways to view the difference, but perhaps the crispest 
distinction is that Modula-3 references never point to anything but 
entire objects in the heap.  There is no taking addresses of variables, 
no address arithmetic, no treatment of arrays as references.  "Var" 
parameters have mode "VAR," rather than being treated as references.  
Thus it is very easy to use a storage model in which there is a (conceptual) 
array associated with each reference type, with references acting 
as indices into those arrays.  In the common case, where the type 
referred to is a record or an object, each field can be treated as 
an independent (non-aliasable) array, still indexed by references. 

Thus, when a reference, say r, appears alone in an expression, we 
almost always mean the reference itself, r\obj.  But when a component, 
say r.f, appears, we are interested in its pre- or post-state value,
f\pre[r] or f\post[r].  If the variable isn't modified, either will 
do.  Except for the result, we find that f\pre occurs more frequently 
than f\post, so we default to that.

In C, however, it is just not feasible to treat pointers as indexes 
into the heap.  They alias with variables all the time.  Furthermore, 
it is quite common to be interested in the pre- or post-state value 
that a pointer points to, even if it isn't qualified with a field 
name.  So we need three sugared "flavors" of x.  We could have made 
x\pre the default, and invented a notation such as x^ for x\obj, 
but it seemed funny to desugar x^ as x, x as pre[x], and x' as post[x]. 
So we chose the more symmetrical sugars x for x, x^ for pre[x], and 
x' for post[x].  This decision is certainly debatable (and was debated), 
but there is no question that it is the one documented in all the 
material about LCL. 

    *    *    *

I don't have the experience to know whether C++ usage is so different 
from C usage that a designer looking only at C++ would make a different 
decision than we made for C.  Your example suggests that perhaps 
you would.  Then you have to decide whether being nicer for C++ is 
more important than being compatible with LCL.  The designers of C++, 
of course, have had to continually wrestle with the same kind of 
problem.

    *    *    *

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

Right.  In the modifies clause, x\obj is almost always what you want.

    Stack() {  // constructor
       modifies self;
       ensures self' \eq empty;
    }

I would have expected

  Stack() {  // constructor
     ensures self' \eq empty /\ fresh(self\obj);
  }

"self" can't be modified (or can't not be modified, depending on 
your point of view), because it doesn't exist in the pre-state.  
But you do want to say that it doesn't alias any pre-existing object
(unless that is implicit in your "// constructor" notation).

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

For the same reasons, I think

  ~Stack() {  // destructor
     ensures trashed(self\obj); 
  }

This brings the number of explicit qualifications to 7, which isn't 
so very different from the 8 required by the LCL conventions.

Jim H.

PS Personally, I hate the need to write x^, especially when, as you 
note, the value isn't changing.
Follow-Up(s):