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

[Index]

HTML generated using lcpp2html.