Subcontracting Readings: OOSCS2 Chapters 14 – 16
EECS3311 A & E: Software Design Fall 2020
CHEN-WEI WANG
Learning Objectives
1. Preconditions: require less vs. require more 2. Postconditions: ensure less vs. ensure more 3. Inheritance and Contracts: Static Analysis
4. Inheritance and Contracts: Runtime Checks
3 of 18
Aspects of Inheritance
● Code Reuse ● Substitutability
○ Polymorphism and Dynamic Binding[ compile-time type checks ]
○ Sub-contracting 2 of 18
[ runtime behaviour checks ]
Background of Logic (1)
Given P1 and P2, we say that if
P2 is less strict on (thus allowing more) inputs than P1 does. {x P1(x)}⊆{x P2(x)}
[ true ]
preconditions
P2 requires less than P1
More concisely:
e.g., For command withdraw(amount: amount),
P1 ⇒ P2
∶ requires less than P1 ∶ amount > 0
P2 amount ≥ 0 precondition
What is the that requires the least? 4 of 18
Background of Logic (2)
Q1 and Q2, we say that Q2 is stricter on (thus allowing less) outputs than Q1 does.
Given or
postconditions
invariants
Q2 ensures more than Q1
if
{x Q2(x)}⊆{x Q1(x)}
More concisely:
e.g., For query q(i: INTEGER): BOOLEAN,
Q1 ∶Result=(i >0)∨(i mod2=0)
What is the postcondition that ensures the most? [ false ] 5 of 18
Q2 ⇒ Q1
Q2 ∶Result=(i>0)∧(imod2=0) ensuresmorethan
Inheritance and Contracts (2.1)
PHONE_USER my_phone: SMART_PHONE
my_phone
SMART_PHONE
get_reminders: LIST[EVENT] require ??
ensure ??
IPHONE_11_PRO
get_reminders: LIST[EVENT] require else ??
ensure then ??
7 of 18
Inheritance and Contracts (1)
● The fact that we allow :
suggests that these instances may
● Intuitively, when expecting SMART PHONE, we can substitute it
for each other. ∵ Descendants accumulate code from its ancestors and can thus
by instances of any of its descendant classes. meet expectations on their ancestors.
● Such can be reflected on contracts, where a
substitutability
substitutable instance
will:
○ Not require more from clients for using the services.
○ Not ensure less to clients for using the services. 6 of 18
polymorphism
local my_phone: SMART PHONE i_phone: IPHONE 11 PRO
samsung_phone: GALAXY S10 PLUS
huawei_phone: HUAWEI P30 PRO do my_phone := i_phone
my_phone := samsung_phone my_phone := huawei_phone
substitute
Inheritance and Contracts (2.2)
Contracts in descendant class IPHONE_11_PRO are not suitable. (battery level ≥ 0.1 ⇒ battery level ≥ 0.15) is not a tautology. e.g., A client able to get reminders on a SMART_PHONE, when battery
8 of 18 level is 12%, will fail to do so on an IPHONE_11_PRO.
class SMART_PHONE get_reminders: LIST[EVENT]
require
↵: battery_level ≥ 0.1 — 10% ensure
: ∀e ∶ Result e happens today end
class IPHONE_11_PRO
inherit SMART_PHONE redefine get_reminders end
get_reminders: LIST[EVENT] require else
: battery_level ≥ 0.15 — 15% ensure then
: ∀e ∶ Result e happens today or tomorrow end
Inheritance and Contracts (2.3)
Contracts in descendant class IPHONE_11_PRO are not suitable. (e happens ty. or tw.)⇒(e happens ty.)nottautology. e.g., A client receiving today’s reminders from SMART_PHONE are
9 of 18 shocked by tomorrow-only reminders from IPHONE_11_PRO.
class SMART_PHONE get_reminders: LIST[EVENT]
require
↵: battery_level ≥ 0.1 — 10% ensure
: ∀e ∶ Result e happens today end
class IPHONE_11_PRO
inherit SMART_PHONE redefine get_reminders end
get_reminders: LIST[EVENT] require else
: battery_level ≥ 0.15 — 15% ensure then
: ∀e ∶ Result e happens today or tomorrow end
Inheritance and Contracts (2.5)
Contracts in descendant class IPHONE_11_PRO are suitable.
○ Ensurethesameormore ⇒
Clients benefiting from SMART_PHONE are not shocked by failing to 11 of 18gain at least those benefits from same feature in IPHONE_11_PRO.
class SMART_PHONE get_reminders: LIST[EVENT]
require
↵: battery_level ≥ 0.1 — 10% ensure
: ∀e ∶ Result e happens today end
class IPHONE_11_PRO
inherit SMART_PHONE redefine get_reminders end
get_reminders: LIST[EVENT] require else
: battery_level ≥ 0.05 — 5% ensure then
: ∀e ∶ Result e happens today between 9am and 5pm end
Inheritance and Contracts (2.4)
Contracts in descendant class IPHONE_11_PRO are suitable.
○ Require the same or less ↵ ⇒ Clients satisfying the precondition for SMART_PHONE are not shocked
10 of 18by not being to use the same feature for IPHONE_11_PRO.
class SMART_PHONE get_reminders: LIST[EVENT]
require
↵: battery_level ≥ 0.1 — 10% ensure
: ∀e ∶ Result e happens today end
class IPHONE_11_PRO
inherit SMART_PHONE redefine get_reminders end
get_reminders: LIST[EVENT] require else
: battery_level ≥ 0.05 — 5% ensure then
: ∀e ∶ Result e happens today between 9am and 5pm end
Contract Redeclaration Rule (1)
● In the context of some feature in a descendant class: ○ Use to redeclare its precondition.
○ Use to redeclare its postcondition.
require else
ensure then
● The resulting are:
runtime assertions checks
○ ⇒ Clients able to satisfy original pre will not be shocked.
∵ true ∨ new pre ≡ true
A precondition violation will not occur as long as clients are able
original_pre or else new_pre
○ to satisfy what is required from the ancestor classes.
⇒ Failing to gain original post will be reported as an issue.
∵ false ∧ new post ≡ false
A postcondition violation occurs (as expected) if clients do not receive at least those benefits promised from the ancestor classes.
original_post and then new_post
12 of 18
Contract Redeclaration Rule (2.1)
● Unspecified original pre is as if declaring
∵ true ∨ new pre ≡ true
class BAR
inherit FOO redefine f end
f
end
13 of 18
class FOO f
do …
end end
require true
class FOO f
do …
end end
do …
ensure then new post end
● Unspecified original post is as if declaring
ensure true
∵ true ∧ new post ≡ new post
class BAR
inherit FOO redefine f end
f require else new pre do …
end end
Invariant Accumulation
● Every class inherits from all its ancestor classes.
● Since invariants are like postconditions of all features, they are
“conjoined” to be checked at runtime.
class POLYGON
vertices: ARRAY[POINT]
invariant
vertices.count ≥ 3 end
class RECTANGLE inherit POLYGON invariant
vertices.count = 4 end
● What is checked on a RECTANGLE instance at runtime: (vertices.count ≥ 3) ∧ (vertices.count = 4) ≡ (vertices.count = 4)
● Can PENTAGON be a descendant class of RECTANGLE?
15 of 18
(vertices.count = 5) ∧ (vertices.count = 4) ≡ false
invariants
Contract Redeclaration Rule (2.2)
class FOO
f require
original pre
do …
end end
● Unspecified new pre is as if declaring
class BAR
inherit FOO redefine f end
f
do …
end end
require else false
class FOO f
do … ensure
original post
end end
∵ original pre ∨ false ≡ original pre
class BAR
inherit FOO redefine f end
f
do …
end end
● Unspecified new post is as if declaring
14 of 18
∵ original post ∧ true ≡ original post
ensure then true
Inheritance and Contracts (3)
class FOO f
require
original pre ensure
original post end
end
Design Time
(Static)
○
○
(Dynamic) : ○ ∨
○ original post ∧ 16 of 18
:
should be proved as a tautology
should be proved as a tautology
is checked
is checked
⇒
⇒ original post Runtime
original pre
new pre
new post
original pre
new pre
new post
class BAR
inherit FOO redefine f end
f
end
require else
new pre ensure then
new post end
Index (1)
Aspects of Inheritance
Learning Objectives
Background of Logic (1)
Background of Logic (2)
Inheritance and Contracts (1)
Inheritance and Contracts (2.1)
Inheritance and Contracts (2.2)
Inheritance and Contracts (2.3)
Inheritance and Contracts (2.4)
Inheritance and Contracts (2.5)
Contract Redeclaration Rule (1)
17 of 18
Index (2)
Contract Redeclaration Rule (2.1)
Contract Redeclaration Rule (2.2)
Invariant Accumulation
Inheritance and Contracts (3)
18 of 18