% @(#)$Id: TrashesSemantics.lsl,v 1.2 1995/11/13 15:34:50 leavens Exp $

TrashesSemantics: trait
  assumes  State, AllocatedAssigned(Loc, T)

  introduces 
    isTrashed:  Loc[T], State, State -> Bool

  asserts
    \forall loc: Loc[T], pre,post: State
      isTrashed(loc, pre, post)
        == (assigned(loc, pre) /\ ~assigned(loc, post))
           \/ (allocated(loc, pre) /\ ~allocated(loc, post));

  implies
    \forall loc: Loc[T], pre,post: State
      isTrashed(loc, pre, post)
         => (allocated(loc, pre)
              /\ (~allocated(loc, post) \/ ~assigned(loc, post)));
      isTrashed(loc, pre, post) => ~assigned(loc, post);
      ~isTrashed(loc, pre, post)
        == (~assigned(loc, pre) \/ assigned(loc, post))
           /\ (~allocated(loc, pre) \/ allocated(loc, post));
      (~isTrashed(loc, pre, post) /\ assigned(loc, pre))
         => assigned(loc, post);
      (~isTrashed(loc, pre, post) /\ allocated(loc, pre))
         => allocated(loc, post);
    converts isTrashed
      exempting \forall loc: Loc[T], st: State
        isTrashed(loc,bottom,st), isTrashed(loc,st,bottom)

[Index]

HTML generated using lcpp2html.