JML

org.jmlspecs.samples.prelimdesign
Class PlusAccount

java.lang.Object
  extended byorg.jmlspecs.samples.prelimdesign.Account
      extended byorg.jmlspecs.samples.prelimdesign.PlusAccount

public class PlusAccount
extends Account


Field Summary
private  MoneyOps checkingPart
           
 
Fields inherited from class org.jmlspecs.samples.prelimdesign.Account
accountOwner_, credit_
 
Constructor Summary
PlusAccount(MoneyOps sav, MoneyOps chk, String own)
           
 
Method Summary
 void deposit(MoneyOps amt)
           
 void depositToChecking(MoneyOps amt)
           
 void payCheck(MoneyOps amt)
           
 void payInterest(double rate)
           
 String toString()
           
 void withdraw(MoneyOps amt)
           
 
Methods inherited from class org.jmlspecs.samples.prelimdesign.Account
balance
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
 

Field Detail

checkingPart

private MoneyOps checkingPart
Constructor Detail

PlusAccount

public PlusAccount(MoneyOps sav,
                   MoneyOps chk,
                   String own)
Method Detail

payInterest

public void payInterest(double rate)
Overrides:
payInterest in class Account

withdraw

public void withdraw(MoneyOps amt)
Overrides:
withdraw in class Account

deposit

public void deposit(MoneyOps amt)
Overrides:
deposit in class Account

depositToChecking

public void depositToChecking(MoneyOps amt)

payCheck

public void payCheck(MoneyOps amt)

toString

public String toString()
Overrides:
toString in class Account

JML

JML is Copyright (C) 1998-2002 by Iowa State University and is distributed under the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This release depends on code from the MultiJava project and is based in part on the Kopi project Copyright (C) 1990-99 DMS Decision Management Systems Ges.m.b.H.