% @(#)$Id: PrePointer.lsl,v 1.7 1995/06/20 22:49:38 leavens Exp $
% Model of pointers as index into an array.
% This follows the idea in LCL [page 60, Guttag-Horning93].

PrePointer(Elem): trait

  assumes Val_Array(Elem), int

  % This would be
  %   "Ptr[Elem] tuple of idx: int, locs: Arr[Elem]"
  % but don't want set_locs, "generated by" and "partitioned by" clauses

  introduces
    [__, __] : int, Arr[Elem] -> Ptr[Elem]
    &__ : Elem -> Ptr[Elem]                  % use if not in an array
    address_of : Arr[Elem], int -> Ptr[Elem] % use if in an array
    __.idx: Ptr[Elem] -> int
    __.locs: Ptr[Elem] -> Arr[Elem]
    locs: Ptr[Elem] -> Arr[Elem]
    index: Ptr[Elem] -> int
    set_idx: Ptr[Elem], int -> Ptr[Elem]
    __ + __: Ptr[Elem], int -> Ptr[Elem]
    __ - __: Ptr[Elem], int -> Ptr[Elem]
    __<__, __<=__, __>=__, __>__: Ptr[Elem], Ptr[Elem] -> Bool

  asserts \forall p: Ptr[Elem], i,j: int, a,a1: Arr[Elem],
                  st: State, l: Elem
    &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[Elem]), IsPO(>=, Ptr[Elem])

[Index]

HTML generated using lcpp2html.