Package account
Class AccountImplDebitGDbC
java.lang.Object
account.AccountImplDebitGDbC
@Invariant("this.balance >= 0.0")
public class AccountImplDebitGDbC
extends java.lang.Object
-
Constructor Summary
Constructors Constructor Description AccountImplDebitGDbC(double amount, java.lang.String owner, int min)
-
Method Summary
Modifier and Type Method Description double
balance()
boolean
containsTA(Transaction t)
void
credit(double amount)
void
debit(double amount, java.time.LocalDate date)
void
debit2(double amount, java.time.LocalDate date)
void
debitOrg(int amount)
java.lang.String
getHolder()
boolean
invariant()
int
overdraft()
void
setHolder(java.lang.String newHolder)
Methods inherited from class java.lang.Object
equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
-
Constructor Details
-
AccountImplDebitGDbC
public AccountImplDebitGDbC(double amount, java.lang.String owner, int min)
-
-
Method Details
-
balance
public double balance() -
containsTA
-
credit
public void credit(double amount) -
debitOrg
public void debitOrg(int amount) -
debit2
public void debit2(double amount, java.time.LocalDate date) -
debit
@Requires("amount >= 0.0 && isFunded(amount)") @Ensures("balance == old(balance) - amount && transactions.contains(tr)") public void debit(double amount, java.time.LocalDate date) -
getHolder
public java.lang.String getHolder() -
setHolder
public void setHolder(java.lang.String newHolder) -
overdraft
public int overdraft() -
invariant
public boolean invariant()
-