% @(#)$Id: AllocatedAssigned.lsl,v 1.7 1995/11/10 07:42:11 leavens Exp $
AllocatedAssigned(Loc, T): trait
  assumes State, WithUnassigned(T), WidenNarrow(Loc[T], Object),
          WidenNarrow(WithUnassigned[T], Value)
  includes SortNames(Loc[T], TYPE, type_of for sort_of)
  introduces
    allocated, assigned: Loc[T], State -> Bool

  asserts
    \forall loc: Loc[T], st: State
      allocated(loc, st)
         == allocated(widen(loc), st)
            /\ type_of(loc) \in types_of(widen(loc), st);
      assigned(loc, st)
         == allocated(loc, st)
            /\ narrow(eval(widen(loc), st)) ~= unassigned;

  implies
    \forall loc: Loc[T], st: State
      allocated(loc, st) => widen(loc) \in domain(st);
      assigned(loc, st) => allocated(loc, st);
    converts
      assigned, allocated: Loc[T], State -> Bool

[Index]

HTML generated using lcpp2html.