module Stack {
  var i: integer;
  var s: [integer]integer;

  procedure step()
    modifies i;
    modifies s;
  {
    i = (i - 1);
    if (i >= 0) {
      s = s[i -> 0];
    }
    i = (i - 1);
    if (i >= 0) {
      s = s[(i + 1) -> s[i]];
    }
  }

  next {
    call step();
  }
}
