% @(#)$Id: PointerAllocatedAuxFuns.lsl,v 1.2 1995/07/26 04:26:19 leavens Exp $

PointerAllocatedAuxFuns(PtrT): trait
  assumes PointerAllocAuxSig(PtrT)
  includes ArrayAllocatedAuxFuns(PtrT)
  introduces
    allocated: PtrT, State -> Bool
  asserts
    \forall p: PtrT, st: State
      allocated(p, st) == allocated(p, 0, st);
  implies
   converts
      allocated: PtrT, State -> Bool

[Index]

HTML generated using lcpp2html.