[Prev][Next][Index]
Re: specification of destructive operation
Pierre-Yves,
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
result.
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
introduces
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
introduces
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]
asserts
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);
~isBottom(empty);
~isBottom(bind(s,obj,v));
isBottom(bottom);
~(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;
implies
converts __ \in __:Object,St -> Bool,
eval, isBottom, added, modified, objs
exempting forall obj:Object, s:St
obj \in bottom,
eval(bottom,obj),
eval(empty,obj),
added(bottom,s), added(s,bottom),
modified(bottom,s), modified(s,bottom),
objs(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
introduces
widen: Loc[T] -> Object
widen: T -> Value
narrow: Object -> Loc[T]
narrow: Value -> T
__ \in __: Loc[T], St -> Bool
__ ! __: Loc[T], St -> T
asserts
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
introduces
contained_objects: T, St -> Set[Object]