% @(#)$Id: BoundedStackPrivateTrait.lsl,v 1.1 1998/08/27 14:57:04 leavens Exp $
BoundedStackPrivateTrait: trait
  assumes StackTrait(Elem for E, BoundedStack[Elem] for C),
          Val_Array(Elem)
  introduces
    toStack: Arr[Elem], int -> BoundedStack[Elem]
  asserts
    \forall elems_val: Arr[Elem], current_top: int
      toStack(elems_val, current_top)
        == if (current_top < 0)
           then empty
           else push(elems_val[current_top],
                     toStack(elems_val, current_top - 1));

[Index]

HTML generated using lcpp2html.