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

      public boolean containsTA​(Transaction t)
    • 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()