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

2.8.2 Formal Model of States

States (sort State) can be thought of as finite mapping from untyped objects (sort Object) to untyped values (sort Value) and sets of types (sort Set[TYPE]). The trait State_Basics gives the basic operators on states used by Larch/C++. The state bottom represents the state that results from a nonterminating computation or error. The state emptyState is the empty finite mapping. The trait function bind adds a mapping from an object to a value, overriding any previous mapping for that object. The trait function eval gives the value associated with an object by a state.

% @(#)$Id: State_Basics.lsl,v 1.11 1997/02/13 00:21:15 leavens Exp $
% The sort State is the sort of C++ states, which this formalizes.
% This is adapted from traits used by GIL [Chen89] and GCIL [Lerner91].
% Hua Zhong helped revise and improve this trait, and proved its implications.

State_Basics: trait
    emptyState, bottom: -> State
    bind: State, Object, Value, Set[TYPE] -> State
    allocated: Object, State -> Bool
    isBottom: State -> Bool
    eval: Object, State -> Value

    State generated by emptyState, bottom, bind
    State partitioned by allocated, eval, isBottom
    \forall obj,obj1: Object, st: State, v: Value, typs: Set[TYPE]
      ~allocated(obj, emptyState);
      ~allocated(obj, bottom);
      allocated(obj, bind(st, obj1, v, typs))
         == ~isBottom(st) /\ ((obj = obj1) \/ allocated(obj, st));
      ~isBottom(st) =>
        (eval(obj1, bind(st,obj,v,typs))
          = (if obj1 = obj 
                then v 
                else eval(obj1, st)));
      isBottom(bind(st,obj,v,typs)) == isBottom(st);
      bind(bottom,obj,v,typs) == bottom;

    \forall obj, obj1:Object, st:State, v,v1: Value,
            typs,typs1: Set[TYPE]
      emptyState ~= bottom;
      isBottom(st) == (st = bottom);
      ~isBottom(st) => (bind(st,obj,v,typs) ~= bottom);
      ~isBottom(st) => 
          (eval(obj1, bind(st, obj1, v, typs)) = v);
      ~isBottom(st) =>
        (eval(obj1, bind(st,obj,v,typs))
          = (if obj1 = obj 
              then eval(obj1, bind(emptyState, obj1, v, typs))
              else eval(obj1, st)));
      ~isBottom(st) =>
        (allocated(obj1, bind(st,obj,v,typs))
          = (if obj1 = obj 
              then allocated(obj1, bind(emptyState, obj1, v, typs))
              else allocated(obj1, st)));
      bind(bind(st, obj, v, typs), obj, v1, typs1)
        == bind(st, obj, v1, typs1);
      bind(bind(st,obj,v,typs), obj1, v1, typs1)
        == if obj1 = obj 
              then bind(st, obj1, v1, typs1)
              else bind(bind(st,obj1,v1,typs1), obj, v, typs);
    converts allocated, eval, isBottom
      exempting \forall obj:Object
        eval(obj,bottom), eval(obj,emptyState)

For each allocated object, a state associates with it a set of types. This set records the names of the sorts to which the object can be sensibly narrowed, using the trait function narrow. Another way to look at this is that each untyped object can be viewed from a limited number of typed perspectives from a C++ program (in a given state). One can imagine the compiler recording this information for each object, potentially updating this information when new aliases are developed to the object with different type perspectives. See section 6.2.2 Allocated and Assigned for one way this information is used. The formal model of this information is specified by the trait TypePerspectives below. An object that is not allocated has no type perspectives.

% @(#)$Id: TypePerspectives.lsl,v 1.10 1996/11/15 12:30:46 leavens Exp $
% What a state knows about the "types" an object may have
% This trait was corrected and proved by Hua Zhong.
TypePerspectives: trait
  assumes State_Basics
  includes Set(TYPE, Set[TYPE], int for Int)
    types_of: Object, State -> Set[TYPE]
    hasType: Object, State, TYPE -> Bool
    \forall obj, obj1: Object, t: TYPE, typs: Set[TYPE],
            v: Value, st: State
      types_of(obj, emptyState) == {};
      types_of(obj, bottom) == {};
      ~isBottom(st) =>
         types_of(obj, bind(st, obj1, v, typs)) 
          = (if (obj=obj1) then typs 
                           else types_of(obj,st));
      hasType(obj, st, t) == t \in types_of(obj, st);
    \forall obj, obj1: Object, t: TYPE, v: Value, st: State
      ~allocated(obj, st) => (types_of(obj, st) = {});
    converts types_of, hasType

An untyped object may have its value and type perspectives updated independently. For example, in mutation of a typed object, loc, the type perspectives recorded for the underlying untyped object, widen(loc), do not change. The trait State_Updates specifies these updates.

% @(#)$Id: State_Updates.lsl,v 1.4 1997/02/13 00:21:17 leavens Exp $
State_Updates: trait

  assumes State_Basics, TypePerspectives
    updateValue: State, Object, Value -> State
    updateTypes: State, Object, Set[TYPE] -> State

    \forall obj, obj1: Object, typs, typs1: Set[TYPE],
            v, v1: Value, st: State
    updateValue(emptyState, obj1, v1) == emptyState;
    updateValue(bottom, obj1, v1) == bottom;
    updateValue(bind(st, obj, v, typs), obj1, v1)
      == if obj = obj1 then bind(st, obj, v1, typs)
                       else bind(updateValue(st, obj1, v1), obj, v, typs);
    updateTypes(emptyState, obj1, typs1) == emptyState;
    updateTypes(bottom, obj1, typs1) == bottom;
    updateTypes(bind(st, obj, v, typs), obj1, typs1)
      == if obj = obj1 then bind(st, obj, v, typs1)
                       else bind(updateTypes(st, obj1, typs1), obj, v, typs);

    \forall obj: Object, typs: Set[TYPE], v: Value, st: State
      ~allocated(obj, st) => \A v (updateValue(st, obj, v) = st);
      ~allocated(obj, st) => \A v (updateTypes(st, obj, typs) = st);
    converts updateValue, updateTypes

The trait State below has the complete model of states for Larch/C++. It includes State_Basics and the other traits defined above.

% @(#)$Id: State.lsl,v 1.23 1997/02/13 00:21:14 leavens Exp $

State: trait
  includes State_Basics, TypePerspectives, State_Updates,
           Set(Object, Set[Object], int for Int)   % from LSL handbook
    domain: State -> Set[Object]
    \forall obj:Object, st:State
      obj \in domain(st) == allocated(obj, st);
      domain(emptyState) == {};
    converts domain

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