Overview  Package   Class  Use  Tree  Deprecated  Index  Help 
JML
 PREV CLASS   NEXT CLASS FRAMES    NO FRAMES    
SUMMARY: NESTED | FIELD | CONSTR | METHOD DETAIL: FIELD | CONSTR | METHOD

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

Class Specifications
private invariant this.checkingPart.greaterThanOrEqualTo(new org.jmlspecs.samples.prelimdesign.USMoney(0));
private invariant this.checkingPart.lessThanOrEqualTo(this.credit_);
public invariant this.savings != null&&this.checking != null;
public invariant_redundantly this.savings.plus(this.checking).greaterThanOrEqualTo(new org.jmlspecs.samples.prelimdesign.USMoney(0));
private represents savings <- this.credit_.minus(this.checkingPart);
private represents checking <- this.checkingPart;
public represents credit \such_that this.credit.equals(this.savings.plus(this.checking));

Specifications inherited from class Account
protected invariant this.accountOwner_ != null&&this.credit_ != null;
protected invariant_redundantly this.credit_.greaterThanOrEqualTo(new org.jmlspecs.samples.prelimdesign.USMoney(0));
public invariant this.accountOwner != null&&this.credit != null&&this.credit.greaterThanOrEqualTo(new org.jmlspecs.samples.prelimdesign.USMoney(0));
protected constraint_redundantly this.accountOwner_.equals(\old(this.accountOwner_));
public constraint this.accountOwner.equals(\old(this.accountOwner));
protected represents credit <- this.credit_;
protected represents accountOwner <- this.accountOwner_;

Specifications inherited from class Object
represents objectState <- org.jmlspecs.lang.JMLDataGroup.IT;
public represents _getClass <- \typeof(this);

Model Field Summary
 MoneyOps checking
           
 MoneyOps savings
           
 
Model fields inherited from class org.jmlspecs.samples.prelimdesign.Account
accountOwner, credit
 
Model fields inherited from class java.lang.Object
_getClass, objectState, theString
 
Ghost Field Summary
 
Ghost fields inherited from class java.lang.Object
objectTimesFinalized, owner
 
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)
           
 
Model Method Summary
 
Model methods inherited from class java.lang.Object
hashValue
 
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
 

Model Field Detail

savings

public MoneyOps savings
Specifications:
is in groups: credit
datagroup contains: checkingPart

checking

public MoneyOps checking
Specifications:
is in groups: credit
datagroup contains: checkingPart
Field Detail

checkingPart

private MoneyOps checkingPart
Specifications: non_null
is in groups: savings checking
Constructor Detail

PlusAccount

public PlusAccount(MoneyOps sav,
                   MoneyOps chk,
                   String own)
Specifications:
public normal_behavior
requires sav != null&&chk != null&&own != null&&(new org.jmlspecs.samples.prelimdesign.USMoney(1)).lessThanOrEqualTo(sav)&&(new org.jmlspecs.samples.prelimdesign.USMoney(1)).lessThanOrEqualTo(chk);
assignable credit, owner;
assignable_redundantly savings, checking;
ensures this.savings.equals(sav)&&this.checking.equals(chk)&&this.owner.equals(own);
ensures_redundantly this.credit.equals(sav.plus(chk));
Method Detail

payInterest

public void payInterest(double rate)
Overrides:
payInterest in class Account
Specifications:
     also
public normal_behavior
old boolean can_scale = this.credit.can_scaleBy(1.0+rate);
requires 0.0 <= rate&&rate <= 1.0&&can_scale;
assignable credit, savings, checking;
ensures this.checking.equals(\old(this.checking).scaleBy(1.0+rate));
    for_example
public normal_example
requires rate == 0.05&&this.checking.equals(new org.jmlspecs.samples.prelimdesign.USMoney(2000));
assignable credit, savings, checking;
ensures this.checking.equals(new org.jmlspecs.samples.prelimdesign.USMoney(2100));
Specifications inherited from overridden method payInterest(double rate) in class Account:
public normal_behavior
old boolean can_scale = this.credit.can_scaleBy(1.0+rate);
requires 0.0 <= rate&&rate <= 1.0&&can_scale;
assignable credit;
ensures this.credit.equals(\old(this.credit).scaleBy(1.0+rate));
    for_example
