Go to the first, previous, next, last section, table of contents.


2.8.1.1 Formal Model of Mutable Objects

Mutable objects are modeled by sorts with names of the form Obj[T], which is the sort of an object containing abstract values of sort T. The trait MutableObj gives the formal model of mutable objects by adding the capability of mutation to the trait TypedObj. (See section 2.8.2 Formal Model of States for the definition of updateValue for untyped objects.) Having the trait function contained_objects defined for mutable objects is useful in specifying template container classes (see section 8 Template Specifications). In any case, all sorts of values must have the trait function contained_objects defined, and objects are considered to be values in Larch/C++, so such a definition is necessary. See section 7.5 Contained Objects for more details on contained objects.

% @(#)$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


Go to the first, previous, next, last section, table of contents.