class Pub {
  //@ invariant beer >= 0;

  private int beer;

  //@ requires beer >= 0;
  public Pub(int beer) { this.beer = beer; }


  //@ requires x >= 0;
  //@ ensures \result >= 0;
  public int getBeer(int x) {
    int r = Math.min(beer, x);
    beer -= r;
    return r;
  }
}

public class Ex {
  //@ requires \nonnullelements(pubs);
  //@ ensures \result >= 0;
  public int drink(Pub[] pubs) {
    int[] r = new int[pubs.length];
    int i;
    for (i = 0; i < pubs.length; ++i)
      r[i] = pubs[i].getBeer(i+1);
    for (i = pubs.length - 1; i >= 0 && r[i] != 0; --i);
    System.out.println("99 bottles of beer on the wall");
    //@ assert (\forall int i; 0 <= i && i < pubs.length ==> r[i] >= 0);
    return i + 1;
  }
}