% @(#)$Id: MutableObj.lsl,v 1.13 1995/11/10 06:50:26 leavens Exp $
MutableObj(T): trait
  includes TypedObj(Obj, T), contained_objects(Obj[T])
  introduces 
    mutate: State, Obj[T], T -> State
  asserts
    \forall mobj: Obj[T], tval: T, st: State
      mutate(st, mobj, tval)
        == updateValue(st, widen(mobj), widen(injectTVal(tval)));
      contained_objects(mobj, st) == {asTypeTaggedObject(mobj)};
  implies
    \forall mobj: Obj[T], tval: T, st: State
      assigned(mobj, mutate(st, mobj, tval));
      eval(mobj, mutate(st, mobj, tval)) == tval;
    converts mutate, contained_objects

[Index]

HTML generated using lcpp2html.