class IntStack
{
  /*@ non_null @*/ int[] stack;
  int number; 
  /*@ invariant 0 <= number && number <= stack.length; @*/

  final int N = 10;

  /*@ ensures isempty() && stack.length == N; @*/
  IntStack() 
  { 
    stack = new int[N]; 
    number = 0; 
  }

  /*@ ensures \result <==> number == 0; @*/
  /*@ pure @*/ boolean isempty()
  { 
    return number == 0; 
  }

  /*@ requires true;
    @ assignable stack, stack[*], number;
    @ ensures number == \old(number)+1
    @      && stack[number-1] == e
    @      && (\forall int i; 0 <= i && i < number-1; 
    @           stack[i] == \old(stack[i]));
    @*/
  void push(int e) 
  { 
    if (number == stack.length) 
      resize();
    stack[number] = e;
    number = number+1;
  }

  /*@ requires !isempty(); 
    @ assignable number;
    @ ensures \result == stack[number] &&
    @         number == \old(number)-1;
    @*/
  int pop(int e)
  {
    number = number-1;
    return stack[number];
  }

  /*@ requires true;
    @ assignable stack;
    @ ensures  \fresh(stack) && 
    @          stack.length > \old(stack.length) &&
    @          (\forall int i; 0 <= i && i < number; 
    @             stack[i] == \old(stack[i]));
    @*/
  void resize()
  {
     int s[] = new int[2*stack.length+1];
     for (int i=0; i<stack.length; i++) 
       s[i] = stack[i];
     stack = s;
  }
}