Subcontracting Readings: OOSCS2 Chapters 14 – 16
EECS3311 M: Software Design Winter 2019
CHEN-WEI WANG
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? 3 of 16
Aspects of Inheritance
● Code Reuse ● Substitutability
○ Polymorphism and Dynamic Binding[ compile-time type checks ]
○ Sub-contracting 2 of 16
[ runtime behaviour checks ]
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 ] 4 of 16
Q2 ⇒ Q1
Q2 ∶Result=(i>0)∧(imod2=0) ensuresmorethan
Inheritance and Contracts (1)
● The fact that we allow :
polymorphism
local my_phone: SMART PHONE i_phone: IPHONE 6S PLUS
samsung_phone: GALAXY S6 EDGE
htc_phone: HTC ONE A9 do my_phone := i_phone
my_phone := samsung_phone my_phone := htc_phone
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
substitute
by instances of any of its descendant classes. meet expectations on their ancestors.
● Such can be reflected on contracts, where a
substitutability
will:
○ Not require more from clients for using the services.
substitutable instance
○ Not ensure less to clients for using the services. 5 of 16
Inheritance and Contracts (2.2)
class SMART_PHONE get_reminders: LIST[EVENT]
require
↵: battery_level ≥ 0.1 — 10% ensure
: ∀e ∶ Result e happens today end
class IPHONE_6S_PLUS
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
Contracts in descendant class IPHONE_6S_PLUS 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
7 of 16 level is 12%, will fail to do so on an IPHONE_6S_PLUS.
Inheritance and Contracts (2.1)
PHONE_USER my_phone: SMART_PHONE
my_phone
SMART_PHONE
get_reminders: LIST[EVENT] require ??
ensure ??
IPHONE_6S_PLUS
get_reminders: LIST[EVENT] require else ??
ensure then ??
6 of 16
Inheritance and Contracts (2.3)
class SMART_PHONE get_reminders: LIST[EVENT]
require
↵: battery_level ≥ 0.1 — 10% ensure
: ∀e ∶ Result e happens today end
class IPHONE_6S_PLUS
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
Contracts in descendant class IPHONE_6S_PLUS are not suitable. (e happens ty. or tw.)⇒(e happens ty.)nottautology. e.g., A client receiving today’s reminders from SMART_PHONE are
8 of 16 shocked by tomorrow-only reminders from IPHONE_6S_PLUS.
Inheritance and Contracts (2.4)
class SMART_PHONE get_reminders: LIST[EVENT]
require
↵: battery_level ≥ 0.1 — 10% ensure
: ∀e ∶ Result e happens today end
class IPHONE_6S_PLUS
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
Contracts in descendant class IPHONE_6S_PLUS are suitable.
○ Require the same or less ↵ ⇒ Clients satisfying the precondition for SMART_PHONE are not shocked
9 of 16 by not being to use the same feature for IPHONE_6S_PLUS.
Contract Redeclaration Rule (1)
● In the context of some feature in a descendant class: ○ Use to redeclare its precondition.
○ Use to redeclare its precondition.
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.
11 of 16
original_post and then new_post
Inheritance and Contracts (2.5)
class SMART_PHONE get_reminders: LIST[EVENT]
require
↵: battery_level ≥ 0.1 — 10% ensure
: ∀e ∶ Result e happens today end
class IPHONE_6S_PLUS
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
Contracts in descendant class IPHONE_6S_PLUS are suitable.
○ Ensurethesameormore ⇒
Clients benefiting from SMART_PHONE are not shocked by failing to 10 of 16gain at least those benefits from same feature in IPHONE_6S_PLUS.
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
12 of 16
class BAR
inherit FOO redefine f end
f require else new pre do …
end end
class FOO f
do …
end end
class FOO f
do …
end end
require true
do …
ensure then new post end
● Unspecified original post is as if declaring
ensure true
∵ true ∧ new post ≡ new post
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
13 of 16
∵ 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 ∧ 15 of 16
:
should be proved as a tautology
should be proved as a tautology
is checked
is checked
⇒
⇒ original post Runtime
class BAR
inherit FOO redefine f end
f
end
require else
new pre ensure then
new post end
original pre
new post
new pre
original pre
new pre
new post
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]
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?
14 of 16
(vertices.count = 5) ∧ (vertices.count = 4) ≡ false
Index (1)
Aspects of Inheritance 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) Contract Redeclaration Rule (2.1) Contract Redeclaration Rule (2.2) Invariant Accumulation
Inheritance and Contracts (3)
16 of 16