Uses of Interface
org.jmlspecs.samples.prelimdesign.MoneyOps

Packages that use MoneyOps

org.jmlspecs.samples.prelimdesign

This package contains samples of JML specifications from the paper Preliminary Design of JML.

Uses of MoneyOps in org.jmlspecs.samples.prelimdesign

Classes in org.jmlspecs.samples.prelimdesign that implement MoneyOps

class

USMoney

Fields in org.jmlspecs.samples.prelimdesign declared as MoneyOps

protected MoneyOps	Account.credit_
private MoneyOps	Account_JML_Test.TestAccount.amt Argument amt
private MoneyOps	Account_JML_Test.TestDeposit.amt Argument amt
private MoneyOps	Account_JML_Test.TestWithdraw.amt Argument amt
private MoneyOps	PlusAccount.checkingPart
private MoneyOps	PlusAccount_JML_Test.TestPlusAccount.sav Argument sav
private MoneyOps	PlusAccount_JML_Test.TestPlusAccount.chk Argument chk
private MoneyOps	PlusAccount_JML_Test.TestWithdraw.amt Argument amt
private MoneyOps	PlusAccount_JML_Test.TestDeposit.amt Argument amt
private MoneyOps	PlusAccount_JML_Test.TestDepositToChecking.amt Argument amt
private MoneyOps	PlusAccount_JML_Test.TestPayCheck.amt Argument amt

Methods in org.jmlspecs.samples.prelimdesign that return MoneyOps

MoneyOps	Account.balance()
abstract MoneyOps	MoneyOps.plus(Money m2)
abstract MoneyOps	MoneyOps.minus(Money m2)
abstract MoneyOps	MoneyOps.scaleBy(double factor)
MoneyOps	USMoney.plus(Money m2)
MoneyOps	USMoney.minus(Money m2)
MoneyOps	USMoney.scaleBy(double factor)

Methods in org.jmlspecs.samples.prelimdesign with parameters of type MoneyOps

void	Account.deposit(MoneyOps amt)
void	Account.withdraw(MoneyOps amt)
void	PlusAccount.withdraw(MoneyOps amt)
void	PlusAccount.deposit(MoneyOps amt)
void	PlusAccount.depositToChecking(MoneyOps amt)
void	PlusAccount.payCheck(MoneyOps amt)

Constructors in org.jmlspecs.samples.prelimdesign with parameters of type MoneyOps

Account(MoneyOps amt, String own)

Account_JML_Test.TestAccount(MoneyOps amt, String own)
Initialize this instance.

Account_JML_Test.TestDeposit(Account receiver$, MoneyOps amt)
Initialize this instance.

Account_JML_Test.TestWithdraw(Account receiver$, MoneyOps amt)
Initialize this instance.

PlusAccount(MoneyOps sav, MoneyOps chk, String own)

PlusAccount_JML_Test.TestPlusAccount(MoneyOps sav, MoneyOps chk, String own)
Initialize this instance.

PlusAccount_JML_Test.TestWithdraw(PlusAccount receiver$, MoneyOps amt)
Initialize this instance.

PlusAccount_JML_Test.TestDeposit(PlusAccount receiver$, MoneyOps amt)
Initialize this instance.

PlusAccount_JML_Test.TestDepositToChecking(PlusAccount receiver$, MoneyOps amt)
Initialize this instance.

PlusAccount_JML_Test.TestPayCheck(PlusAccount receiver$, MoneyOps amt)
Initialize this instance.