% @(#) $Id: MultiDimensionalArray.lsl,v 1.27 1999/01/12 22:40:17 leavens Exp $
% Supplement for higher dimensions of an array in C++

MultiDimensionalArray(SubObjArr, SubValArr): trait

  assumes State, SubArray(SubObjArr, SubValArr)

  includes Val_Array(SubObjArr), Val_Array(SubValArr),
           NoContainedObjects(Arr[SubValArr]),
           ArrayAllocatedAuxFuns(Arr[SubObjArr]),
           ArrayAssignedAuxFuns(Arr[SubObjArr]),
           contained_objects(Arr[SubObjArr])

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

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

      eval(create(n): Arr[SubValArr], st) == create(n);
      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) : Arr[SubObjArr], st, si) == {};
      contained_without_indexes(assign(a,i,e), st, si)
        == if i \in si then contained_without_indexes(a, st, si)
           else contained_objects(e, st)
                \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 objectsInRange(a[k], 0, maxIndex(a[k]))
                \U objectsInRangeHelper(a, insert(k, si));

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

  implies
    \forall a: Arr[SubObjArr], st: State
      size(contained_objects(a, st)) <= (maxIndex(a) + 1);
    converts
      allocated: Arr[SubObjArr], int, State -> Bool,
      assigned: Arr[SubObjArr], int, State -> Bool,
      contained_objects: Arr[SubObjArr], State -> Set[TypeTaggedObject],
      objectsInRange: Arr[SubObjArr], int, int -> Set[TypeTaggedObject],
      objectsUpTo: Arr[SubObjArr], int -> Set[TypeTaggedObject]

[Index]

HTML generated using lcpp2html.