Copies: Reference vs. Shallow vs. Deep Writing Complete Postconditions
EECS3311 A: Software Design Winter 2020
CHEN-WEI WANG
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 are references to objects.
2 of 39
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
3 of 39
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.
4 of 39
○ 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
5 of 39
Base Case: a is primitive (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”
EE6CSo,fYo3r9kUniversity ObjectOrientedSoftwareConstruction 15-05-2716: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)
Before we undergo a change on imp, we “ copy ” it to old imp. After the change is completed, we compare imp vs. old imp. Can a change always be visible between “old” and “new” imp?
7 of 39
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.
8 of 39
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 is j all imp [j] old_imp [j] 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”
9 of 39
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 is j all imp [j] old_imp [j] 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”
10 of 39
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 is j all imp [j] old_imp [j] 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”
11 of 39
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 is j
all imp [j] old_imp [j] 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”
12 of 39
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 is j
all imp [j] old_imp [j] 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
13 of 39
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., acc.withdraw(10)):
The current state of acc 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., e.g., e.g.,
, of old expressions in the post-condition .
[ old accounts i id ∶= accounts[i].id ] [ old accounts i ∶= accounts[i] ] [ old accounts i twin ∶= accounts[i].twin ] [ old accounts ∶= accounts ] [ old accounts twin ∶= accounts.twin ] [ old current ∶= Current ] [ old current twin ∶= Current.twin ]
:=
old accounts[i].id
(old accounts[i]).id
(old accounts[i].twin).id
(old accounts)[i].id
(old accounts.twin)[i].id
(old Current).accounts[i].id
(old Current.twin).accounts[i].id
○ Right after the feature call:
The current state of acc 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.
14 of 39
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 ]
15 of 39
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
16 of 39
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 is acc some acc.owner n end
— not (across accounts is acc all acc.owner / n end) do … ensure Result.owner n end
add (n: STRING)
require — the input name does not exist
non_existing: across accounts is acc all acc.owner / n end — not (across accounts is acc some acc.owner n end)
local new_account: ACCOUNT do
create new_account.make (n)
accounts.force (new_account, accounts.upper + 1) end
end
17 of 39
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
18 of 39
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
19 of 39
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 is acc some acc.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: Current.account_of(n).balance =
old Current.account_of(n).balance + a end
end
20 of 39
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
21 of 39
Test of Version 1: Result
22 of 39
Version 2:
Incomplete Contracts, Wrong Implementation
class BANK
deposit_on_v2 (n: STRING; a: INTEGER)
require across accounts is acc some acc.owner n end local i: INTEGER
do …
— imp. of version 1, followed by a deposit into 1st account
accounts[accounts.lower].deposit(a)
ensure
num_of_accounts_unchanged: accounts.count = old accounts.count
balance_of_n_increased: Current.account_of(n).balance =
old Current.account_of(n).balance + a end
end
Current postconditions lack a check that accounts other than n
are unchanged.
23 of 39
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
24 of 39
Test of Version 2: Result
25 of 39
Version 3:
Complete Contracts with Reference Copy
class BANK
deposit_on_v3 (n: STRING; a: INTEGER)
require across accounts is acc some acc.owner n end local i: INTEGER
do …
— imp. of version 1, followed by a deposit into 1st account
accounts[accounts.lower].deposit(a)
ensure
num_of_accounts_unchanged: accounts.count = old accounts.count balance_of_n_increased:
Current.account_of(n).balance =
old Current.account_of(n).balance + a
others unchanged :
across old accounts is acc all
acc.owner / n implies acc Current.account_of(acc.owner) end
end end
26 of 39
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
27 of 39
Test of Version 3: Result
28 of 39
Version 4:
Complete Contracts with Shallow Object Copy
class BANK
deposit_on_v4 (n: STRING; a: INTEGER)
require across accounts is acc some acc.owner n end local i: INTEGER
do …
— imp. of version 1, followed by a deposit into 1st account
accounts[accounts.lower].deposit(a)
ensure
num_of_accounts_unchanged: accounts.count = old accounts.count balance_of_n_increased:
Current.account_of(n).balance =
old Current.account_of(n).balance + a
others unchanged :
across old accounts.twin is acc all
acc.owner / n implies acc Current.account_of(acc.owner) end
end end
29 of 39
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
30 of 39
Test of Version 4: Result
31 of 39
Version 5:
Complete Contracts with Deep Object Copy
class BANK
deposit_on_v5 (n: STRING; a: INTEGER)
require across accounts is acc some acc.owner n end local i: INTEGER
do …
— imp. of version 1, followed by a deposit into 1st account accounts[accounts.lower].deposit(a)
ensure
num_of_accounts_unchanged: accounts.count = old accounts.count balance_of_n_increased:
Current.account_of(n).balance =
old Current.account_of(n).balance + a
others unchanged :
across old accounts.deep twin is acc all
acc.owner / n implies acc Current.account_of(acc.owner) end
end end
32 of 39
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
33 of 39
Test of Version 5: Result
34 of 39
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? 35 of 39
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)
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) Shallow Copy of Collection Object (2)
Deep Copy of Collection Object (1)
36 of 39
Index (2)
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
37 of 39
Index (3) Version 2:
Incomplete Contracts, Wrong Implementation 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
38 of 39
Index (4)
Version 5:
Complete Contracts with Deep Object Copy
Test of Version 5
Test of Version 5: Result Exercise
39 of 39