Common Eiffel Errors: Contracts vs. Implementations
EECS3311 A: Software Design Winter 2020
CHEN-WEI WANG
Contracts vs. Implementations: Definitions
In Eiffel, there are two categories of constructs:
○ Implementations
are step-by-step instructions that have side-effects
e.g., ,
change attribute values do not return values
commands
e.g., ,
use attribute and parameter values to specify a condition return a Boolean value (i.e., True or False)
queries
… := …
across … as … loop … end
2 of 23
○ Contracts
are Boolean expressions that have no side-effects
… = …
across … as … all … end
Contracts vs. Implementations: Where?
● Instructions for Implementations: inst1, inst2
● Boolean expressions for Contracts: exp1, exp2, exp3, exp4, exp5
class
feature — Queries balance: INTEGER
require
exp1 do
inst1 ensure
exp2 end
3 of 23
ACCOUNT
feature — Commands withdraw
require
exp3 do
inst2 ensure
exp4 end
invariant
exp5
end — end of class ACCOUNT
Implementations:
Instructions with No Return Values
● Assignments
● Selections with branching instructions:
● Loops
if a > 0 then acc.deposit (a) else acc.withdraw (-a) end
from
i := a.lower until
i > a.upper loop
Result := Result + a[i]
i := i + 1 end
from list.start
until list.after
loop list.item.wdw(10) list.forth
end
across
list as cursor
loop
sum :=
sum + cursor.item
end
4 of 23
balance := balance + a
Contracts:
Expressions with Boolean Return Values
● Relational Expressions (using =, /=, ∼, /∼, >, <, >=, <=)
● Binary Logical Expressions (using and, and then, or, or else, implies)
● Logical Quantification Expressions (using all, some)
a>0
(a.lower <= index) and (index <= a.upper)
across
a.lower |..| a.upper as cursor
all
a [cursor.item] >= 0 end
● old keyword can only appear in postconditions (i.e., ensure).
5 of 23
balance = old balance + a
Contracts: Common Mistake (1)
class
ACCOUNT
feature
withdraw (a: INTEGER)
do
…
ensure
balance := old balance – a
end
…
Colon-Equal sign (:=) is used to write assignment instructions. 6 of 23
Contracts: Common Mistake (1) Fixed
class
ACCOUNT
feature
withdraw (a: INTEGER)
do
…
ensure
balance = old balance – a
end
…
7 of 23
Contracts: Common Mistake (2)
class
ACCOUNT
feature
withdraw (a: INTEGER)
do
…
ensure
across
a as cursor loop
…
end
…
across . . . loop . . . end is used to create loop instructions. 8 of 23
Contracts: Common Mistake (2) Fixed
class
ACCOUNT
feature
withdraw (a: INTEGER)
do
…
ensure
across
a as cursor
all — if you meant ¦, or use some if you meant §
… — A Boolean expression is expected here! end
…
9 of 23
Contracts: Common Mistake (3)
class
ACCOUNT
feature
withdraw (a: INTEGER)
do
…
ensure
old balance – a
end
…
Contracts can only be specified as Boolean expressions.
10 of 23
Contracts: Common Mistake (3) Fixed
class
ACCOUNT
feature
withdraw (a: INTEGER)
do
…
ensure
postcond_1: balance = old balance – a postcond_2: old balance > 0
end
…
11 of 23
Contracts: Common Mistake (4)
class
ACCOUNT
feature
withdraw (a: INTEGER)
require
old balance > 0
do
…
ensure
…
end
…
● Only postconditions may use the old keyword to specify the relationship between pre-state values (before the execution of withdraw) and post-state values (after the execution of withdraw ).
● Pre-state values (right before the feature is executed) are
indeed the old values, so there’s no need to qualify them!
12 of 23
Contracts: Common Mistake (4) Fixed
class
ACCOUNT
feature
withdraw (a: INTEGER)
require
balance > 0 do
…
ensure
…
end
…
13 of 23
Contracts: Common Mistake (5)
class LINEAR_CONTAINER create make
feature — Attributes
a: ARRAY[STRING] feature — Queries
count: INTEGER do Result := a.count end
get (i: INTEGER): STRING do Result := a[i] end feature — Commands
make do create a.make_empty end update (i: INTEGER; v: STRING) do …
ensure — Others Unchanged
across
1 |..| count as j
all
j.item /= i implies old get(j.item) get(j.item)
end end
end
Compilation Error:
○ Expression value to be cached before executing update?
[ Current.get(j.item) ] ○ But, in the pre-state, integer cursor j does not exist!
14 of 23
Contracts: Common Mistake (5) Fixed
class LINEAR_CONTAINER create make
feature — Attributes
a: ARRAY[STRING] feature — Queries
count: INTEGER do Result := a.count end
get (i: INTEGER): STRING do Result := a[i] end feature — Commands
make do create a.make_empty end update (i: INTEGER; v: STRING) do …
ensure — Others Unchanged
across
1 |..| count as j
all
j.item /= i implies (old Current).get(j.item) get(j.item)
end end
end
15 of 23
○ The idea is that the old expression should not involve the local cursor variable j that is introduced in the postcondition.
○ Whether to put (old Current.twin) or (old Current.deep twin) is up to your need.
Implementations: Common Mistake (1)
class
ACCOUNT
feature
withdraw (a: INTEGER)
do
balance = balance + 1 end
…
● Equal sign (=) is used to write Boolean expressions.
● In the context of implementations, Boolean expression values must appear:
○ on the RHS of an assignment;
○ as one of the branching conditions of an if-then-else statement; or ○ as the exit condition of a loop instruction.
16 of 23
Implementations: Common Mistake (1) Fixed
class
ACCOUNT
feature
withdraw (a: INTEGER)
do
balance := balance + 1 end
…
17 of 23
Implementations: Common Mistake (2)
class
BANK
feature
min_credit: REAL accounts: LIST[ACCOUNT]
no_warning_accounts: BOOLEAN do
across
accounts as cursor
all
cursor.item.balance > min_credit end
end
…
Again, in implementations, Boolean expressions cannot appear alone without their values being “captured”.
18 of 23
Implementations: Common Mistake (2) Fixed
1 2 3 4 5 6 7 8 9
10
11
12
13
14
15
16
class
BANK
feature
min_credit: REAL accounts: LIST[ACCOUNT]
no_warning_accounts: BOOLEAN do
Result := across
accounts as cursor all
cursor.item.balance > min_credit end
end
…
Rewrite L10 – L14 using across … as … some … end.
Hint: ∀x ● P(x) ≡ ¬(∃x ● ¬P(x)) 19 of 23
Implementations: Common Mistake (3)
class
BANK
feature
accounts: LIST[ACCOUNT]
total_balance: REAL do
Result := across
accounts as cursor loop
Result := Result + cursor.item.balance end
…
end
…
In implementations, since instructions do not return values, they
cannot be used on the RHS of assignments.
20 of 23
Implementations: Common Mistake (3) Fixed
class
BANK
feature
accounts: LIST[ACCOUNT]
total_balance: REAL do
across
accounts as cursor
loop
Result := Result + cursor.item.balance
end end
21 of 23
Index (1)
Contracts vs. Implementations: Definitions
Contracts vs. Implementations: Where? Implementations:
Instructions with No Return Values Contracts:
Expressions with Boolean Return Values Contracts: Common Mistake (1) Contracts: Common Mistake (1) Fixed Contracts: Common Mistake (2) Contracts: Common Mistake (2) Fixed Contracts: Common Mistake (3) Contracts: Common Mistake (3) Fixed Contracts: Common Mistake (4) Contracts: Common Mistake (4) Fixed
Contracts: Common Mistake (5)
22 of 23
Index (2)
Contracts: Common Mistake (5) Fixed
Implementations: Common Mistake (1) Implementations: Common Mistake (1) Fixed Implementations: Common Mistake (2) Implementations: Common Mistake (2) Fixed Implementations: Common Mistake (3)
Implementations: Common Mistake (3) Fixed
23 of 23