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);
    int s = 0;
    for (i = 0; i < r.length; ++i) s+=r[i];
    //@ assert r.length == pubs.length;
    //@ assert s >= 0;
    int pc = 1;
    for (i = 0; i < pubs.length; ++i) if (r[i] != 0) ++pc;
    //@ assert pc > 0;
    return pubs.length == 0? 0 : s / pubs.length;
  }
}