public normal_example
requires rate == 0.05&&(new org.jmlspecs.samples.prelimdesign.USMoney(4000)).equals(this.credit);
assignable credit;
ensures this.credit.equals(new org.jmlspecs.samples.prelimdesign.USMoney(4200));

withdraw

public void withdraw(MoneyOps amt)
Overrides:
withdraw in class Account
Specifications:
     also
public normal_behavior
requires amt != null&&(new org.jmlspecs.samples.prelimdesign.USMoney(0)).lessThanOrEqualTo(amt)&&amt.lessThanOrEqualTo(this.savings);
assignable credit, savings;
ensures this.savings.equals(\old(this.savings).minus(amt))&&\not_modified(checking);
     also
public normal_behavior
requires amt != null&&(new org.jmlspecs.samples.prelimdesign.USMoney(0)).lessThanOrEqualTo(amt)&&amt.lessThanOrEqualTo(this.credit)&&amt.greaterThan(this.savings);
assignable credit, savings, checking;
ensures this.savings.equals(new org.jmlspecs.samples.prelimdesign.USMoney(0))&&this.checking.equals(\old(this.checking).minus(amt.minus(this.savings)));
    for_example
public normal_example
requires this.savings.equals(new org.jmlspecs.samples.prelimdesign.USMoney(40001))&&amt.equals(new org.jmlspecs.samples.prelimdesign.USMoney(40000));
assignable credit, savings, checking;
ensures this.savings.equals(new org.jmlspecs.samples.prelimdesign.USMoney(1))&&\not_modified(checking);
       also
public normal_example
requires this.savings.equals(new org.jmlspecs.samples.prelimdesign.USMoney(30001))&&this.checking.equals(new org.jmlspecs.samples.prelimdesign.USMoney(10000))&&amt.equals(new org.jmlspecs.samples.prelimdesign.USMoney(40000));
assignable credit, savings, checking;
ensures this.savings.equals(new org.jmlspecs.samples.prelimdesign.USMoney(0))&&this.checking.equals(new org.jmlspecs.samples.prelimdesign.USMoney(1));
Specifications inherited from overridden method withdraw(MoneyOps amt) in class Account:
public normal_behavior
requires amt != null&&(new org.jmlspecs.samples.prelimdesign.USMoney(0)).lessThanOrEqualTo(amt)&&amt.lessThanOrEqualTo(this.credit);
assignable credit;
ensures this.credit.equals(\old(this.credit).minus(amt));
    for_example
public normal_example
requires this.credit.equals(new org.jmlspecs.samples.prelimdesign.USMoney(40001))&&amt.equals(new org.jmlspecs.samples.prelimdesign.USMoney(40000));
assignable credit;
ensures this.credit.equals(new org.jmlspecs.samples.prelimdesign.USMoney(1));

deposit

public void deposit(MoneyOps amt)
Overrides:
deposit in class Account
Specifications:
     also
public normal_behavior
old boolean can_add = this.credit.can_add(amt);
requires amt != null&&amt.greaterThanOrEqualTo(new org.jmlspecs.samples.prelimdesign.USMoney(0))&&can_add;
assignable credit, savings;
ensures this.savings.equals(\old(this.savings).plus(amt))&&\not_modified(checking);
    for_example
public normal_example
requires this.savings.equals(new org.jmlspecs.samples.prelimdesign.USMoney(20000))&&amt.equals(new org.jmlspecs.samples.prelimdesign.USMoney(1));
assignable credit, savings, checking;
ensures this.savings.equals(new org.jmlspecs.samples.prelimdesign.USMoney(20001));
Specifications inherited from overridden method deposit(MoneyOps amt) in class Account:
public normal_behavior
old boolean can_add = this.credit.can_add(amt);
requires amt != null&&amt.greaterThanOrEqualTo(new org.jmlspecs.samples.prelimdesign.USMoney(0))&&can_add;
assignable credit;
ensures this.credit.equals(\old(this.credit).plus(amt));
    for_example
