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.