% @(#)$Id: cpp_char_string.lsl,v 1.25 1995/11/06 16:02:59 leavens Exp $
% Compare Guttag and Horning's book (Springer-Verlag, 1994), page 64

cpp_char_string: trait

  includes int, char, TypedObj(Obj, char),
           Pointer(Obj, char),
           String(char, String[char], int for Int)

  introduces
    null: -> char
    nullTerminated: Ptr[Obj[char]], State -> Bool
    nullTerminated: Arr[Obj[char]], State -> Bool
    throughNull: Ptr[Obj[char]], State -> String[char]
    throughNull: Arr[Obj[char]], State -> String[char]
    uptoNull: Ptr[Obj[char]], State -> String[char]
    uptoNull: Arr[Obj[char]], State -> String[char]
    sameCharsThroughNull: Ptr[Obj[char]], State, Ptr[Obj[char]], State -> Bool
    sameCharsThroughNull: Arr[Obj[char]], State, Ptr[Obj[char]], State -> Bool
    sameCharsThroughNull: Ptr[Obj[char]], State, Arr[Obj[char]], State -> Bool
    sameCharsThroughNull: Arr[Obj[char]], State, Arr[Obj[char]], State -> Bool
    lengthToNull: Ptr[Obj[char]], State -> int
    lengthToNull: Arr[Obj[char]], State -> int
    objectsToNull: Ptr[Obj[char]], State -> Set[Object]
    objectsToNull: Arr[Obj[char]], State -> Set[Object]
    legalStringIndex: Ptr[Obj[char]], State, int -> Bool
    legalStringIndex: Arr[Obj[char]], State, int -> Bool

  asserts
    \forall p, p1, p2: Ptr[Obj[char]], st, st1, st2: State, i: int,
            a, a1, a2: Arr[Obj[char]]
      null == 0;

      nullTerminated(p, st) ==
        assigned(p,st) /\ (eval(*p,st) = null \/ nullTerminated(p+1,st));
      nullTerminated(a, st) == nullTerminated(address_of(a,0), st);

      nullTerminated(p, st)
        => (throughNull(p, st)
             = (if eval(*p,st) = null then {null}
                else eval(*p,st) \precat throughNull(p+1,st)));
      throughNull(a, st) == throughNull(address_of(a,0), st);

      nullTerminated(p, st)
        => (uptoNull(p, st)
             = (if eval(*p,st) = null then empty
                else eval(*p,st) \precat uptoNull(p+1,st)));
      uptoNull(a, st) == uptoNull(address_of(a,0), st);

      (nullTerminated(p1, st1) /\ nullTerminated(p2, st2))
        => (sameCharsThroughNull(p1, st1, p2, st2) =
             (throughNull(p1,st1) = throughNull(p2,st2)));
      sameCharsThroughNull(a1, st1, p2, st2) ==
        sameCharsThroughNull(address_of(a1,0), st1, p2, st2);
      sameCharsThroughNull(p1, st1, a2, st2) ==
        sameCharsThroughNull(p1, st1, address_of(a2,0), st2);
      sameCharsThroughNull(a1, st1, a2, st2) ==
        sameCharsThroughNull(address_of(a1,0), st1, address_of(a2,0), st2);

      nullTerminated(p, st)
        => (lengthToNull(p, st) = len(throughNull(p,st)) - 1);
      lengthToNull(a, st) == lengthToNull(address_of(a,0), st);

      nullTerminated(p, st)
        => (objectsToNull(p,st) = (if eval(*p,st) = null then {widen(*p)}
                                 else {widen(*p)} \U objectsToNull(p+1,st)));
      objectsToNull(a, st) == objectsToNull(address_of(a,0), st);

      nullTerminated(p, st)
        => (legalStringIndex(p, st, i) = (0 <= i /\ i < lengthToNull(p,st)));
      legalStringIndex(a, st, i) == legalStringIndex(address_of(a,0), st, i);

  implies converts null, nullTerminated: Ptr[Obj[char]], State -> Bool,
                   nullTerminated: Arr[Obj[char]], State -> Bool

[Index]

HTML generated using lcpp2html.