public class ATM {
	private int cash;
	private int cashDispensed;
	
	public ATM(int cash) {
		this.cash = cash;
	}
	
	public static void main(String[] args) {
		ATM atm = new ATM(-10000);
		
		Client client = new Client(20);
		
		System.out.println("Cash available in ATM: " + atm.cash 
				+ " dollars.  Client has: $" + client.getAmountCash());
		
		atm.withdraw(50, client);
		
		System.out.println("Cash available in ATM: " + atm.cash 
				+ " dollars.  Client has: $" + client.getAmountCash());
	}
	
	// Pre-condition, Post-condition: cash >= 0.
	// Invariant: cash + cashDispensed
	public boolean withdraw(int amount, Client client) {
		assert cash >= 0;
		
		int total = cash + cashDispensed;
		
		if (cash >= amount) {
			cash -= amount;
			client.addCash(amount);
			cashDispensed += amount;
			
			assert cash + cashDispensed == total;
			assert cash >= 0;
			
			return true;
		}
		
		return false;
	}
}

class Client {
	private int cash;
	
	public Client(int cash) {
		this.cash = cash;
	}
	
	public int getAmountCash() {
		return cash;
	}
	
	public void addCash(int cashToAdd) {
		cash += cashToAdd;
	}
	
	public void spendCash(int cashToSubtract) {
		cash += cashToSubtract;
	}
}