Writing Complete Contracts
EECS3311: Software Design Fall 2017
CHEN-WEI WANG
How are contracts checked at runtime?
● All contracts are specified as Boolean expressions. ● Right before a feature call (e.g., ):
○ The current state of is called its pre-state.
○ Evaluate pre-condition using current values of attributes/queries.
○ Cache values of all expressions involving the old keyword in the
post-condition .
e.g., cache the value of via old balance ∶= balance
● Right after the feature call:
○ The current state of is called its post-state.
○ Evaluate invariant using current values of attributes and queries.
○ Evaluate post-condition using both current values and
“cached” values of attributes and queries. 2 of 25
acc
acc.withdraw(10)
old balance
acc
When are contracts complete?
● In post-condition , for each attribute , specify the relationship between its pre-state value and its post-state value.
○ Eiffel supports this purpose using the old keyword.
● This is tricky for attributes whose structures are composite rather than simple:
e.g., ARRAY, LINKED LIST are composite-structured. e.g., INTEGER, BOOLEAN are simple-structured.
● Rule of thumb: For an attribute whose structure is composite, we should specify that after the update:
1. The intended change is present; and
2. The rest of the structure is unchanged .
● The second contract is much harder to specify:
○ Reference aliasing [ ref copy vs. shallow copy vs. deep copy ] ○ Iterable structure [ use across ]
3 of 25
Account
class
ACCOUNT
inherit ANY
redefine is_equal end create
make
feature
owner: STRING balance: INTEGER
make (n: STRING) do
owner := n
balance := 0 end
deposit(a: INTEGER) do
balance := balance + a ensure
balance = old balance + a end
is_equal(other: ACCOUNT): BOOLEAN do
Result :=
owner other.owner
and balance = other.balance end
end
4 of 25
Bank
class BANK create make feature
accounts: ARRAY[ACCOUNT]
make do create accounts.make_empty end account_of (n: STRING): ACCOUNT
require
existing: across accounts as acc some acc.item.owner n end
do …
ensure Result.owner n end
add (n: STRING) require
non_existing:
across accounts as acc all acc.item.owner / n end
local new_account: ACCOUNT do
create new_account.make (n)
accounts.force (new_account, accounts.upper + 1) end
end
5 of 25
Roadmap of Illustrations
We examine 5 different versions of a command
deposit on (n ∶ STRING; a ∶ INTEGER)
VERSION
1 2 3 4 5
IMPLEMENTATION
Correct
Wrong Wrong Wrong Wrong
CONTRACTS
SATISFACTORY?
Incomplete No
Incomplete No Complete (reference copy) No Complete (shallow copy) No
Complete (deep copy) Yes
6 of 25
Object Structure for Illustration
We will test each version by starting with the same runtime object structure:
BANK accounts
b.accounts
01
b
ACCOUNT
owner
7 of 25
balance
0
ACCOUNT
owner
“Bill” “Steve”
balance
0
Version 1:
Incomplete Contracts, Correct Implementation
class BANK
deposit_on_v1 (n: STRING; a: INTEGER)
require across accounts as acc some acc.item.owner n end local i: INTEGER
do
from i := accounts.lower until i > accounts.upper loop
if accounts[i].owner n then accounts[i].deposit(a) end
i := i + 1 end
ensure
num_of_accounts_unchanged: accounts.count = old accounts.count
balance_of_n_increased:
account_of (n).balance = old account_of (n).balance + a
end end
8 of 25
Test of Version 1
class TEST_BANK test_bank_deposit_correct_imp_incomplete_contract: BOOLEAN
local
b: BANK do
comment(“t1: correct imp and incomplete contract”) create b.make
b.add (“Bill”)
b.add (“Steve”)
— deposit 100 dollars to Steve’s account
b.deposit on v1 (“Steve”, 100)
Result :=
b.account_of (“Bill”).balance = 0
and b.account_of (“Steve”).balance = 100 check Result end
end end
9 of 25
Test of Version 1: Result
10 of 25
Version 2:
Incomplete Contracts, Wrong Implementation
class BANK
deposit_on_v2 (n: STRING; a: INTEGER)
require across accounts as acc some acc.item.owner n end local i: INTEGER
do
— same loop as in version 1
— wrong implementation: also deposit in the first account
accounts[accounts.lower].deposit(a)
ensure
num_of_accounts_unchanged: accounts.count = old accounts.count
balance_of_n_increased:
account_of (n).balance = old account_of (n).balance + a
end end
Current postconditions lack a check that accounts other than n
are unchanged.
11 of 25
Test of Version 2
class TEST_BANK test_bank_deposit_wrong_imp_incomplete_contract: BOOLEAN
local
b: BANK do
comment(“t2: wrong imp and incomplete contract”) create b.make
b.add (“Bill”)
b.add (“Steve”)
— deposit 100 dollars to Steve’s account
b.deposit on v2 (“Steve”, 100)
Result :=
b.account_of (“Bill”).balance = 0
and b.account_of (“Steve”).balance = 100 check Result end
end end
12 of 25
Test of Version 2: Result
13 of 25
Version 3:
Complete Contracts with Reference Copy
class BANK
deposit_on_v3 (n: STRING; a: INTEGER)
require across accounts as acc some acc.item.owner n end local i: INTEGER
do
— same loop as in version 1
— wrong implementation: also deposit in the first account
accounts[accounts.lower].deposit(a)
ensure
num_of_accounts_unchanged: accounts.count = old accounts.count balance_of_n_increased:
account_of(n).balance = old account_of(n).balance + a others unchanged :
across old accounts as cursor
all cursor.item.owner / n implies
cursor.item account_of (cursor.item.owner) end
end end
14 of 25
Test of Version 3
class TEST_BANK test_bank_deposit_wrong_imp_complete_contract_ref_copy: BOOLEAN
local
b: BANK do
comment(“t3: wrong imp and complete contract with ref copy”) create b.make
b.add (“Bill”)
b.add (“Steve”)
— deposit 100 dollars to Steve’s account
b.deposit on v3 (“Steve”, 100)
Result :=
b.account_of (“Bill”).balance = 0
and b.account_of (“Steve”).balance = 100 check Result end
end end
15 of 25
Test of Version 3: Result
16 of 25
Version 4:
Complete Contracts with Shallow Object Copy
class BANK
deposit_on_v4 (n: STRING; a: INTEGER)
require across accounts as acc some acc.item.owner n end local i: INTEGER
do
— same loop as in version 1
— wrong implementation: also deposit in the first account
accounts[accounts.lower].deposit(a)
ensure
num_of_accounts_unchanged: accounts.count = old accounts.count balance_of_n_increased:
account_of (n).balance = old account_of (n).balance + a others unchanged :
across old accounts.twin as cursor all cursor.item.owner / n implies
17 of 25
cursor.item account_of (cursor.item.owner)
end end
end
Test of Version 4
class TEST_BANK test_bank_deposit_wrong_imp_complete_contract_shallow_copy: BOOLEAN
local
b: BANK do
comment(“t4: wrong imp and complete contract with shallow copy”) create b.make
b.add (“Bill”)
b.add (“Steve”)
— deposit 100 dollars to Steve’s account
b.deposit on v4 (“Steve”, 100)
Result :=
b.account_of (“Bill”).balance = 0
and b.account_of (“Steve”).balance = 100 check Result end
end end
18 of 25
Test of Version 4: Result
19 of 25
Version 5:
Complete Contracts with Deep Object Copy
class BANK
deposit_on_v5 (n: STRING; a: INTEGER)
require across accounts as acc some acc.item.owner n end local i: INTEGER
do
— same loop as in version 1
— wrong implementation: also deposit in the first account
accounts[accounts.lower].deposit(a)
ensure
num_of_accounts_unchanged: accounts.count = old accounts.count balance_of_n_increased:
account_of (n).balance = old account_of (n).balance + a others unchanged :
across old accounts.deep twin as cursor all cursor.item.owner / n implies
cursor.item account_of (cursor.item.owner) end
end end
20 of 25
Test of Version 5
class TEST_BANK test_bank_deposit_wrong_imp_complete_contract_deep_copy: BOOLEAN
local
b: BANK do
comment(“t5: wrong imp and complete contract with deep copy”) create b.make
b.add (“Bill”)
b.add (“Steve”)
— deposit 100 dollars to Steve’s account
b.deposit on v5 (“Steve”, 100)
Result :=
b.account_of (“Bill”).balance = 0
and b.account_of (“Steve”).balance = 100 check Result end
end end
21 of 25
Test of Version 5: Result
22 of 25
Exercise
● Consider the query account of (n: STRING) of BANK.
● How do we specify (part of) its postcondition to assert that the
state of the bank remains unchanged:
○ [×] ○ [×] ○ [×] ○ [×] ○ [×] ○ [✓]
● Which equality of the above is appropriate for the postcondition?
● Why is each one of the other equalities not appropriate? 23 of 25
accounts = old accounts
accounts = old accounts.twin
accounts = old accounts.deep_twin
accounts ̃ old accounts
accounts ̃ old accounts.twin
accounts ̃ old accounts.deep_twin
Index (1)
How are contracts checked at runtime? When are contracts complete? Account
Bank
Roadmap of Illustrations
Object Structure for Illustration
Version 1:
Incomplete Contracts, Correct Implementation
Test of Version 1
Test of Version 1: Result Version 2:
Incomplete Contracts, Wrong Implementation
Test of Version 2
Test of Version 2: Result
24 of 25
Index (2)
Version 3:
Complete Contracts with Reference Copy
Test of Version 3
Test of Version 3: Result
Version 4:
Complete Contracts with Shallow Object Copy
Test of Version 4
Test of Version 4: Result
Version 5:
Complete Contracts with Deep Object Copy
Test of Version 5
Test of Version 5: Result
Exercise
25 of 25