Objects in Larch/C++ are modeled using several traits.
The main trait is `TypedObj`

, which
handles the translation between typed objects and values
and the untyped objects and values used in the trait `State`

(see section 2.8.2 Formal Model of States).
This model builds on the work of Wing [Wing87], Chen [Chen89],
Lerner [Lerner91], and most recently has benefited discussions
with Chalin and his work [Chalin95].

The formal model of this trait (and its relation to
the sorts in the trait `State`

)
may be explained with the help of the
following (crudely-drawn) picture.
This picture shows a sort `T`

of abstract values,
with a representative element, `tval`

.
The trait function `injectTVal`

maps this into the sort
`WithUnassigned[T]`

, a sort that also includes the special
value `unassigned`

.
The trait function `extractTVal`

is its (near) inverse.
The sort `Loc[T]`

of typed objects containing `T`

values
(or `unassigned`

) has `loc`

as a typical element.
The sorts `WithUnassigned[T]`

and `Loc[T]`

in the trait `TypedObj`

are the typed counterparts of
the sorts `Value`

and `Object`

in the trait `State`

.
The overloaded trait functions named `widen`

map typed to untyped
values and objects.
Their inverses are the trait functions named `narrow`

.
In each trait, the `eval`

mapping takes a second argument
which is a state, written as `st`

in the picture.

trait TypedObj trait State Loc[T] Object !---------------! widen !-----------------------! ! ! --------------> ! ! ! loc ! ! widen(loc) ! ! ! narrow ! ! ! ! <-------------- ! ! !---------------! !-----------------------! / ! / | / | / | / eval(__, st) | eval(__, st) / | / | / | / ! / ! T v WithUnassigned[T] v Value !--------! injectTVal !------------! widen !-----------------------! ! ! -----------> ! ! --------> ! ! ! tval ! !injectTVal( ! !widen(injectTVal(tval))! ! ! extractTVal ! tval)! narrow ! ! ! ! <----------- ! ! <-------- ! ! !--------! ! - - - - - -! ! ! ! unassigned ! ! widen(unassigned) ! !------------! !-----------------------! A picture of the sorts in the traits TypedObj and State, and some of the mappings between them. The second argument to eval is a state, st.

The `TypedObj`

trait itself includes several other traits,
and uses them to define the sort `Loc[T]`

.
The included traits will be explained individually below.

% @(#)$Id: TypedObj.lsl,v 1.29 1997/02/13 00:21:23 leavens Exp $ TypedObj(Loc, T): trait includes State, WithUnassigned(T), WidenNarrow(Loc[T], Object), WidenNarrow(WithUnassigned[T], Value), TypedObjEval(Loc, T), AllocatedAssigned(Loc, T), ModifiesSemantics(Loc, T), FreshSemantics(Loc, T), TrashesSemantics asserts sort Loc[T] generated by narrow sort Loc[T] partitioned by widen

The conversions to and from typed and untyped versions
of objects and values are defined by the two inclusions of the trait
`WidenNarrow`

given below.

% @(#)$Id: WidenNarrow.lsl,v 1.3 1997/02/13 00:21:25 leavens Exp $ % Maps between untyped and typed values. % This could be used to describe any partially inverse pair of mappings. WidenNarrow(Typed, Untyped): trait introduces widen: Typed -> Untyped narrow: Untyped -> Typed asserts \forall t: Typed narrow(widen(t)) == t; implies \forall u: Untyped narrow(widen(narrow(u))) == narrow(u);

The sort `WithUnassigned[T]`

is specified by the following trait.
(Those who are familiar with denotational semantics
[Schmidt86] will recognize
this as the "lift" of `T`

, with `unassigned`

used
in place of the usual notation for a bottom element.
The mappings `injectTVal`

and `extractTVal`

are
explicit conversions to and from this lifted set.)

% @(#)$Id: WithUnassigned.lsl,v 1.1 1995/11/06 05:12:17 leavens Exp $ WithUnassigned(T): trait introduces injectTVal: T -> WithUnassigned[T] extractTVal: WithUnassigned[T] -> T unassigned: -> WithUnassigned[T] isUnassigned: WithUnassigned[T] -> Bool asserts sort WithUnassigned[T] generated by injectTVal, unassigned sort WithUnassigned[T] partitioned by isUnassigned, extractTVal \forall tval: T extractTVal(injectTVal(tval)) == tval; ~isUnassigned(injectTVal(tval)); isUnassigned(unassigned); implies \forall tval: T injectTVal(extractTVal(injectTVal(tval))) == injectTVal(tval); converts isUnassigned, extractTVal exempting extractTVal(unassigned)

The trait `TypedObjEval`

is defined below.
Evaluation is, as in the picture above, defined by widening the typed object
to an untyped object, using the untyped `eval`

to get the untyped
object's value, and narrowing that value to a `WithUnassigned[T]`

value,
then extracting that to a value of type T.

% @(#)$Id: TypedObjEval.lsl,v 1.3 1995/11/10 06:35:44 leavens Exp $ TypedObjEval(Loc, T): trait assumes State, WithUnassigned(T), WidenNarrow(Loc[T], Object), WidenNarrow(WithUnassigned[T], Value) introduces eval: Loc[T], State -> T asserts \forall loc: Loc[T], st: State eval(loc, st) == extractTVal(narrow(eval(widen(loc), st))); implies converts eval: Loc[T], State -> T exempting \forall loc: Loc[T], st: State, typs: Set[TYPE] eval(loc, bottom), eval(loc, emptyState), eval(loc, bind(st, widen(loc), widen(unassigned), typs))

The trait `AllocatedAssigned`

defines notions of when a typed object is allocated in a state,
and when it is assigned a well-defined value (i.e., is not unassigned).
See section 6.2.2 Allocated and Assigned for details.

The trait `ModifiesSemantics`

defines
trait functions that help give a semantics to the Larch/C++
modifies clause.
See section 6.2.3 The Modifies Clause for details.

The trait `FreshSemantics`

defines
trait functions that help in giving the semantics
of the Larch/C++ built-in `lcpp-primary` `fresh`

.
See section 6.3.1 Fresh for details.

The trait `TrashesSemantics`

defines
trait functions that help in giving the semantics
of the Larch/C++ `trashes-clause`.
See section 6.3.2 The Trashes Clause for details.

Objects in Larch/C++ come in two flavors, mutable and constant (immutable).
Mutable objects include global variables and reference parameters.
Constant objects include global variables declared using
the C++ `cv-qualifier` `const`

.

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