% @(#)$Id: ModifiesSemantics.lsl,v 1.16 1995/11/13 15:38:59 leavens Exp $
% This is based on Chalin's help and his work [Chalin95].
ModifiesSemantics(Loc, T): trait
  assumes  State, AllocatedAssigned(Loc, T), TypedObjEval(Loc, T)

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

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

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

[Index]

HTML generated using lcpp2html.