Copying Objects
Writing Complete Postconditions
EECS3311 A & E: Software Design Fall 2020
CHEN-WEI WANG
Part 1
Copying Objects
3 of 41
Learning Objectives
Upon completing this lecture, you are expected to understand: 1. 3 Levels of Copying Objects:
Reference vs. Shallow vs. Deep
2. Use of the old keyword in Postconditions
3. Writing Complete Postconditions using logical quantifications:
Universal (∀) vs. Existential (∃) 2 of 41
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.
c1
c2
c1.a
c2.a
a
C
C
a
4 of 41
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.
c1
c2
5 of 41
[ aliasing ] c1.a
c2.a
c1 := c2
C
a
C
a
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
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 := c3
C
a
c1.a
c2.a.deep_twin
c2.a
c1
c3
c2
C a
C
a
7 of 41
⇒ 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.
Copying Objects: Shallow Copy
Shallow Copy
○ Create a temporary, behind-the-scene object c3 of type C.
○ Initialize each attribute a of c3 via reference copy: c3.a := c2.a ○ Make a reference copy of c3: c1 := c3
⇒ c1 and c2 are not pointing to the same object. [ c1 /= c2 ] ⇒ c1.a and c2.a are pointing to the same object.
⇒ Aliasing still occurs: at 1st level (i.e., attributes of c1 and c2)
c1 := c2.twin
C
a
c1
c3
c1.a
c2.a
a
C
a
C
c2
6 of 41
Copying OShbajelclotsw and deep cloning
b := a
b
a
O1
! Initial situation: ! Result of:
name landlord loved_one
O2
“Almaviva”
O3
“Susanna”
“Figaro”
c := a.twin
O4 c
d := a.deep_twin
O6
d name landlord loved_one
“Almaviva”
“Almaviva”
O5
O7
“Susanna”
“Figaro”
EE8CSo,fYo4r1kUniversity 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.
● Afterthechangeiscompleted,wecompareimpvs.oldimp.
9 of 41 ● Can a change always be visible between “old” and “new” imp?
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
1 2
3 4 5 6 7
Reference Copy of Collection Object
Before Executing L3
After Executing L3
old_imp
imp
ARRAY[STRING]
STRING STRING STRING value “Alan” value “Mark” value “Tom”
STRING value “Jim”
old_imp
imp
ARRAY[STRING]
“Mark”
STRING
STRING
STRING
value
“Alan”
value
value
“Tom”
11 of 41
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.
ARRAY[STRING]
imp
imp[1] imp[2] imp[3]
STRING
value
“Mark”
STRING
value
“Alan”
STRING
??
value
“Tom”
old_imp
10 of 41
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
1 2
3 4 5 6 7
Shallow Copy of Collection Object (1)
Before Executing L3
After Executing L3
ARRAY[STRING]
ARRAY[STRING]
ING
imp
old_imp
Alan” “Mark” “Tom”
ARRAY[STRING]
imp
old_imp
Alan”
ARRAY[STRING]
“Mark”
ST
“Jim”
“Tom”
STRING
STRING
STRING
STRING
STRING
STRING
value “
value
value
value “
value
R value
value
12 of 41
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
1 2
3 4 5 6 7
Shallow Copy of Collection Object (2)
Before Executing L3
After Executing L3
ARRAY[STRING]
ARRAY[STRING]
imp
old_imp
Alan” “Mark” “Tom”
ARRAY[STRING]
imp
old_imp
“Mark***”
STRING
STRING
STRING
STRING
STRING
STRING
value “
value
value
value
“Alan”
value
“Mark”
value
“Tom”
ARRA
Y[STR
ING]
13 of 41
Deep Copy of Collection Object (2)
1 old imp := imp.deep twin
2 Result := old_imp = imp — Result = false
3 imp[2].append (“***”) 4 Result :=
5 6
across 1 |..| imp.count is j
all imp [j] ∼ old_imp [j] end — Result = false
Before Executing L3 After Executing L3
imp
old_imp
ARRAY[STRING]
STRING STRING STRING value “Alan” value “Mark” value “Tom”
“Mark***”
imp
old_imp
ARRAY[STRING]
STRING STRING STRING value “Alan” value “Mark” value “Tom”
STRING STRING STRING value “Alan” value “Mark” value “Tom”
STRING STRING STRING value “Alan” value “Mark” value “Tom”
ARRAY[STRING]
ARRAY[STRING]
15 of 41
Deep Copy of Collection Object (1)
1 old imp := imp.deep twin
2 Result := old_imp = imp — Result = false
3 imp[2] := “Jim” 4 Result :=
5 6
across 1 |..| imp.count is j
all imp [j] ∼ old_imp [j] end — Result = false
Before Executing L3 After Executing L3
ARRAY[STRING]
STRING STRING STRING value “Alan” value “Mark” value “Tom”
STRING STRING STRING value “Alan” value “Mark” value “Tom”
old_imp
imp
imp
old_imp
ARRAY[STRING] STRING value “Jim”
STRING STRING STRING value “Alan” value “Mark” value “Tom”
STRING STRING STRING value “Alan” value “Mark” value “Tom”
ARRAY[STRING]
ARRAY[STRING]
14 of 41
Experiment: Copying Objects
● Download the Eiffel project archive (a zip file) here:
EECS3311/codes/copying_objects.zip
● Unzip and compile the project in Eiffel Studio.
● Reproduce the illustrations explained in lectures.
https://www.eecs.yorku.ca/ ̃jackie/teaching/lectures/2020/F/
16 of 41
Part 2
Writing Complete Postconditions
17 of 41
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 ]
19 of 41
How are contracts checked at runtime?
○ All contracts are specified as Boolean expressions.
○ Right before a feature call (e.g., acc.withdraw(10)):
● Thecurrentstateofacciscalleditspre-state.
● Evaluatepre-conditionusingcurrentvaluesofattributes/queries.
● Cache values, via 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
:=
e.g., ( )
e.g., (
e.g., (old accounts)[i].id
e.g., (old accounts.twin)[i].id
e.g., (old Current).accounts[i].id e.g., ( ) [ ]
old accounts[i] .id
)
values of attributes and queries.
18of41 ● Evaluateinvariantusingcurrentvaluesofattributesandqueries.
old accounts[i].twin .id
old Current.twin .accounts i .id
○ Right after the feature call:
● Thecurrentstateofacciscalleditspost-state.
● Evaluate post-condition using both current values and “cached”
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
end end
Result :=
owner ∼ other.owner
and balance = other.balance
20 of 41
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
21 of 41
Object Structure for Illustration
We will test each version by starting with the same runtime object structure:
BANK accounts
b
b.accounts
01
“Bill” “Steve”
ACCOUNT
owner
balance
0
ACCOUNT
owner
balance
0
23 of 41
Roadmap of Illustrations
We examine 5 different versions of a command
deposit on (n ∶ STRING; a ∶ INTEGER)
VERSION
1 Correct Incomplete No
IMPLEMENTATION CONTRACTS
SATISFACTORY?
2 3 4 5
Wrong Incomplete No Wrong Complete (reference copy) No Wrong Complete (shallow copy) No Wrong Complete (deep copy) Yes
22 of 41
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
24 of 41
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
25 of 41
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.
27 of 41
Test of Version 1: Result
26 of 41
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
28 of 41
Test of Version 2: Result
29 of 41
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
31 of 41
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
30 of 41
Test of Version 3: Result
32 of 41
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
33 of 41
Test of Version 4: Result
35 of 41
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
34 of 41
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
36 of 41
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
37 of 41
Experiment: Complete Postconditions
● Download the Eiffel project archive (a zip file) here:
EECS3311/codes/array_math_contract.zip
● Unzip and compile the project in Eiffel Studio.
● Reproduce the illustrations explained in lectures.
39 of 41
https://www.eecs.yorku.ca/ ̃jackie/teaching/lectures/2020/F/
Test of Version 5: Result
38 of 41
Beyond this lecture
● 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:
○
○
○
○ accounts ∼ old accounts
○ accounts ∼ old accounts.twin
○ accounts ∼ old accounts.deep twin
● Which equality of the above is appropriate for the postcondition?
● Why is each one of the other equalities not appropriate? 40 of 41
[×] [×] [×] [×] [×]
accounts = old accounts
accounts = old accounts.twin
accounts = old accounts.deep twin
[ ✓ ]
Index (1)
Learning Objectives
Part 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)
41 of 41
Index (3)
Version 1:
Incomplete Contracts, Correct Implementation
Test of Version 1
Test of Version 1: Result
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
43 of 41
Index (2)
Shallow Copy of Collection Object (2)
Deep Copy of Collection Object (1)
Deep Copy of Collection Object (2)
Experiment: Copying Objects
Part 2
How are contracts checked at runtime?
When are contracts complete?
Account
Bank
Roadmap of Illustrations
Object Structure for Illustration
42 of 41
Index (4)
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
Experiment: Complete Postconditions
Beyond this lecture
44 of 41