public normal_example
requires this.credit.equals(new org.jmlspecs.samples.prelimdesign.USMoney(40000))&&amt.equals(new org.jmlspecs.samples.prelimdesign.USMoney(1));
assignable credit;
ensures this.credit.equals(new org.jmlspecs.samples.prelimdesign.USMoney(40001));

depositToChecking

public void depositToChecking(MoneyOps amt)
Specifications:
public normal_behavior
old boolean can_add = this.credit.can_add(amt);
requires amt != null&&amt.greaterThanOrEqualTo(new org.jmlspecs.samples.prelimdesign.USMoney(0))&&can_add;
assignable credit, checking;
ensures this.checking.equals(\old(this.checking).plus(amt))&&\not_modified(savings);
    for_example
public normal_example
requires this.checking.equals(new org.jmlspecs.samples.prelimdesign.USMoney(20000))&&amt.equals(new org.jmlspecs.samples.prelimdesign.USMoney(1));
assignable credit, checking;
ensures this.checking.equals(new org.jmlspecs.samples.prelimdesign.USMoney(20001));

payCheck

public void payCheck(MoneyOps amt)
Specifications:
public normal_behavior
requires amt != null;
{|
requires (new org.jmlspecs.samples.prelimdesign.USMoney(0)).lessThanOrEqualTo(amt)&&amt.lessThanOrEqualTo(this.checking);
assignable credit, checking;
ensures this.checking.equals(\old(this.checking).minus(amt))&&\not_modified(savings);
also
requires (new org.jmlspecs.samples.prelimdesign.USMoney(0)).lessThanOrEqualTo(amt)&&amt.lessThanOrEqualTo(this.credit)&&amt.greaterThan(this.checking);
assignable credit, checking, savings;
ensures this.checking.equals(new org.jmlspecs.samples.prelimdesign.USMoney(0))&&this.savings.equals(\old(this.savings).minus(amt.minus(this.checking)));
|}
    for_example
public normal_example
requires this.checking.equals(new org.jmlspecs.samples.prelimdesign.USMoney(40001))&&amt.equals(new org.jmlspecs.samples.prelimdesign.USMoney(40000));
assignable credit, checking;
ensures this.checking.equals(new org.jmlspecs.samples.prelimdesign.USMoney(1))&&\not_modified(savings);
       also
public normal_example
requires this.savings.equals(new org.jmlspecs.samples.prelimdesign.USMoney(30001))&&this.checking.equals(new org.jmlspecs.samples.prelimdesign.USMoney(10000))&&amt.equals(new org.jmlspecs.samples.prelimdesign.USMoney(40000));
assignable credit, checking, savings;
ensures this.checking.equals(new org.jmlspecs.samples.prelimdesign.USMoney(0))&&this.savings.equals(new org.jmlspecs.samples.prelimdesign.USMoney(1));

toString

public String toString()
Overrides:
toString in class Account
Specifications inherited from overridden method in class Account:
      --- None ---
Specifications inherited from overridden method in class Object:
       non_null
public normal_behavior
assignable objectState;
ensures \result != null&&\result .equals(this.theString);
ensures (* \result is a string representation of this object *);
     also
public code normal_behavior
assignable \nothing;
ensures \result != null&&(* \result is the instance's class name, followed by an @, followed by the instance's hashcode in hex *);
     also
public code model_program { ... }
    implies_that
assignable objectState;
ensures \result != null;
Overview  Package   Class  Use  Tree  Deprecated  Index  Help 
JML
 PREV CLASS   NEXT CLASS FRAMES    NO FRAMES    
SUMMARY: NESTED | FIELD | CONSTR | METHOD DETAIL: FIELD | CONSTR | METHOD
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.