accountadt.java

国外的数据结构与算法分析用书

/**	A simple bank account interface with preconditions, postconditions, and the
	invariant in the comments. */
public interface AccountADT
{
	/**	The name of the owner. */
	String owner();

	/**	The current balance in the account. */
	float balance();

	/**	The current line of credit for the account. */
	float lineOfCredit();

	/**	Deposit an amount in the account.
		PRECONDITION:
			amount >= 0
		POSTCONDITION:
			balance() == entry(balance()) + amount
			owner() == entry(owner())
			lineOfCredit() == entry(lineOfCredit()) */
	void deposit(float amount);

	/**	Withdraw an amount from the account.
		PRECONDITION:
			amount >= 0 
			amount <= balance() + lineOfCredit() 
		POSTCONDITION:
			balance() == entry(balance()) - amount
			owner() == entry(owner())
			lineOfCredit() == entry(lineOfCredit()) */
	void withdraw(float amount);

	/**	Change approved line of credit for the account.
		PRECONDITION:
			amount >= 0 
			balance() >= -amount 
		POSTCONDITION:
			balance() == entry(balance())
			owner() == entry(owner())
			lineOfCredit() == amount */
	void changeLOC(float amount);

/** INVARIANT:
	lineOfCredit() >= 0
	balance() >= -lineOfCredit() */
}