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


2.8.1 Formal Model of Objects

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.