% @(#) $Id: Array.lsl,v 1.38 1997/07/25 19:03:58 leavens Exp $ 
% Arrays as in C++, elements are some kind of object

Array(Loc, Elem): trait

  includes Val_Array(Loc[Elem]), Val_Array(Elem),
           ArrayAllocatedAuxFuns(Arr[Loc[Elem]]),
           ArrayAssignedAuxFuns(Arr[Loc[Elem]]),
           contained_objects(Arr[Loc[Elem]])

  assumes TypedObj(Loc, Elem), contained_objects(Loc[Elem])

  introduces
    allocated, assigned: Arr[Loc[Elem]], int, State -> Bool
    allocated, assigned: Arr[Loc[Elem]], State -> Bool
    eval: Arr[Loc[Elem]], State -> Arr[Elem]
    contained_without_indexes: Arr[Loc[Elem]], State, Set[int]
                               -> Set[TypeTaggedObject]
    objectsInRange: Arr[Loc[Elem]], int, int -> Set[TypeTaggedObject]
    objectsInRangeHelper: Arr[Loc[Elem]], Set[int] -> Set[TypeTaggedObject]
    objectsUpTo: Arr[Loc[Elem]], int -> Set[TypeTaggedObject]

  asserts
    \forall a: Arr[Loc[Elem]], i,j,k,n,siz: int, e: Loc[Elem], st: State,
            si: Set[int]
      allocated(a, i, st) == allocated(a,i) /\ allocated(a[i], st);
      assigned(a, i, st) == allocated(a,i) /\ assigned(a[i], st);
      allocated(a, st) == allAllocated(a,st);
      assigned(a, st) == allAssigned(a,st);

      eval(create(i),st) == create(i);
      eval(assign(a,i,e),st) == assign(eval(a,st), i, eval(e,st));

      contained_objects(a, st)
        == contained_without_indexes(a, st, {}:Set[int]);
      contained_without_indexes(create(i), st, si) == {};
      contained_without_indexes(assign(a,i,e), st, si)
        == if i \in si then contained_without_indexes(a, st, si)
           else {asTypeTaggedObject(e)}
                \U contained_without_indexes(a, st, insert(i, si));

      objectsInRange(a, i, j) == objectsInRangeHelper(slice(a,i,j), {});
      objectsInRangeHelper(create(k), si) == {};
      objectsInRangeHelper(assign(a,k,e), si)
        == if k \in si then objectsInRangeHelper(a, si)
           else {asTypeTaggedObject(e)}
                \U objectsInRangeHelper(a, insert(k, si));

      objectsUpTo(a, siz) == objectsInRange(a, 0, siz-1);

  implies
    \forall a: Arr[Loc[Elem]], i: int, e: Loc[Elem], st: State
      size(contained_objects(a, st)) <= (maxIndex(a) + 1);
      asTypeTaggedObject(e) \in contained_objects(assign(a,i,e), st);
    converts
      allocated: Arr[Loc[Elem]], int, State -> Bool,
      assigned: Arr[Loc[Elem]], int, State -> Bool,
      contained_objects: Arr[Loc[Elem]], State -> Set[TypeTaggedObject],
      objectsInRange, objectsInRangeHelper, objectsUpTo

[Index]

HTML generated using lcpp2html.