Constant objects are modeled by sorts with names of the form
ConstObj[T],
which is the sort of a constant object containing
abstract values of sort T.
The trait ConstObj gives the formal model of constant objects.
See section 7.5 Contained Objects for the details of the trait contained_objects.
The trait function contained_objects
is defined so that constant objects work correctly with various
sugars for C++ structs.
% @(#)$Id: ConstObj.lsl,v 1.11 1995/11/08 04:17:38 leavens Exp $
ConstObj(T): trait
includes TypedObj(ConstObj, T), contained_objects(ConstObj[T])
assumes contained_objects(T)
asserts
\forall cobj: ConstObj[T], st: State
contained_objects(cobj, st)
== if assigned(cobj,st)
then contained_objects(eval(cobj,st), st)
else {};
implies
converts
contained_objects: ConstObj[T], State -> Set[TypeTaggedObject]
Go to the first, previous, next, last section, table of contents.