package esercizio0;

public class Account {

	private/*@ spec_public*/int balance;

	public Account() {
		balance = 100;
	}

	// precondizioni
	// post: il bilancio viene aggiornato correttamente
	public void preleva(int qta) {
		balance -= qta;
	}

	//@requires qta>0;
	//@ensures balance==\old(balance)+qta;
	public void deposita(int qta) {
		balance += qta;
	}

}
//@ code_bigint_math