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

  private int beer;

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


  public int getBeer(int x) {
    return Math.min(beer, x);
  }
}

public class Ex {
  //@ requires \nonnullelements(pubs);
  public int drink(Pub[] pubs) {
    int r = 0;
    for (int i = 0; i < pubs.length; ++i)
      r += pubs[i].getBeer(i+1);
    return r;
  }
}