[Prev][Next][Index]
Re: specification of destructive operation
Arnd,
Below is how you can specify your example in Larch/C++.
I changed the interface slightly, because I didn't want to deal with
structs for listelem, as in Larch/C++ they have annoyingly complex
abstract values (on purpose).
I don't think it's possible to specify what you want in LCL,
because the LCL model of pointers is not detailed enough;
but the LCL folk can correct me if I'm wrong about this.
Note that, in regard to Jim's comment, I haven't tried
to prove stuff from such specifications, and so there may be details
wrong, and/or it may be difficult to do such proofs.
(That is, I haven't thought about whether stating the traits in different
ways would ease the proofs.) Also it's clear to me that when I get
around to adding the LCL claims clause to Larch/C++, that would be very
useful in specifications like this.
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
P.S. I had to make a couple of fixes in Larch/C++ to parse this (:-)
and I had to update a trait to specify this easily; so if you get Larch/C++
or the manual close to the time this is sent, it may not work on this spec.
But it will, and that's a benefit of doing such an exercise.
Here's the Larch/C++ spec...
// @(#)$Id: intlist.lcc,v 1.1 1995/01/13 19:52:52 leavens Exp $
imports pretend_bool;
class listelem {
uses ListElemTrait;
public:
listelem(int val = 0, listelem * next = 0) {
constructs self;
ensures self' = [val, next];
}
};
typedef listelem * list; // implicitly uses Pointer(Obj, listelem);
list empty() {
ensures result = NULL;
}
bool isempty( list l ) {
requires isLegal(l);
ensures result = to_bool(isNull(l));
}
bool equal( list l1, list l2 ) {
// I'm guessing that you don't want LISP's eq, but equality of values.
uses ToListTrait;
requires not(circular(l1, pre) \/ circular(l2, pre));
ensures result = to_bool(toList(l1,pre) = toList(l2,pre));
}
int top( list l ) {
requires isValid(l); // which means l is not NULL
ensures result = (*l)^.car;
}
list rest( list l ) {
requires isValid(l);
ensures result = (*l)^.cdr;
}
list append( int i, list l ) {
requires isLegal(l);
ensures fresh(result) /\ (*result)' = [i,l];
}
list copy( list l ) {
uses ToListTrait;
requires isLegal(l);
ensures fresh(reach(result))
/\ toList(l,pre) = toList(result,post);
}
list conc( list l1, list l2 ) {
uses ToListTrait;
requires isNull(l1);
ensures result = l2;
requires isValid(l1) /\ not(circular(l1, pre));
modifies last_elem(l1, pre));
ensures result = l1 /\ last_elem(l1, post)'.cdr = l2;
}
... end of intlist.lcc
A note about the last function spec. The spec of conc is done
with a very handy syntactic sugar. This kind of case analysis is
equivalent to the following desugared spec.
list conc( list l1, list l2 ) {
uses ToListTrait;
requires isNull(l1) \/ (isValid(l1) /\ not(circular(l1, pre)));
modifies last_elem(l1, pre));
ensures (isNull(l1) => result = l2) and unchanged(all);
/\ (isValid(l1) /\ not(circular(l1, pre))
=> result = l1 /\ last_elem(l1, post)'.cdr = l2);
}
Here are the traits used above...
% @(#)$Id: ListElemTrait.lsl,v 1.1 1995/01/13 19:52:52 leavens Exp $
ListElemTrait: trait
assumes MutableObj(listelem), Pointer(Obj, listelem) % Larch/C++ traits
listelem tuple of car: int, cdr: Ptr[Obj[listelem]]
introduces
contained_objects: listelem, St -> Set[Object]
asserts \forall i: int, p: Ptr[Obj[listelem]], st: St
contained_objects([i,p], st) == contained_objects(p, st)
% @(#)$Id: ToListTrait.lsl,v 1.2 1995/01/13 20:08:34 leavens Exp $
ToListTrait: trait
includes ListElemTrait, List(int, List[int], int for Int),
Set(Obj[listelem], Set[Obj[listelem]], int for Int)
introduces
circular: Ptr[Obj[listelem]], St -> Bool
circular2: Ptr[Obj[listelem]], St, Set[Obj[listelem]] -> Bool
toList: Ptr[Obj[listelem]], St -> List[int]
last_elem: Ptr[Obj[listelem]], St -> Obj[listelem]
asserts \forall i: int, p: Ptr[Obj[listelem]], st: St, so: Set[Obj[listelem]]
isLegal(p) => (circular(p,st) = circular2(p, st, {}));
circular2(NULL, st, so) == false;
isValid(p) => (circular2(p, st, so)
= ((*p) \in so)
\/ circular2(((*p)!st).cdr, st, so \U {*p}));
toList(NULL, st) == empty;
(isValid(p) /\ not(circular(p, st)))
=> (toList(p, st) = {((*p)!st).car} || toList(((*p)!st).cdr, st));
(isValid(p) /\ not(circular(p, st)))
=> (last_elem(p, st) = (if ((*p)!st).cdr = NULL then *p
else last_elem(((*p)!st).cdr, st)))
% @(#)$Id: Pointer.lsl,v 1.15 1995/01/13 17:55:55 leavens Exp $
% Pointers, with the possibility of the null pointer and invalid pointers.
Pointer(Loc, Val): trait
includes Array(Loc, Val),
PrePointer(Loc, Val)
assumes TypedObj(Loc, Val)
introduces
NULL: -> Ptr[Loc[Val]]
isNull: Ptr[Loc[Val]] -> Bool
notNull: Ptr[Loc[Val]] -> Bool
minIndex: Ptr[Loc[Val]] -> int
maxIndex: Ptr[Loc[Val]] -> int
legalIndex: Ptr[Loc[Val]], int -> Bool
isLegal, isValid: Ptr[Loc[Val]] -> Bool
* __: Ptr[Loc[Val]] -> Loc[Val]
contained_objects: Ptr[Loc[Val]], St -> Set[Object]
asserts
sort Ptr[Loc[Val]] generated by NULL, [__,__]
sort Ptr[Loc[Val]] partitioned by isNull, .idx, .locs
\forall p: Ptr[Loc[Val]], i: int, st: St
isNull(p) == (p = NULL);
notNull(p) == ~(p = NULL);
notNull(p) => (minIndex(p) = -(p.idx));
notNull(p) => (maxIndex(p) = maxIndex(p.locs) - p.idx);
legalIndex(p,i) == if isNull(p) then false
else ((minIndex(p) <= i) /\ (i <= maxIndex(p)));
isLegal(p) == isNull(p) \/ legalIndex(p,p.idx);
isValid(p) == notNull(p) /\ legalIndex(p,p.idx);
isValid(p) => (*p = p.locs[p.idx]);
legalIndex(p,i) => (widen(*(p + i)) \in contained_objects(p, st));
size(contained_objects(p, st)) <= (maxIndex(p.locs) + 1)
implies \forall p: Ptr[Loc[Val]], st: St
notNull(p) => (minIndex(p) + maxIndex(p) = maxIndex(p.locs));
contained_objects(NULL, st) == {};
isValid(p) == notNull(p) /\ isLegal(p)
converts .idx, .locs, locs, index,
minIndex, maxIndex: Ptr[Loc[Val]] -> int,
legalIndex: Ptr[Loc[Val]], int -> Bool,
isValid, *: Ptr[Loc[Val]] -> Loc[Val]
exempting NULL.idx, NULL.locs, locs(NULL),
index(NULL), minIndex(NULL), maxIndex(NULL), *NULL
% @(#)$Id: PrePointer.lsl,v 1.4 1995/01/04 03:03:52 leavens Exp $
% Model of pointers as index into an array.
% This follows the idea in LCL [page 60, Guttag-Horning93].
PrePointer(Loc, Val): trait
assumes Val_Array(Loc[Val]), int
% This would be
% "Ptr[Loc[Val]] tuple of idx: int, locs: Arr[Loc[Val]]"
% but don't want set_locs, "generated by" and "partitioned by" clauses
introduces
[__, __] : int, Arr[Loc[Val]] -> Ptr[Loc[Val]]
&__ : Loc[Val] -> Ptr[Loc[Val]] % use if not in an array
address_of : Arr[Loc[Val]], int -> Ptr[Loc[Val]] % use if in an array
__.idx: Ptr[Loc[Val]] -> int
__.locs: Ptr[Loc[Val]] -> Arr[Loc[Val]]
locs: Ptr[Loc[Val]] -> Arr[Loc[Val]]
index: Ptr[Loc[Val]] -> int
set_idx: Ptr[Loc[Val]], int -> Ptr[Loc[Val]]
__ + __: Ptr[Loc[Val]], int -> Ptr[Loc[Val]]
__ - __: Ptr[Loc[Val]], int -> Ptr[Loc[Val]]
__<__, __<=__, __>=__, __>__: Ptr[Loc[Val]], Ptr[Loc[Val]] -> Bool
asserts \forall p: Ptr[Loc[Val]], i,j: int, a,a1: Arr[Loc[Val]],
st: St, l: Loc[Val]
&l == [0,assign(create(1), 0, l)];
address_of(a,i) == [i,a];
([i,a] = [j,a1]) == (i = j) /\ (a = a1);
([i,a]).idx == i;
([i,a]).locs == a;
locs(p) == p.locs;
index(p) == p.idx;
set_idx([i,a], j) == [j,a];
p + i == set_idx(p, p.idx + i);
p - i == set_idx(p, p.idx - i);
([i,a] < [j,a]) == (i < j);
([i,a] > [j,a]) == (i > j);
([i,a] <= [j,a]) == (i <= j);
([i,a] >= [j,a]) == (i >= j);
implies IsPO(<=, Ptr[Loc[Val]]), IsPO(>=, Ptr[Loc[Val]])
Other traits can be found in the standard LSL handbook or in the Larch/C++
release.
Follow-Up(s):
Reference(s):