% @(#)$Id: ArrayIterateProc.lsl,v 1.2 1995/12/24 22:25:22 leavens Exp $
% Iteration of state changes for elements of an array
ArrayIterateProc(Loc, Elem): trait
  assumes SideEffectsFun(Elem)
  includes Array(Loc, Elem)
  introduces
    isIteratedStateFor: Arr[Loc[Elem]], int, int, State, State -> Bool
  asserts \forall a: Arr[Loc[Elem]], i,ub: int, pre,next,post: State
    (i >= ub)
      => isIteratedStateFor(a, i, ub, pre, pre);
    ((i < ub)
        /\ isStateFor(eval(a, pre)[i], pre, next)
        /\ isIteratedStateFor(a, i+1, ub, next, post))
      => isIteratedStateFor(a, i, ub, pre, post);

[Index]

HTML generated using lcpp2html.