% @(#)$Id: FreshSemantics.lsl,v 1.10 1995/11/13 22:20:37 leavens Exp $

FreshSemantics(Loc, T): trait
  assumes AllocatedAssigned(Loc, T)
  introduces 
    isFresh: Loc[T], State, State -> Bool
  asserts
    \forall loc: Loc[T], pre, post: State
      isFresh(loc, pre, post)
        == ~allocated(loc, pre) /\ allocated(loc, post);
  implies
    converts isFresh
      exempting \forall loc: Loc[T], st:State
        isFresh(loc, bottom, st), isFresh(loc, st, bottom)

[Index]

HTML generated using lcpp2html.