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 $
State_Updates: trait
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
includes State_Basics, TypePerspectives, State_Updates,
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
Go to the first, previous, next, last section, table of contents.