% @(#) $Id: Val_Array.lsl,v 1.17 1995/08/11 21:38:30 leavens Exp $ 
% Mappings from integers to values (pre-arrays) with 0-based indexes

Val_Array(Elem): trait

  includes int, % trait for C++ built-in type int.
           Set(int, Set[int], int for Int)

  introduces
    create: int -> Arr[Elem]
    allocated, allocatedUpTo: Arr[Elem], int -> Bool
    allAllocated: Arr[Elem] -> Bool
    allocatedInRange: Arr[Elem], int, int -> Bool
    assign: Arr[Elem], int, Elem -> Arr[Elem]
    __[__]: Arr[Elem], int -> Elem
    maxIndex, minIndex: Arr[Elem] -> int
    legalIndex: Arr[Elem], int -> Bool
    size: Arr[Elem] -> int
    slice: Arr[Elem], int, int -> Arr[Elem]
    slice_helper: Arr[Elem], int, int, Arr[Elem], Set[int] -> Arr[Elem]

  asserts
    sort Arr[Elem] generated by create, assign
    sort Arr[Elem] partitioned by size, allocated, __[__]

    \forall a: Arr[Elem], i,j,n,siz: int, e: Elem
      ~allocated(create(n), j);
      allocated(assign(a,i,e), j)
        == legalIndex(a,j) /\ (i = j \/ allocated(a, j));
      allAllocated(a) == allocatedInRange(a, 0, maxIndex(a)); 
      allocatedInRange(a, i, j)
        == i > j \/ (allocated(a, i) /\ allocatedInRange(a, i+1, j));
      allocatedUpTo(a, siz) == allocatedInRange(a, 0, siz-1);
      assign(a,i,e)[j] == (if i = j then e else a[j]);
      maxIndex(assign(a,i,e)) == maxIndex(a);
      maxIndex(create(n)) == n - 1;
      minIndex(a) == 0;
      legalIndex(a,i) == (0 <= i) /\ (i <= maxIndex(a));
      size(create(n)) = n;
      size(assign(a,i,e)) = size(a);

    \forall a, a2: Arr[Elem], i, j, k: int, s: Set[int], e: Elem
      slice(a,i,j)
        == if i <= j then slice_helper(a, i, j, create(j-i), {})
           else create(0);
      slice_helper(create(k), i, j, a2, s) == a2;
      slice_helper(assign(a,k,e), i, j, a2, s)
        == if i <= k /\ k <= j /\ ~(k \in s)
           then slice_helper(a, i, j, assign(a2,k,e), insert(k, s))
           else slice_helper(a, i, j, a2, s);

  implies
    sort Arr[Elem] partitioned by maxIndex, allocated, __[__]
    \forall a: Arr[Elem], i, j: int, e1, e2: Elem
      assign(assign(a,i,e1),i,e2) == assign(a,i,e2);
      i ~= j => assign(assign(a,i,e1),j,e2) = assign(assign(a,j,e2),i,e1);
      allocated(a,i) => legalIndex(a,i);
      size(a) == maxIndex(a) + 1;
      j < 0 => (slice(a, i, j) = create(0));
    converts allocated: Arr[Elem], int -> Bool,
             allAllocated, allocatedInRange,
             maxIndex, minIndex, legalIndex, size: Arr[Elem] -> int,
             __[__]
      exempting \forall n, i: int
        create(n)[i]

[Index]

HTML generated using lcpp2html.