% @(#)$Id: U_Pre_Trait.lsl,v 1.2 1997/07/31 21:14:14 leavens Exp $

% Improved in response to a criticism of Chalin's [Chalin95]

U_Pre_Trait(U, Loc, Val): trait

  assumes int, Pointer(Obj, char),
          TypedObj(Loc, int), TypedObj(Loc, Ptr[Obj[char]]),
          contained_objects(Loc[int]), contained_objects(Loc[Ptr[Obj[char]]])
         
  includes NoContainedObjects(Val),
           contained_objects(U)

  U union of i_var: Loc[int], char_p: Loc[Ptr[Obj[char]]]
  Val union of i_var: int, char_p: Ptr[Obj[char]]

  introduces
    eval: U, State -> Val
    allocated, assigned: U, State -> Bool

  asserts
    \forall st: State, u: U, s: Loc[Ptr[Obj[char]]], i: Loc[int]

       % both tags share the same untyped object
       widen(i_var(i).char_p) == widen(i_var(i).i_var);
       widen(char_p(s).i_var) == widen(char_p(s).char_p);

       % a union with a given tag contains the object tagged with each sort
       contained_objects(i_var(i), st)
         == {asTypeTaggedObject(i)}
            \U {asTypeTaggedObject(narrow(widen(i)):Loc[Ptr[Obj[char]]])};
       contained_objects(char_p(s), st)
         == {asTypeTaggedObject(s)}
            \U {asTypeTaggedObject(narrow(widen(s)):Loc[int])};

       eval(i_var(i), st) == i_var(eval(i, st));
       eval(char_p(s), st) == char_p(eval(s, st));

       allocated(i_var(i), st) == allocated(i, st);
       allocated(char_p(s), st) == allocated(s, st);
       assigned(i_var(i), st) == assigned(i, st);
       assigned(char_p(s), st) == assigned(s, st);

    implies
       converts
         eval: U, State -> Val,
         allocated: U, State -> Bool, assigned: U, State -> Bool

[Index]

HTML generated using lcpp2html.