/**
 * @invariants
 * balance >= 0 and balance < limit
 *
 * @preconditions
 * balance + amount < limit and amount >=0
 *
 * @postconditions
 * balance = balance@pre + amount
 *
 */
public class PayCard { 
    final int limit;
    int balance;
    int unsuccessfulOperations;
    
    public void charge(int amount) {
	if (this.balance + amount >= this.limit) {
	    this.unsuccessfulOperations++;
	} else {
	    this.balance = this.balance + amount;
	}
    }
}