Re: specification of destructive operation


You wrote about my definition of a trait that defines aliasing:

   > 	shared(l1,l2) == (l1 = l2)

   This is not the right definition. Two pointer objects are shared iff their  
   implementations contain a common cell.
   Eg. in the classical implementation of conc(l1,l2), l2 is shared in the

A specification being "right" or not depends on whether or not it corresponds
to some other (intuitive) notion of what is to be specified.
Clearly, your defintion of two lists being shared differs from what I thought.

What I specified was whether l1 and l2 are the same object.

To deal with what you mean requires more than what seems to be found
in either LCL or LM3.  Larch/C++ however, does have a systematic way
to deal with objects within abstract values, and like LM3 has reified states,
so you can pass whole states to trait functions.  In Larch/C++, for each
sort T, one specifies a trait function

	contained_objects: T, St -> Set[Object]

(where the sort St is the sort of states, essentially a mapping of
objects (locations) to values, and the sort Object is the sort of
untyped objects -- see the trait State below).

This allows a simple solution to the problem of defining a trait function
that tells whether two objects are indirectly aliased (at the top level).

TopLevelAliased(Loc, T) : trait
   includes TypedObj % see below, this is from the Larch/C++ release
   assumes contained_objects(T) % see below, this is from the Larch/C++ release
      top_level_aliased: T, T, St -> Bool
      top_level_aliased: Loc[T], Loc[T], St -> Bool
   asserts \forall l1, l2: Loc[T], v1,v2: T, st: St
      top_level_aliased(v1, v2,st)
	== not((contained_objects(v1,st) \I contained_objects(v2,st)) = {});
      top_level_aliased(l1, l2, st)
	== (l1 = l2) \/ top_level_aliased(l1!st, l2!st, st)

Of course, this leaves the work of defining what contained_objects
means for lists to you, but that is certainly possible by induction over
the structure of the list.

The above shows that your final comment...

   The problem of sharing is that it is not really abstract -- although it must  
   appear in the pre/post you cannot express it in abstract terms.

... is not true if you reify states as LM3 and Larch/C++ do.
In Larch/C++ we can express (assuming the objects involved are mutable...): 

   bool someListFun(List v1, List v2) {
        uses TopLevelAliased(Obj, List);
	requires not(top_level_aliased(v1, v2, pre));

which I think is what you wanted.

Your questions are not naive, however, because I think this use of reified
states in Larch/C++ to express properties of contained objects is new,
and hasn't been documented except in the Larch/C++ reference manual.
(I'd be interested to hear of other prior work on this idea;
I know it generalizes the work of Luckham and Suzuki about how to reason
about pointers in Pascal.)  Despite the fact that it's new,
it appears to be needed for a faithful treatment of
pointer-based data structures even in non-object-oriented languages.
You might look at the Larch/C++ treatment of C/C++ character strings
(trait cpp_char_string) in the Larch/C++ release for another example.

	Gary Leavens
	229 Atanasoff Hall, Department of Computer Science
	Iowa State Univ., Ames, Iowa 50011-1040 USA / leavens@cs.iastate.edu
	phone: (515)294-1580 fax: (515)294-0258 ftp site: ftp.cs.iastate.edu
	URL: http://www.cs.iastate.edu/~leavens/larchc++.html

% @(#)$Id: State.lsl,v 1.6 1995/01/04 04:19:51 leavens Exp $
% based on GIL [Chen89] and GCIL [Lerner91]
% The sort St is the sort of C++ states, which this formalizes.

State: trait
includes Set(Object, Set[Object], int for Int)    % from LSL handbook
  empty: -> St
  bind: St, Object, Value -> St
  bottom: -> St
  __ \in __: Object, St -> Bool
  eval: St, Object -> Value
  isBottom: St -> Bool
  added: St, St -> Set[Object]
  modified: St, St -> Set[Object]
  objs: St -> Set[Object]
  St generated by empty, bottom, bind
  St partitioned by \in, eval, isBottom
  forall obj,obj1:Object, s,s1:St, v,v1: Value
    ~(obj \in empty);
    obj \in bind(s,obj1,v) == (obj = obj1) \/ (obj \in s);
    eval(bind(s,obj,v),obj1) == if obj1 = obj then v else eval(s,obj1);
    ~(empty = bottom);
    ~(bind(s,obj,v) = bottom);
    obj \in added(s,s1) == ~(obj \in s) /\ (obj \in s1);
    obj \in modified(s,s1) == (obj \in s) 
      /\ ~((obj \in s1) /\ (eval(s,obj) = eval(s1,obj)));
    obj \in objs(s) == obj \in s;
    converts __ \in __:Object,St -> Bool,
             eval, isBottom, added, modified, objs
      exempting forall obj:Object, s:St
        obj \in bottom,
        added(bottom,s), added(s,bottom),
        modified(bottom,s), modified(s,bottom),

% @(#)$Id: TypedObj.lsl,v 1.7 1995/01/04 03:03:52 leavens Exp $
% Adapted from the Larch/Generic Interface Language [Chen 89]

TypedObj(Loc, T): trait
  includes State
    widen: Loc[T] -> Object
    widen: T -> Value
    narrow: Object -> Loc[T]
    narrow: Value -> T
    __ \in __: Loc[T], St -> Bool
    __ ! __: Loc[T], St -> T
    sort Loc[T] generated by narrow
    sort Loc[T] partitioned by widen
    \forall loc: Loc[T], obj: Object, tval: T, val: Value, s: St
      narrow(widen(loc)) == loc;
      widen(narrow(obj)) == obj;
      narrow(widen(tval)) == tval;
      widen(narrow(val)) == val;
      loc \in s == widen(loc) \in s;
      loc!s == narrow(eval(s, widen(loc)))

% @(#)$Id: contained_objects.lsl,v 1.3 1995/01/04 04:19:51 leavens Exp $
% Assumption about the sort of contained_objects
contained_objects(T): trait
  includes State
    contained_objects: T, St -> Set[Object]