% @(#)$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)

[Index]

HTML generated using lcpp2html.