module stack
{
  const n : integer;
  type stack_t = record { top : integer; arr : array [0..n-1] of integer; };

  var s : stack_t;

  procedure push(x : integer)
    modifies s;
  {
    assume(s.top < n);
    s.arr[s.top] := x;
    s.top := s.top + 1;
  }

  procedure pop()
    modifies s;
  {
    assume(s.top > 0);
    s.top := s.top - 1;
  }

  function top() : integer
  {
    assume(s.top > 0);
    return s.arr[s.top-1];
  }

  init {
    s.top := 0;
  }

  next {
    call push(top());
    call pop();
  }
}
