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

[Index]

HTML generated using lcpp2html.