/**
   * @invariants
   * balance >= 0 and balance < limit
   */
  public class PayCard { 
      final int limit;
      int balance;

      public void charge(int amount) {}
  }