Subcontracting Readings: OOSCS2 Chapters 14 – 16
EECS3311 A & E: Software Design Fall 2020
CHEN-WEI WANG
Aspects of Inheritance
● Code Reuse ● Substitutability
○ Polymorphism and Dynamic Binding
[ compile-time type checks ]
2 of 18
○ Sub-contracting
[ runtime behaviour checks ]
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
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)}
More concisely:
P1 ⇒ P2
e.g., For command withdraw(amount: amount),
requires less than
What is the that requires the least? [ true ] 4 of 18
preconditions
P2 requires less than P1
P2 ∶ amount ≥ 0
P1 ∶ amount > 0
precondition
Background of Logic (2)
Given or
Q2 is stricter on (thus allowing less) outputs than Q1 does.
postconditions
Q2 ensures more than Q1
More concisely:
invariants
if
{x ∣Q2(x)}⊆{x ∣Q1(x)}
Q2 ⇒ Q1
e.g., For query q(i: INTEGER): BOOLEAN,
ensures more than
What is the that ensures the most? [ false ] 5 of 18
Q1 and Q2, we say that
Q2 ∶Result=(i >0)∧(i mod2=0)
Q1 ∶Result=(i >0)∨(i mod2=0)
postcondition
Inheritance and Contracts (1)
● The fact that we allow :
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
polymorphism
suggests that these instances may for each other.
● Intuitively, when expecting SMART PHONE, we can substitute it
by instances of any of its descendant classes.
∵ Descendants accumulate code from its ancestors and can thus meet expectations on their ancestors.
● Such can be reflected on contracts, where a
will:
○ Not require more from clients for using the services.
○ Not ensure less to clients for using the services. 6 of 18
substitutability
substitute
substitutable instance
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 (2.2)
class SMART_PHONE get_reminders: LIST[EVENT]
α: battery_level 0.1 — 10% ensure
require
β: ¦e Result S 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 S e happens today or tomorrow end
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 level is 12%, will fail to do so on an IPHONE_11_PRO.
8 of 18
Inheritance and Contracts (2.3)
class SMART_PHONE get_reminders: LIST[EVENT]
α: battery_level 0.1 — 10% ensure
require
β: ¦e Result S 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 S e happens today or tomorrow end
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 shocked by tomorrow-only reminders from IPHONE_11_PRO.
9 of 18
Inheritance and Contracts (2.4)
class SMART_PHONE get_reminders: LIST[EVENT]
α: battery_level 0.1 — 10% ensure
require
β: ¦e Result S 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 S e happens today between 9am and 5pm end
Contracts in descendant class IPHONE_11_PRO are suitable.
○ Require the same or less α ⇒ γ Clients satisfying the precondition for SMART_PHONE are not shocked
by not being to use the same feature for IPHONE_11_PRO. 10 of 18
Inheritance and Contracts (2.5)
class SMART_PHONE get_reminders: LIST[EVENT]
α: battery_level 0.1 — 10% ensure
require
β: ¦e Result S 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 S e happens today between 9am and 5pm end
Contracts in descendant class IPHONE_11_PRO are suitable.
○ Ensurethesameormore δ⇒β
Clients benefiting from SMART_PHONE are not shocked by failing to gain at least those benefits from same feature in IPHONE_11_PRO.
11 of 18
Contract Redeclaration Rule (1)
● In the context of some feature in a descendant class:
○ Use ○ Use
● The resulting ○
to redeclare its precondition. to redeclare its postcondition.
are:
12 of 18
require else
ensure then
runtime assertions checks
original_pre or else new_pre
⇒ 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 to satisfy what is required from the ancestor classes.
○
original_post and then new_post
⇒ 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.
Contract Redeclaration Rule (2.1)
class FOO f
do …
end end
● Unspecified original pre is as if declaring
∵ true ∨ new pre ≡ true
class BAR
inherit FOO redefine f end
f require else new pre do …
end end
require true
● Unspecified original post is as if declaring
∵ true ∧ new post ≡ new post
13 of 18
class BAR
inherit FOO redefine f end
f
end
class FOO f
do …
end end
do …
ensure then new post end
ensure true
Contract Redeclaration Rule (2.2)
class FOO
f require
original pre
do …
end end
class BAR
inherit FOO redefine f end
f
do …
end end
● Unspecified new pre is as if declaring
∵ original pre ∨ false ≡ original pre
require else false
class FOO f
do … ensure
original post
end end
● Unspecified new post is as if declaring
∵ original post ∧ true ≡ original post
14 of 18
class BAR
inherit FOO redefine f end
f
do …
end end
ensure then true
Invariant Accumulation
● Every class inherits invariants 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]
vertices.count 3 end
invariant
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
Inheritance and Contracts (3)
class FOO f
require
original pre
ensure
original post
end end
(Static) : ○
○
(Dynamic) : ○
○
should be proved as a tautology should be proved as a tautology
is checked
is checked
Design Time
class BAR
inherit FOO redefine f end
f
require else
new pre
ensure then
new post
end end
original pre
⇒
new pre
new post
⇒
original post
Runtime
original pre
∨
new pre
original post
∧
new post
16 of 18
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