% @(#)$Id: ArrayAllocatedAuxFuns.lsl,v 1.4 1995/08/24 21:30:19 leavens Exp $

ArrayAllocatedAuxFuns(T): trait
  assumes int, State, ArrayAllocAuxSig(T)
  introduces
    allAllocated: T, State -> Bool
    allocatedInRange: T, int, int, State -> Bool
    allocatedUpTo: T, int, State -> Bool
  asserts
    \forall p: T, i,j,siz: int, st: State
      allAllocated(p, st)
        == allocatedInRange(p, minIndex(p), maxIndex(p), st);
      allocatedInRange(p, i, j, st)
        == i > j \/ (allocated(p, i, st) /\ allocatedInRange(p, i+1, j, st));
      allocatedUpTo(p, siz, st) == allocatedInRange(p, 0, siz-1, st); 
  implies
   converts
      allAllocated: T, State -> Bool,
      allocatedInRange: T, int, int, State -> Bool,
      allocatedUpTo: T, int, State -> Bool

[Index]

HTML generated using lcpp2html.