% @(#) $Id: Person_Pre_Trait.lsl,v 1.1 1997/07/31 17:25:51 leavens Exp $

% This trait would be automatically constructed by Larch/C++

Person_Pre_Trait(Person, Loc, Val): trait

  assumes AbstractStringTrait, int, cpp_member_function,
          TypedObj(Loc, String[char]), TypedObj(Loc, int),
          ConstObj(cpp_member_function),
          contained_objects(Loc[String[char]]), contained_objects(Loc[int])

  includes NoContainedObjects(Val), contained_objects(Person)

  Person tuple of age: Loc[int], name: Loc[String[char]],
                  destructor: ConstObj[cpp_member_function],
                  Change_Name: ConstObj[cpp_member_function],
                  Name: ConstObj[cpp_member_function],
                  Make_Year_Older: ConstObj[cpp_member_function],
                  Years_Old: ConstObj[cpp_member_function]

  Val tuple of age: int, name: String[char], 
                  destructor: cpp_member_function,
                  Change_Name: cpp_member_function,
                  Name: cpp_member_function,
                  Make_Year_Older: cpp_member_function,
                  Years_Old: cpp_member_function

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

  asserts
    \forall per: Person, oi: Loc[int], os: Loc[String[char]], 
            odestroy, och_nm, onm, omyo, oyo: ConstObj[cpp_member_function],
            st: State

       contained_objects([oi,os,odestroy,och_nm,onm,omyo,oyo], st)
         == {asTypeTaggedObject(oi)} \U {asTypeTaggedObject(os)}
            \U {asTypeTaggedObject(odestroy)} \U {asTypeTaggedObject(och_nm)}
            \U {asTypeTaggedObject(onm)} \U {asTypeTaggedObject(omyo)}
            \U {asTypeTaggedObject(oyo)};

       eval(per,st)
         == [eval(per.age, st), eval(per.name, st),
             eval(per.destructor, st),  eval(per.Change_Name, st),
             eval(per.Name, st), eval(per.Make_Year_Older, st),
             eval(per.Years_Old, st)];

       allocated(per,st)
         == allocated(per.age, st) /\ allocated(per.name, st)
          /\ allocated(per.destructor, st) /\ allocated(per.Change_Name, st)
          /\ allocated(per.Name, st) /\ allocated(per.Make_Year_Older, st)
          /\ allocated(per.Years_Old, st);

       assigned(per,st)
         == assigned(per.age, st) /\ assigned(per.name, st)
          /\ assigned(per.destructor, st) /\ assigned(per.Change_Name, st)
          /\ assigned(per.Name, st) /\ assigned(per.Make_Year_Older, st)
          /\ assigned(per.Years_Old, st);

  implies
    converts
      contained_objects: Person, State -> Set[TypeTaggedObject],
      eval: Person, State -> Val,
      allocated: Person, State -> Bool, assigned: Person, State -> Bool

[Index]

HTML generated using lcpp2html.