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.