### 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
introduces
emptyState, bottom: -> State
bind: State, Object, Value, Set[TYPE] -> State
allocated: Object, State -> Bool
isBottom: State -> Bool
eval: Object, State -> Value

asserts
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(emptyState);
isBottom(bottom);
isBottom(bind(st,obj,v,typs)) == isBottom(st);
bind(bottom,obj,v,typs) == bottom;

implies
\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)
introduces
types_of: Object, State -> Set[TYPE]
hasType: Object, State, TYPE -> Bool
asserts
\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);
implies
\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$

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

asserts
\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);

implies
\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
Set(Object, Set[Object], int for Int)   % from LSL handbook
introduces
domain: State -> Set[Object]
asserts
\forall obj:Object, st:State
obj \in domain(st) == allocated(obj, st);
implies
equations
domain(emptyState) == {};
converts domain