Design-by-Contract (DbC) Readings: OOSC2 Chapter 11
EECS3311 A: Software Design Winter 2020
CHEN-WEI WANG
What This Course Is About
for your design suffices.
● Focus is design
○ Architecture: (many) inter-related modules
○ Specification: precise (functional) interface of each module
● For this course, having a prototypical, working implementation
● A later refinement into more efficient data structures and algorithms is beyond the scope of this course.
[ assumed from EECS2011, EECS3101 ] ∴ Having a suitable language for design matters the most.
Q: Is Java also a “good” design language?
A: Let’s first understand what a “good” design is.
3 of 61
Motivation: Catching Defects – When?
● To minimize , minimize software defects.
● Software Development Cycle:
Requirements → Design → Implementation → Release Q. Design or Implementation Phase?
Catch defects as early as possible .
∵ The cost of fixing defects increases exponentially as software
progresses through the development lifecycle.
● Discovering defects after release costs up to 30 times more
than catching them in the design phase.
● Choice of design language for your project is therefore of
paramount importance.
Source:
Minimizing code defects to improve software quality and lower development costs.
2 of 61
development costs
Terminology: Contract, Client, Supplier
●A ●A
implements/provides a service (e.g., microwave).
supplier
○
uses a service provided by some supplier.
The client is required to follow certain instructions to obtain the service (e.g., supplier that client powers on, closes door, and heats something that is not explosive).
If instructions are followed, the client would that the service does what is guaranteed (e.g., a lunch box is heated). The client does not care how the supplier implements it.
○
client
assumes
○
● What then are the benefits and obligations os the two parties?
benefits obligations CLIENT follow instructions SUPPLIER assume instructions followed provide a service
obtain a service
expect
● There is a contract between two parties, violated if:
○ The instructions are not followed. [ Client’s fault ]
○ Instructions followed, but service not satisfactory. [ Supplier’s fault ] 4 of 61
Client, Supplier, Contract in OOP (1)
class MicrowaveUser {
public static void main(…) {
Microwave m = new Microwave(); Object obj = ;
m.power(); m.lock();]
m.heat(obj); }}
class Microwave {
private boolean on;
private boolean locked;
void power() {on = true;} void lock() {locked = true;} void heat(Object stuff) {
/* Assume: on && locked */
/* stuff not explosive. */
}}
Method call m.heat(obj) indicates a client-supplier relation.
○ Client: resident class of the method call [ MicrowaveUser ]
○ Supplier: type of context object (or call target) m [ Microwave ] 5 of 61
???
What is a Good Design?
● A “good” design should explicitly and unambiguously describe the contract between clients (e.g., users of Java classes) and suppliers (e.g., developers of Java classes).
We call such a contractual relation a specification .
● When you conduct software design, you should be guided by the “appropriate” contracts between users and developers.
○ Instructions to clients should not be unreasonable.
e.g., asking them to assemble internal parts of a microwave
○ Working conditions for suppliers should not be unconditional. e.g., expecting them to produce a microwave which can safely heat an explosive with its door open!
○ You as a designer should strike proper balance between obligations and benefits of clients and suppliers.
e.g., What is the obligation of a binary-search user (also benefit of a
binary-search implementer)? [ The input array is sorted. ] ○ Upon contract violation, there should be the fault of only one side.
○ This design process is called Design by Contract (DbC) . 7 of 61
Client, Supplier, Contract in OOP (2)
class Microwave {
private boolean on;
private boolean locked;
void power() {on = true;} void lock() {locked = true;} void heat(Object stuff) {
class {
public static void main(…) {
Microwave m = new Microwave(); Object obj = ;
m.power(); m.lock();
m.heat(obj); ● The is honoured if:
/* Assume: on && locked */
/* stuff not explosive. */ } }} }
contract
:
● Stateofmisasassumed:m.on==trueandm.locked==ture
● Theinputargumentobjisvalid(i.e.,notexplosive).
: obj is properly heated.
● If any of these fails, there is a contract violation.
● m.onorm.lockedisfalse ⇒MicrowaveUser’sfault. ● objisanexplosive ⇒MicrowaveUser’sfault.
A fault from the client is identified ⇒ Method call will not start. 6 of 61 ● Method executed but obj not properly heated ⇒ Microwave’s fault
MicrowaveUser
???
Right before the method call
Right after the method call
A Simple Problem: Bank Accounts
Provide an object-oriented solution to the following problem:
: Each account is associated with the name of its owner (e.g., “Jim”) and an integer balance that is always positive.
: We may withdraw an integer amount from an account.
: Each bank stores a list of accounts.
: Given a bank, we may add a new account in it.
: Given a bank, we may query about the associated account of a owner (e.g., the account of “Jim”).
: Given a bank, we may withdraw from a specific account, identified by its name, for an integer amount.
Let’s first try to work on and in Java.
This may not be as easy as you might think!
REQ1
REQ2
REQ3
REQ4
REQ5
REQ6
REQ1
REQ2
8 of 61
Playing the Various Versions in Java
● Download the project archive (a zip file) here:
● Follow this tutorial to learn how to import an project archive
into your workspace in Eclipse:
● Follow this tutorial to learn how to enable assertions in Eclipse:
9 of 61
http://www.eecs.yorku.ca/ ̃jackie/teaching/
lectures/2020/W/EECS3311/codes/DbCIntro.zip
Version 1: Why Not a Good Design? (1)
public class {
public static void main(String[] args) {
System.out.println(“Create an account for Alan with balance -10:”); AccountV1 alan = new AccountV1(“Alan”, -10) ;
System.out.println(alan);
Console Output:
Create an account for Alan with balance -10:
Alan’s current balance is: -10
● Executing AccountV1’s constructor results in an account object whose state (i.e., values of attributes) is invalid (i.e., Alan’s balance is negative). ⇒ Violation of
● Unfortunately, both client and supplier are to be blamed: BankAppV1 passed an invalid balance, but the API of AccountV1 does not require that! ⇒ A lack of defined contract
REQ1
11 of 61
BankAppV1
Version 1: An Account Class
1 2 3 4 5 6 7 8 9
10
11
12
13
14
15
● Is this a good design? Recall : Each account is associated with . . . an integer balance that is always positive .
REQ1
● This requirement is not reflected in the above Java code. 10 of 61
public class AccountV1 { private String owner;
private int balance;
public String getOwner() { return owner; } public int getBalance() { return balance; } public AccountV1(String owner, int balance) {
this.owner = owner; this.balance = balance; public void withdraw(int amount) {
this.balance = this.balance – amount;
}
public String toString() {
} }
}
return owner + “’s current balance is: ” + balance;
Version 1: Why Not a Good Design? (2)
public class {
public static void main(String[] args) {
System.out.println(“Create an account for Mark with balance 100:”); AccountV1 mark = new AccountV1(“Mark”, 100);
System.out.println(mark);
System.out.println(“Withdraw -1000000 from Mark’s account:”); mark. withdraw(-1000000) ;
System.out.println(mark);
Create an account for Mark with balance 100:
Mark’s current balance is: 100
Withdraw -1000000 from Mark’s account:
Mark’s current balance is: 1000100
● Mark’s account state is always valid (i.e., 100 and 1000100). ● Withdraw amount is never negative! ⇒ Violation of
● Again a lack of contract between BankAppV1 and AccountV1. 12 of 61
REQ2
BankAppV1
Version 1: Why Not a Good Design? (3)
public class {
public static void main(String[] args) {
System.out.println(“Create an account for Tom with balance 100:”); AccountV1 tom = new AccountV1(“Tom”, 100);
System.out.println(tom);
System.out.println(“Withdraw 150 from Tom’s account:”); tom. withdraw(150) ;
System.out.println(tom);
● Withdrawal was done via an “appropriate” reduction, but the resulting balance of Tom is invalid. ⇒ Violation of
● Again a lack of contract between BankAppV1 and AccountV1. 13 of 61
Create an account for Tom with balance 100:
Tom’s current balance is: 100
Withdraw 150 from Tom’s account:
Tom’s current balance is: -50
REQ1
BankAppV1
Version 1: How Should We Improve it? (2)
● The best we can do in Java is to encode the logical negations of preconditions as exceptions:
○ divide(int x, int y)
throws DivisionByZeroException when y == 0.
○ binSearch(int x, int[] xs)
throws ArrayNotSortedException when xs is not sorted.
○ topoSort(Graph g)
throws NotDAGException when g is not directed and acyclic.
● Design your method by specifying the preconditions (i.e., service conditions for valid inputs) it requires, not the exceptions (i.e., error conditions for invalid inputs) for it to fail.
● Create by adding exceptional conditions (an of preconditions) to the constructor and
withdraw method of the Account class. 15 of 61
Version 2
approximation
Version 1: How Should We Improve it? (1)
Preconditions of a method specify the precise circumstances under which that method can be executed.
14 of 61
○ Precond. of divide(int x, int y)?
○ Precond. of binSearch(int x, int[] xs)? ○ Precond. of topoSort(Graph g)?
[ y != 0 ] [ xs is sorted ] [ g is a DAG ]
Version 2: Added Exceptions
to Approximate Method Preconditions
1 public class AccountV2 {
2 public AccountV2(String owner, int balance) throws
3 4{ 5
6
7 8}
BalanceNegativeException
if( balance < 0 ) { /* negated precondition */ throw new BalanceNegativeException(); }
else { this.owner = owner; this.balance = balance; }
9
10
11
12
13
14
15
public void withdraw(int amount) throws WithdrawAmountNegativeException, WithdrawAmountTooLargeException {
if( amount < 0 ) { /* negated precondition */ throw new WithdrawAmountNegativeException(); }
else if ( balance < amount ) { /* negated precondition */ throw new WithdrawAmountTooLargeException(); }
16 }
else { this.balance = this.balance - amount; } 16 of 61
Version 2: Why Better than Version 1? (1)
1 public class {
2
3
4
5 AccountV2 alan = new AccountV2("Alan", -10) ;
public static void main(String[] args) {
System.out.println("Create an account for Alan with balance -10:"); try {
6
7}
8 catch ( BalanceNegativeException bne) {
9
10 }
System.out.println(alan);
System.out.println("Illegal negative account balance.");
Create an account for Alan with balance -10:
Illegal negative account balance.
L6: When attempting to call the constructor AccountV2 with a negative balance -10, a BalanceNegativeException (i.e.,
precondition violation) occurs, preventing further operations upon this invalid object.
17 of 61
BankAppV2
Version 2: Why Better than Version 1? (2.2)
Console Output:
Create an account for Mark with balance 100:
Mark’s current balance is: 100
Withdraw -1000000 from Mark’s account:
Illegal negative withdraw amount.
● L8: When attempting to call method withdraw with a negative amount -1000000, a WithdrawAmountNegativeException (i.e., precondition violation) occurs, preventing the withdrawal from proceeding.
● We should observe that adding preconditions to the supplier BankV2’s code forces the client BankAppV2’s code to get complicated by the try-catch statements.
● Adding clear contract (preconditions in this case) to the design
should not be at the cost of complicating the client’s code!! 19 of 61
Version 2: Why Better than Version 1? (2.1)
1 public class BankAppV2 {
2
3
4
5 AccountV2 mark = new AccountV2("Mark", 100); 6 System.out.println(mark);
public static void main(String[] args) {
System.out.println("Create an account for Mark with balance 100:"); try {
7
8
9 System.out.println(mark);
System.out.println("Withdraw -1000000 from Mark’s account:"); mark. withdraw(-1000000) ;
10 }
11
12
13 }
catch (BalanceNegativeException bne) { System.out.println("Illegal negative account balance.");
catch ( WithdrawAmountNegativeException wane) {
15
16 }
14
System.out.println("Illegal negative withdraw amount."); catch (WithdrawAmountTooLargeException wane) {
17
18
19 }
System.out.println("Illegal too large withdraw amount."); 18 of 61
Version 2: Why Better than Version 1? (3.1)
1 public class BankAppV2 {
2
3
4
5 AccountV2 tom = new AccountV2("Tom", 100); 6 System.out.println(tom);
public static void main(String[] args) {
System.out.println("Create an account for Tom with balance 100:"); try {
7
8
9 System.out.println(tom);
System.out.println("Withdraw 150 from Tom’s account:"); tom. withdraw(150) ;
10 }
11
12
13 }
14
15
16 }
17
18
19 }
catch (BalanceNegativeException bne) { System.out.println("Illegal negative account balance.");
catch (WithdrawAmountNegativeException wane) { System.out.println("Illegal negative withdraw amount.");
catch ( WithdrawAmountTooLargeException wane) { System.out.println("Illegal too large withdraw amount.");
20 of 61
Version 2: Why Better than Version 1? (3.2)
Console Output:
Create an account for Tom with balance 100:
Tom’s current balance is: 100
Withdraw 150 from Tom’s account:
Illegal too large withdraw amount.
● L8: When attempting to call method withdraw with a positive but too large amount 150, a WithdrawAmountTooLargeException (i.e., precondition violation) occurs, preventing the withdrawal from proceeding.
● We should observe that due to the added preconditions to the supplier BankV2’s code, the client BankAppV2’s code is forced to repeat the long list of the try-catch statements.
● Indeed, adding clear contract (preconditions in this case)
should not be at the cost of complicating the client’s code!! 21 of 61
Version 2: Why Still Not a Good Design? (2.1)
1 public class BankAppV2 {
2
3
4
5 AccountV2 jim = new AccountV2("Jim", 100); 6 System.out.println(jim);
public static void main(String[] args) {
System.out.println("Create an account for Jim with balance 100:"); try {
7
8
9 System.out.println(jim);
System.out.println("Withdraw 100 from Jim’s account:"); jim. withdraw(100) ;
10 }
11
12
13 }
14
15
16 }
17
18
19 }
23 of 61
catch (BalanceNegativeException bne) { System.out.println("Illegal negative account balance.");
catch (WithdrawAmountNegativeException wane) { System.out.println("Illegal negative withdraw amount.");
catch (WithdrawAmountTooLargeException wane) { System.out.println("Illegal too large withdraw amount.");
Version 2: Why Still Not a Good Design? (1)
1 public class AccountV2 {
2 public AccountV2(String owner, int balance) throws
3 4{ 5
6
7 8}
BalanceNegativeException
if( balance < 0 ) { /* negated precondition */ throw new BalanceNegativeException(); }
else { this.owner = owner; this.balance = balance; }
9
10
11
12
13
14
15
public void withdraw(int amount) throws WithdrawAmountNegativeException, WithdrawAmountTooLargeException {
if( amount < 0 ) { /* negated precondition */ throw new WithdrawAmountNegativeException(); }
else if ( balance < amount ) { /* negated precondition */ throw new WithdrawAmountTooLargeException(); }
16 }
else { this.balance = this.balance - amount; }
● Are all the exception conditions (¬ preconditions) appropriate?
● What if amount == balance when calling withdraw? 22 of 61
Version 2: Why Still Not a Good Design? (2.2)
L9: When attempting to call method withdraw with an amount 100 (i.e., equal to Jim’s current balance) that would result in a
zero balance (clearly a violation of ), there should have been a precondition violation.
Supplier AccountV2’s exception condition balance < amount has a missing case :
Create an account for Jim with balance 100:
Jim’s current balance is: 100
Withdraw 100 from Jim’s account:
Jim’s current balance is: 0
REQ1
● Calling withdraw with amount == balance will also result in an invalid account state (i.e., the resulting account balance is zero).
● ∴ L13 of AccountV2 should be balance <= amount. 24 of 61
Version 2: How Should We Improve it?
● Even without fixing this insufficient precondition, we could have avoided the above scenario by checking at the end of each method that the resulting account is valid.
⇒ We consider the condition this.balance > 0 as invariant throughout the lifetime of all instances of Account.
● Invariants of a class specify the precise conditions which all instances/objects of that class must satisfy.
○ Inv. of CSMajoarStudent? [ gpa >= 4.5 ] ○ Inv. of BinarySearchTree? [ in-order trav. → sorted key seq. ]
● The best we can do in Java is encode invariants as assertions: ○ CSMajorStudent: assert this.gpa >= 4.5
○ BinarySearchTree: assert this.inOrder() is sorted ○ Unlike exceptions, assertions are not in the class/method API.
● Create by adding assertions to the end of
Version 3
constructor and withdraw method of the Account class. 25 of 61
Version 3: Why Better than Version 2?
1ublicclass {
2 3 4 5 6 7 8
9 10
public static void main(String[] args) {
System.out.println(“Create an account for Jim with balance 100:”); try { AccountV3 jim = new AccountV3(“Jim”, 100);
System.out.println(jim);
System.out.println(“Withdraw 100 from Jim’s account:”); jim. withdraw(100) ;
System.out.println(jim); }
/* catch statements same as this previous slide:
* Version 2: Why Still Not a Good Design? (2.1) */
L8: Upon completion of jim.withdraw(100), Jim has a zero
balance, an assertion failure (i.e., invariant violation) occurs, 27 of 61preventing further operations on this invalid account object.
BankAppV3
Create an account for Jim with balance 100:
Jim’s current balance is: 100
Withdraw 100 from Jim’s account:
Exception in thread “main”
java.lang.AssertionError: Invariant: positive balance
p
Version 3: Added Assertions
to Approximate Class Invariants
1 public class AccountV3 {
2 public AccountV3(String owner, int balance) throws
3 4{ 5
6
7
8 9}
BalanceNegativeException
if(balance < 0) { /* negated precondition */ throw new BalanceNegativeException(); }
else { this.owner = owner; this.balance = balance; }
assert this.getBalance() > 0 : “Invariant: positive balance”;
10
11
12
13
14
15
16
17 assert this.getBalance() > 0 : “Invariant: positive balance”; 18 }
public void withdraw(int amount) throws WithdrawAmountNegativeException, WithdrawAmountTooLargeException {
if(amount < 0) { /* negated precondition */ throw new WithdrawAmountNegativeException(); }
else if (balance < amount) { /* negated precondition */ throw new WithdrawAmountTooLargeException(); }
else { this.balance = this.balance - amount; }
26 of 61
Version 3: Why Still Not a Good Design?
Let’s recall what we have added to the method withdraw:
○ From : exceptions encoding negated preconditions ○ From : assertions encoding the class invariants
1 public class AccountV3 {
Version 2
Version 3
2
3
4
5
6
7
8 9}
28 of 61
public void withdraw(int amount) throws WithdrawAmountNegativeException, WithdrawAmountTooLargeException {
if( amount < 0 ) { /* negated precondition */ throw new WithdrawAmountNegativeException(); }
else if ( balance < amount ) { /* negated precondition */ throw new WithdrawAmountTooLargeException(); }
else { this.balance = this.balance - amount; }
assert this.getBalance() > 0 : “Invariant: positive balance”;
contract
However, there is no in withdraw which specifies: ○ Obligations of supplier (AccountV3) if preconditions are met. ○ Benefits of client (BankAppV3) after meeting preconditions.
⇒ We illustrate how problematic this can be by creating
Version 4 , where deliberately mistakenly implement withdraw.
Version 4: What If the
Implementation of withdraw is Wrong? (1)
1 2 3 4 5 6 7 8 9
10 11
public class AccountV4 {
public void withdraw(int amount) throws
WithdrawAmountNegativeException, WithdrawAmountTooLargeException { if(amount < 0) { /* negated precondition */
throw new WithdrawAmountNegativeException(); }
else if (balance < amount) { /* negated precondition */
throw new WithdrawAmountTooLargeException(); } else { /* WRONT IMPLEMENTATION */
this.balance = this.balance + amount; } assert this.getBalance() > 0 :
owner + “Invariant: positive balance”; }
○ Apparently the implementation at L11 is wrong.
○ Adding a positive amount to a valid (positive) account balance
would not result in an invalid (negative) one.
⇒ The class invariant will not catch this flaw.
○ When something goes wrong, a good design (with an appropriate
contract ) should report it via a contract violation . 29 of 61
Version 4: How Should We Improve it?
● of a method specify the precise conditions which it will satisfy upon its completion.
This relies on the assumption that right before the method starts, its preconditions are satisfied (i.e., inputs valid) and invariants are satisfied (i.e,. object state valid).
○ Postcondition of double divide(int x, int y)?
[ Result × y == x ]
○ Postcondition of boolean binSearch(int x, int[] xs)?
● The best we can do in Java is, similar to the case of invariants, encode postconditions as assertions.
But again, unlike exceptions, these assertions will not be part of the class/method API.
● Create by adding assertions to the end of
[x∈xs ⇐⇒ Result]
Version 5
withdraw method of the Account class. 31 of 61
Postconditions
Version 4: What If the
Implementation of withdraw is Wrong? (2)
1 public class BankAppV4 {
2
3
4
5 System.out.println(jeremy);
public static void main(String[] args) {
System.out.println(“Create an account for Jeremy with balance 100:”) try { AccountV4 jeremy = new AccountV4(“Jeremy”, 100);
6 7
8
9 10
System.out.println(“Withdraw 50 from Jeremy’s account:”); jeremy. withdraw(50) ;
System.out.println(jeremy); }
/* catch statements same as this previous slide:
* Version 2: Why Still Not a Good Design? (2.1) */
L7: Resulting balance of Jeremy is valid (150 > 0), but withdrawal 30 of 61was done via an mistaken increase. ⇒ Violation of
Create an account for Jeremy with balance 100:
Jeremy’s current balance is: 100
Withdraw 50 from Jeremy’s account:
Jeremy’s current balance is: 150
REQ2
Version 5: Added Assertions
to Approximate Method Postconditions
1 public class AccountV5 {
2
3
4 int oldBalance = this.balance;
5 if(amount < 0) { /* negated precondition */
public void withdraw(int amount) throws WithdrawAmountNegativeException, WithdrawAmountTooLargeException {
6 7 8 9
throw new WithdrawAmountNegativeException(); }
else if (balance < amount) { /* negated precondition */
throw new WithdrawAmountTooLargeException(); }
else { this.balance = this.balance - amount; }
assert this.getBalance() > 0 :”Invariant: positive balance”;
10
11
12 }
assert this.getBalance() == oldBalance – amount :
“Postcondition: balance deducted”;
relates
32 of 61
⇒ Extra code (L4) to capture the pre-execution value of balance for the comparison at L11.
A postcondition typically the pre-execution value and the post-execution value of each relevant attribute (e.g.,balance in the case of withdraw).
;
Version 5: Why Better than Version 4?
1ublicclass {
2 3 4 5 6 7 8
9 10
public static void main(String[] args) {
System.out.println(“Create an account for Jeremy with balance 100:”) try { AccountV5 jeremy = new AccountV5(“Jeremy”, 100);
33 of 61
System.out.println(jeremy);
System.out.println(“Withdraw 50 from Jeremy’s account:”); jeremy. withdraw(50) ;
System.out.println(jeremy); }
/* catch statements same as this previous slide:
* Version 2: Why Still Not a Good Design? (2.1) */
L8: Upon completion of jeremy.withdraw(50), Jeremy has a wrong balance 150, an assertion failure (i.e., postcondition violation) occurs, preventing further operations on this invalid account object.
BankAppV5
Create an account for Jeremy with balance 100:
Jeremy’s current balance is: 100
Withdraw 50 from Jeremy’s account:
Exception in thread “main”
java.lang.AssertionError: Postcondition: balance deducted
Version 5:
Contract between Client and Supplier
benefits
obligations
amount non-negative amount not too large
balance deduction positive balance
BankAppV5.main
(CLIENT)
BankV5.withdraw
(SUPPLIER)
CLIENT SUPPLIER
35 of 61
amount non-negative balance deduction
amount not too large
benefits
positive balance
obligations
precondition precondition postcondition & invariant
postcondition & invariant
p
;
Evolving from Version 1 to Version 5
Design Flaws
Complete lack of Contract
Preconditions not strong enough (i.e., with missing cases) may result in an invalid account state.
–
Incorrect implementations do not necessarily result in a state that violates the class invariants.
–
● In Versions 2, 3, 4, 5, preconditions approximated as exceptions.
/Thesearenotpreconditions,buttheir logicalnegation.
/ Client BankApp’s code complicated by repeating the list of try-catch statements. ● In Versions 3, 4, 5, class invariants and postconditions approximated as assertions.
Improvements Made
–
V1 V2
V3
V4
V5 Added assertions as
Added exceptions as
method preconditions
Added assertions as
class invariants
Deliberately changed withdraw’s implementa- tion to be incorrect.
method postconditions
/ Unlike exceptions, these assertions will not appear in the API of withdraw. Potential clients of this method cannot know: 1) what their benefits are; and 2) what their suppliers’ obligations are.
/ For postconditions, extra code needed to capture pre-execution values of attributes.
34 of 61
DbC in Java
DbC is possible in Java, but not appropriate for your learning:
● Preconditions of a method: Supplier
● Encodetheirlogicalnegationsasexceptions.
● Inthebeginningofthatmethod,alistofif-statementsforthrowing
the appropriate exceptions.
Client
● Alistoftry-catch-statementsforhandlingexceptions.
● Postconditions of a method: Supplier
● Encodedasalistofassertions,placedattheendofthatmethod. Client
● AllsuchassertionsdonotappearintheAPIofthatmethod.
● Invariants of a class: Supplier
● Encodedasalistofassertions,placedattheendofeverymethod. Client
36of61 ● AllsuchassertionsdonotappearintheAPIofthatclass.
Why Java Interfaces Unacceptable ADTs (1)
It is useful to have:
● A generic collection class where the homogeneous type of
elements are parameterized as E.
● A reasonably intuitive overview of the ADT.
37 of 61
Java 8 List API
DbC in Eiffel: Supplier
DbC is supported natively in Eiffel for supplier:
class ACCOUNT create
make
feature — Attributes owner : STRING
balance : INTEGER feature — Constructors
make(nn: STRING; nb: INTEGER) require — precondition
positive_balance: nb > 0 do
owner := nn
balance := nb end
feature — Commands withdraw(amount: INTEGER)
require — precondition
non_negative_amount: amount > 0
affordable_amount: amount <= balance -- problematic, why?
do
balance := balance - amount ensure -- postcondition
balance_deducted: balance = old balance - amount end
invariant -- class invariant positive_balance: balance > 0
end
39 of 61
Why Java Interfaces Unacceptable ADTs (2)
Methods described in a natural language can be ambiguous:
38 of 61
DbC in Eiffel: Contract View of Supplier
Any potential client who is interested in learning about the kind of services provided by a supplier can look through the
(without showing any implementation details):
contract view
class ACCOUNT create
make
feature — Attributes owner : STRING
balance : INTEGER feature — Constructors
make(nn: STRING; nb: INTEGER) require — precondition
positive_balance: nb > 0 end
feature — Commands withdraw(amount: INTEGER)
require — precondition
non_negative_amount: amount > 0
affordable_amount: amount <= balance -- problematic, why?
ensure -- postcondition
balance_deducted: balance = old balance - amount
end
invariant -- class invariant
positive_balance: balance > 0 end
40 of 61
DbC in Eiffel: Anatomy of a Class
● Use feature clauses to group attributes, commands, queries. ● Explicitly declare list of commands under create clause, so
that they can be used as class constructors.
[ See the groups panel in Eiffel Studio. ]
● The class invariant invariant clause may be omitted:
○ There’s no class invariant: any resulting object state is acceptable.
○ The class invariant is equivalent to writing 41 of 61
invariant true
class SOME_CLASS create
— Explicitly list here commands used as constructors feature — Attributes
— Declare attribute here feature — Commands
— Declare commands (mutators) here feature — Queries
— Declare queries (accessors) here
invariant
— List of tagged boolean expressions for class invariants
end
Runtime Monitoring of Contracts (1)
In the specific case of ACCOUNT class with creation procedure make and command withdraw:
postcond_withdraw:
acc.balance = old acc.balance – a and acc.owner ~ old acc.owner
STATE: balance owner
account_inv: balance > 0
call
acc.withdraw(a)
precond_withdraw: 0 < a and a < balance
execute
acc.withdraw(a)
not (postcond_withdraw) Postcondition
Violation
not (postcond_make) create {ACCOUNT} acc.make(a, n)
not (account_inv) Class
not (precond_withdraw) Precondition
Violation
Invariant Violation
not (precond_make) create {ACCOUNT} acc.make(a, n)
call
precond_make: a > 0
execute
postcond_make:
acc.balance = a and acc.owner = n
43 of 61
DbC in Eiffel: Anatomy of a Feature
some_command
— Description of the command.
require
— List of tagged boolean expressions for preconditions
local
— List of local variable declarations
do
— List of instructions as implementation
ensure
— List of tagged boolean expressions for postconditions
end
● The precondition require clause may be omitted:
○ There’s no precondition: any starting state is acceptable. ○ The precondition is equivalent to writing
● The postcondition ensure clause may be omitted:
○ There’s no postcondition: any resulting state is acceptable.
○ The postcondition is equivalent to writing 42 of 61
require true
ensure true
Runtime Monitoring of Contracts (2)
In general, class C with creation procedure cp and any feature f: postcond_f:
STATE: class A
not I Class
Invariant Violation
not Pf Precondition
Violation
not Qf Postcondition
Violation
Qf
a_inv: attributes of I
call
a.f(…)
precond_f: Pf
execute
a.f(…)
not Qm create {A} a.make(…)
not Pm
create {A} a.make(…) Pm
postcond_make:
call
precond_make:
execute
44 of 61
Qm
Runtime Monitoring of Contracts (3)
● All are specified as Boolean expressions.
● Right a feature call (e.g., acc.withdraw(10)):
○ The current state of acc is called the pre-state.
○ Evaluate feature withdraw’s pre-condition using current values
of attributes and queries.
○ Cache values (implicitly) of all expressions involving the old
keyword in the post-condition .
e.g., cache the value of old balance via old balance ∶= balance
● Right the feature call:
○ The current state of acc is called the post-state.
○ Evaluate class ACCOUNT’s invariant using current values of
attributes and queries.
○ Evaluate feature withdraw’s post-condition using both current
and “cached” values of attributes and queries. 45 of 61
contracts
before
after
DbC in Eiffel: Precondition Violation (1.2)
47 of 61
DbC in Eiffel: Precondition Violation (1.1)
The client need not handle all possible contract violations:
class BANK_APP inherit
ARGUMENTS
create
make
feature — Initialization make
— Run application.
local
alan: ACCOUNT do
— A precondition violation with tag “positive_balance”
create {ACCOUNT} alan.make (“Alan”, -10) end
end
By executing the above code, the runtime monitor of Eiffel Studio
will report a contract violation (precondition violation with tag
“positive balance”). 46 of 61
DbC in Eiffel: Precondition Violation (2.1)
The client need not handle all possible contract violations:
class BANK_APP inherit
ARGUMENTS
create
make
feature — Initialization make
— Run application.
local
mark: ACCOUNT do
create {ACCOUNT} mark.make (“Mark”, 100)
— A precondition violation with tag “non_negative_amount” mark.withdraw(-1000000)
end end
By executing the above code, the runtime monitor of Eiffel Studio
will report a contract violation (precondition violation with tag 48 of 61″non negative amount”).
DbC in Eiffel: Precondition Violation (2.2)
49 of 61
DbC in Eiffel: Precondition Violation (3.2)
51 of 61
DbC in Eiffel: Precondition Violation (3.1)
The client need not handle all possible contract violations:
class BANK_APP inherit
ARGUMENTS
create
make
feature — Initialization make
— Run application.
local
tom: ACCOUNT do
create {ACCOUNT} tom.make (“Tom”, 100)
— A precondition violation with tag “affordable_amount” tom.withdraw(150)
end end
By executing the above code, the runtime monitor of Eiffel Studio
will report a contract violation (precondition violation with tag 50 of 61″affordable amount”).
DbC in Eiffel: Class Invariant Violation (4.1)
The client need not handle all possible contract violations:
class BANK_APP inherit
ARGUMENTS
create
make
feature — Initialization make
— Run application.
local
jim: ACCOUNT do
create {ACCOUNT} tom.make (“Jim”, 100)
jim.withdraw(100)
— A class invariant violation with tag “positive_balance”
end end
By executing the above code, the runtime monitor of Eiffel Studio
will report a contract violation (class invariant violation with tag 52 of 61″positive balance”).
DbC in Eiffel: Class Invariant Violation (4.2)
53 of 61
DbC in Eiffel: Postcondition Violation (5.2)
55 of 61
DbC in Eiffel: Postcondition Violation (5.1)
The client need not handle all possible contract violations:
class BANK_APP
inherit ARGUMENTS
create make
feature — Initialization
make
— Run application.
local
jeremy: ACCOUNT do
— Faulty implementation of withdraw in ACCOUNT: — balance := balance + amount
create {ACCOUNT} jeremy.make (“Jeremy”, 100) jeremy.withdraw(150)
— A postcondition violation with tag “balance_deducted”
end end
By executing the above code, the runtime monitor of Eiffel Studio
will report a contract violation (postcondition violation with tag 54 of 61″balance deducted”).
Beyond this lecture…
● Study this tutorial series on DbC and TDD: 56 of 61
https://www.youtube.com/playlist?list=PL5dxAmCmjv_
6r5VfzCQ5bTznoDDgh__KS
Index (1)
Motivation: Catching Defects – When?
What This Course Is About
Terminology: Contract, Client, Supplier
Client, Supplier, Contract in OOP (1)
Client, Supplier, Contract in OOP (2)
What is a Good Design?
A Simple Problem: Bank Accounts
Playing with the Various Versions in Java
Version 1: An Account Class
Version 1: Why Not a Good Design? (1)
Version 1: Why Not a Good Design? (2)
Version 1: Why Not a Good Design? (3)
Version 1: How Should We Improve it? (1)
Version 1: How Should We Improve it? (2)
57 of 61
Index (3)
Version 3: Why Still Not a Good Design?
Version 4: What If the
Implementation of withdraw is Wrong? (1)
Version 4: What If the
Implementation of withdraw is Wrong? (2)
Version 4: How Should We Improve it?
Version 5: Added Assertions
to Approximate Method Postconditions
Version 5: Why Better than Version 4?
Evolving from Version 1 to Version 5
Version 5:
Contract between Client and Supplier
DbC in Java
Why Java Interfaces Unacceptable ADTs (1)
Why Java Interfaces Unacceptable ADTs (2)
59 of 61
Index (2)
Version 2: Added Exceptions
to Approximate Method Preconditions
Version 2: Why Better than Version 1? (1)
Version 2: Why Better than Version 1? (2.1)
Version 2: Why Better than Version 1? (2.2)
Version 2: Why Better than Version 1? (3.1)
Version 2: Why Better than Version 1? (3.2)
Version 2: Why Still Not a Good Design? (1)
Version 2: Why Still Not a Good Design? (2.1)
Version 2: Why Still Not a Good Design? (2.2)
Version 2: How Should We Improve it?
Version 3: Added Assertions
to Approximate Class Invariants
Version 3: Why Better than Version 2?
58 of 61
Index (4)
DbC in Eiffel: Supplier
DbC in Eiffel: Contract View of Supplier
DbC in Eiffel: Anatomy of a Class
DbC in Eiffel: Anatomy of a Feature
Runtime Monitoring of Contracts (1)
Runtime Monitoring of Contracts (2)
Runtime Monitoring of Contracts (3)
DbC in Eiffel: Precondition Violation (1.1)
DbC in Eiffel: Precondition Violation (1.2)
DbC in Eiffel: Precondition Violation (2.1)
DbC in Eiffel: Precondition Violation (2.2)
DbC in Eiffel: Precondition Violation (3.1)
DbC in Eiffel: Precondition Violation (3.2)
DbC in Eiffel: Class Invariant Violation (4.1)
60 of 61
Index (5)
DbC in Eiffel: Postcondition Violation (5.1)
DbC in Eiffel: Postcondition Violation (5.2)
Beyond this lecture…
61 of 61
DbC in Eiffel: Class Invariant Violation (4.2)