Types: Reference vs. Expanded Copies: Reference vs. Shallow vs. Deep Writing Complete Postconditions
EECS3311 M: Software Design Winter 2019
CHEN-WEI WANG
Expanded Class: Modelling
● We may want to have objects which are: ○ Integral parts of some other objects
○ Not shared among objects
e.g., Each workstation has its own CPU, monitor, and keyword. All workstations share the same network.
2 of 43
Expanded Class: Programming (2)
class KEYBOARD … end class CPU … end class MONITOR … end class NETWORK … end class WORKSTATION
k: expanded KEYBOARD c: expanded CPU
m: expanded MONITOR n: NETWORK
end
Alternatively:
expanded class KEYBOARD … end expanded class CPU … end expanded class MONITOR … end class NETWORK … end
class WORKSTATION k: KEYBOARD
c: CPU
m: MONITOR
n: NETWORK end
3 of 43
Expanded Class: Programming (3)
1 2 3 4 5 6 7 8 9
10 11 12 13 14
● L5: object of expanded type is automatically initialized.
● L9 & L10: no sharing among objects of expanded type.
● L7 & L12: = between expanded objects compare their contents.
expanded class
B
feature
change_i (ni: INTEGER)
do
i := ni end
feature
i: INTEGER
end
4 of 43
test_expanded: BOOLEAN local
eb1, eb2: B do
Result := eb1.i = 0 and eb2.i = 0 check Result end
Result := eb1 = eb2
check Result end
eb2.change_i (15)
Result := eb1.i = 0 and eb2.i = 15 check Result end
Result := eb1 /= eb2
check Result end
end
Reference vs. Expanded (1)
● Every entity must be declared to be of a certain type (based on a class).
● Every type is either referenced or expanded.
● In reference types:
○ y denotes a reference to some object
○ x := y attaches x to same object as does y ○ x = y compares references
● In expanded types:
○ y denotes some object (of expanded type)
5 of 43
○ x := y copies contents of y into x ○ x = y compares contents
[x y]
Reference vs. Expanded (2)
Problem: Every published book has an author. Every author may publish more than one books. Should the author field of a book reference-typed or expanded-typed?
reference-typed author expanded-typed author
6 of 43
Copying Objects
Say variables c1 and c2 are both declared of type C. [ c1, c2: C ]
● There is only one attribute a declared in class C. ● c1.a and c2.a may be of either:
○ expanded type or ○ reference type
7 of 43
c1
c1.a
C
a
c2
a
C
c2.a
Copying Objects: Reference Copy
Reference Copy
○ Copy the address stored in variable c2 and store it in c1.
⇒ Both c1 and c2 point to the same object.
⇒ Updates performed via c1 also visible to c2. [ aliasing ]
c1 := c2
8 of 43
c1
c1.a
C
a
c2
a
C
c2.a
Copying Objects: Shallow Copy
Shallow Copy
○ Create a temporary, behind-the-scene object c3 of type C.
9 of 43
○ Initialize each attribute a of c3 via reference copy: ○ Make a reference copy of c3:
c3.a := c2.a c1 := c3 [ c1 /= c2 ]
⇒ c1 and c2 are not pointing to the same object.
⇒ c1.a and c2.a are pointing to the same object.
⇒ Aliasing still occurs: at 1st level (i.e., attributes of c1 and c2)
a
C
c1 := c2.twin
c1
c3
c2
c2.a
c1.a
a
C
a
C
Copying Objects: Deep Copy
Deep Copy
○ Create a temporary, behind-the-scene object c3 of type C. ○ Recursively initialize each attribute a of c3 as follows:
c1 := c2.deep_twin
10 of 43
Base Case: a is expanded (e.g., INTEGER). c3.a := c2.a. Recursive Case: a is referenced. c3.a := c2.a.deep_twin
○ Make a reference copy of c3:
⇒ c1 and c2 are not pointing to the same object.
⇒ c1.a and c2.a are not pointing to the same object. ⇒ No aliasing occurs at any levels.
c1 := c3
c1
c3
C a
a
c1.a
c2.a.deep_twin
c2.a
C
C
c2
a
Copying OShbajelclotsw and deep cloning
a
O1
! Initial situation: ! Result of:
name landlord loved_one
O2
“Almaviva”
O3
“Figaro”
“Susanna”
b := a
b
c := a.twin
O4 c
“Almaviva”
d := a.deep_twin
O6
d name landlord loved_one
“Almaviva”
O5
“Figaro”
O7
“Susanna”
EE1C1S,oYfor4k3University Object Oriented Software Construction 15-05-27 16:29 28
Example: Collection Objects (1)
● In any OOPL, when a variable is declared of a type that corresponds to a known class (e.g., STRING, ARRAY, LINKED LIST, etc.):
At runtime, that variable stores the address of an object of that type (as opposed to storing the object in its entirety).
● Assume the following variables of the same type:
…
local
imp : ARRAY[STRING] old_imp: ARRAY[STRING]
do
create {ARRAY[STRING]} imp.make_empty imp.force(“Alan”, 1) imp.force(“Mark”, 2)
imp.force(“Tom”, 3)
…
12 of 43
Example: Collection Objects (2)
● Variables imp and old imp store address(es) of some array(s). ● Each “slot” of these arrays stores a STRING object’s address.
13 of 43
imp
imp[1] imp[2] imp[3]
STRING
value
“Mark”
STRING
value
“Alan”
old_imp
ARRAY[STRING]
??
STRING
value
“Tom”
Reference Copy of Collection Object
1 2
3 4 5 6 7
old imp := imp
Result := old_imp = imp — Result = true imp[2] := “Jim”
Result :=
across 1 |..| imp.count as j
all imp [j.item] old_imp [j.item] end — Result = true
Before Executing L3
After Executing L3
ARRAY[STRING]
old_imp
imp
ARRAY[STRING]
old_imp
imp
STRING
value
“Alan”
“Mark” “Tom”
STRING
value
STRING
value
STRING
STRING
STRING
STRING
value
“Alan”
value
“Mark”
value
“Tom”
value
“Jim”
14 of 43
1 2
3 4 5 6 7
Shallow Copy of Collection Object (1)
old imp := imp.twin
Result := old_imp = imp — Result = false imp[2] := “Jim”
Result :=
across 1 |..| imp.count as j
all imp [j.item] old_imp [j.item] end — Result = false
Before Executing L3
After Executing L3
ARRAY[STRING]
ARRAY[STRING]
STRING
imp
old_imp
imp
old_imp
value
“Jim”
STRING
STRING
STRING
STRING
STRING
value
“Alan”
value
“Mark”
STRING
value
“Tom”
value
“Alan”
value
“Mark”
ARRA
Y[STR
ING]
ARRA
Y[STR
ING]
value
“Tom”
15 of 43
1 2
3 4 5 6 7
Shallow Copy of Collection Object (2)
old imp := imp.twin
Result := old_imp = imp — Result = false imp[2].append (“***”)
Result :=
across 1 |..| imp.count as j
all imp [j.item] old_imp [j.item] end — Result = true
Before Executing L3
After Executing L3
ARRAY[STRING]
ARRAY[STRING]
imp
old_imp
imp
old_imp
“Mark***”
STRING
STRING
STRING
STRING
STRING
value
“Alan”
value
“Mark”
value
“Tom”
value
“Alan”
value
“Mark”
STRING
value
ARRA
Y[STR
ING]
ARRA
Y[STR
ING]
“Tom”
16 of 43
1 2
3 4 5 6
Deep Copy of Collection Object (1)
old imp := imp.deep twin
Result := old_imp = imp — Result = false imp[2] := “Jim”
Result :=
across 1 |..| imp.count as j
all imp [j.item] old_imp [j.item] end — Result = false
Before Executing L3
After Executing L3
imp
ARRAY[STRING]
STRING STRING STRING value “Alan” value “Mark” value “Tom”
STRING STRING STRING value “Alan” value “Mark” value “Tom”
17 of 43
imp
STRING
ARRAY[STRING]
ING
ST
“Jim”
STRING
STRING
value
“Alan”
value
STRING
STRING
value
“Alan”
“Mark”
“Mark”
“Tom”
value
R value
value
“Tom”
STRING
value
old_imp
old_imp
ARRAY[STRING]
ARRAY[STRING]
Deep Copy of Collection Object (2)
1 2
3 4 5 6
old imp := imp.deep twin
Result := old_imp = imp — Result = false imp[2].append (“***”)
Result :=
across 1 |..| imp.count as j
all imp [j.item] old_imp [j.item] end — Result = false
imp
ARRAY[STRING]
STRING STRING STRING value “Alan” value “Mark” value “Tom”
STRING STRING STRING value “Alan” value “Mark” value “Tom”
old_imp
18 of 43
Before Executing L3
After Executing L3
imp
ARRAY[STRING]
STRING STRING STRING value “Alan” value “Mark” value “Tom”
“Mark***”
old_imp
STRING STRING STRING value “Alan” value “Mark” value “Tom”
ARRAY[STRING]
ARRAY[STRING]
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, via e.g.,
e.g., e.g., e.g., e.g.,
, of in the post-condition . [ old balance ∶= balance ] [ old accounts i id ∶= accounts[i].id ] [ old accounts i ∶= accounts[i] ]
[ old accounts ∶= accounts ] [ old current ∶= Current ]
oldbalance = balance−a
:=
acc.withdraw(10)
acc
old expressions
old accounts[i].id
(old accounts[i]).id
(old accounts)[i].id
(old Current).accounts[i].id
● 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. 19 of 43
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 ]
20 of 43
Account
class
ACCOUNT
inherit ANY
redefine is_equal end create
make
feature — Attributes owner: STRING balance: INTEGER
feature — Commands 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
21 of 43
Bank
class BANK create make feature
accounts: ARRAY[ACCOUNT]
make do create accounts.make_empty end account_of (n: STRING): ACCOUNT
require — the input name exists
existing: across accounts as acc some acc.item.owner n end
— not (across accounts as acc all acc.item.owner / n end) do …
ensure Result.owner n
end
add (n: STRING)
require — the input name does not exist
non_existing: across accounts as acc all acc.item.owner / n end
— not (across accounts as acc some acc.item.owner n end) local new_account: ACCOUNT
do
create new_account.make (n)
accounts.force (new_account, accounts.upper + 1) end
end
22 of 43
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
23 of 43
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
24 of 43
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
25 of 43
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
26 of 43
Test of Version 1: Result
27 of 43
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.
28 of 43
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
29 of 43
Test of Version 2: Result
30 of 43
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
31 of 43
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
32 of 43
Test of Version 3: Result
33 of 43
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
34 of 43
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
35 of 43
Test of Version 4: Result
36 of 43
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
37 of 43
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
38 of 43
Test of Version 5: Result
39 of 43
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? 40 of 43
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)
Expanded Class: Modelling Expanded Class: Programming (2) Expanded Class: Programming (3) Reference vs. Expanded (1) Reference vs. Expanded (2) Copying Objects
Copying Objects: Reference Copy Copying Objects: Shallow Copy Copying Objects: Deep Copy Example: Copying Objects Example: Collection Objects (1) Example: Collection Objects (2) Reference Copy of Collection Object
Shallow Copy of Collection Object (1)
41 of 43
Index (2)
Shallow Copy of Collection Object (2) Deep Copy of Collection Object (1) Deep Copy of Collection Object (2) 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
42 of 43
Index (3)
Test of Version 2
Test of Version 2: Result 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
43 of 43