% @(#)$Id: TypedObjEval.lsl,v 1.3 1995/11/10 06:35:44 leavens Exp $
TypedObjEval(Loc, T): trait
  assumes State, WithUnassigned(T), WidenNarrow(Loc[T], Object),
           WidenNarrow(WithUnassigned[T], Value)
  introduces
    eval: Loc[T], State -> T
  asserts
    \forall loc: Loc[T], st: State
      eval(loc, st) == extractTVal(narrow(eval(widen(loc), st)));
  implies
    converts
      eval: Loc[T], State -> T
        exempting \forall loc: Loc[T], st: State, typs: Set[TYPE]
          eval(loc, bottom), eval(loc, emptyState),
          eval(loc, bind(st, widen(loc), widen(unassigned), typs))

[Index]

HTML generated using lcpp2html.