3 of 40

Array Notation

Prefix: All elements from the start (inclusive) to j (exclusive):

A[ : j] = elements 0, ..., j - 1
Like python array slice

Suffix: All elements starting at j (inclusive) to the end:

A[j : ] = elements j, …, end

Thus, A[ : j] ++ A[j : ] = A

Other useful facts:

A[len(A) : ] = nil
A[ : 0] = nil
A[ : j] ⧺ [A[j]] = A[ : j + 1]
A[ : len(A)] = A

4 of 40

‘For Any’ Facts

Necessary facts about arbitrary parts of an array

Ex: To show an array is sorted in ascending order:

A[i] < A[i+1] for any 0 ≤ i < len(A) – 1

// @requires A[i] < A[i+1] for any 0 <= i < len(A)-1

// @returns true if A[i] == y for any 0 <= i < len(A)

// false otherwise

public boolean bsearch(int[] A, int y) { … }

5 of 40

Array Mutation

Array mutation can change “for any” facts!

A[0] = 100;

{{ (A[j] < A[j+1] for any 1 ≤ j ≤ 9) and A_0[0] < A[1] and A[0] = 100 }}

Old facts about A[0] could be invalidated!

Need to update the range of “for any” facts

6 of 40

Mutating Arrays (add/remove)

Adding to the end of an array

A.add(100); A.add(100);

Removing from the end of an array

A.remove(A.size()-1); A.remove(A.size()-1);

{{ P(A_0) and {{ P(A) }}

A = A_0[ : len(A_0) – 1] }}

7 of 40

Task 1 – Tw-Y’s Removed

Considering the following method specification:

/**

* Removes all instances of an int from the provided array, writing

* the remaining elements into the first j indicies and returning j.

* @param y the int to remove

* @param arr the array to remove from

* @requires arr != null

* @modifies arr

* @effects arr[: j] holds all the non-y elements in arr

* @returns j the length of the non-y elements in arr

public static int remove(int[] arr, int y);

In this problem, we will check the correctness of the following code that implements remove.

8 of 40

Task 1 – Tw-Y’s Removed

Fill in P1 using forward reasoning and then prove that P1 implies Inv.

public static int remove(int[] arr, int y) {

int i = 0;

int j = 0;

{{ P1: ______________________________________________________________ }}

{{ Inv: arr[: j] contains all non-y elements from arr_0[: i] and

arr[i :] = arr_0[i :] and length of arr = length of arr_0 }}

9 of 40

Task 1 – Tw-Y’s Removed

Fill in P1 using forward reasoning and then prove that P1 implies Inv.

public static int remove(int[] arr, int y) {

int i = 0;

int j = 0;

{{ Inv: arr[: j] contains all non-y elements from arr_0[: i] and

arr[i :] = arr_0[i :] and length of arr = length of arr_0 }}

10 of 40

Task 1 – Tw-Y’s Removed

Fill in P1 using forward reasoning and then prove that P1 implies Inv.

public static int remove(int[] arr, int y) {

int i = 0;

int j = 0;

{{ Inv: arr[: j] contains all non-y elements from arr_0[: i] and

arr[i :] = arr_0[i :] and length of arr = length of arr_0 }}

The first fact of Inv holds since:

arr[: j] = arr[: 0] since j = 0

= nil

= arr_0[: 0]

= arr_0[: i] since i = 0

Since j is 0, arr[: j] is the empty array. The same holds for i = 0, so arr_0[: i] is also the empty array. There cannot be any non-y elements in the empty array, so this fact clearly holds.

11 of 40

Task 1 – Tw-Y’s Removed

Fill in P1 using forward reasoning and then prove that P1 implies Inv.

public static int remove(int[] arr, int y) {

int i = 0;

int j = 0;

{{ Inv: arr[: j] contains all non-y elements from arr_0[: i] and

arr[i :] = arr_0[i :] and length of arr = length of arr_0 }}

The second fact of Inv holds since:

arr[i :] = arr[0 :] since i = 0

= arr

= arr_0 since arr = arr_0

= arr_0[0 :]

= arr_0[i :] since i = 0

Since i is 0, arr_0[i :] = arr_0. Since arr has not been modified, arr = arr_0. We know that arr_0 = arr_0[0 :], and so arr_0[i :] = arr[i :]

12 of 40

Task 1 – Tw-Y’s Removed

Fill in P1 using forward reasoning and then prove that P1 implies Inv.

public static int remove(int[] arr, int y) {

int i = 0;

int j = 0;

{{ Inv: arr[: j] contains all non-y elements from arr_0[: i] and

arr[i :] = arr_0[i :] and length of arr = length of arr_0 }}

The third fact of Inv holds since:

length of arr = length of arr_0 since arr = arr_0

Since arr has not been reassigned, the length of arr = length of arr_0.

13 of 40

Task 1 – Tw-Y’s Removed

b) Fill in P4 using forward reasoning and then prove that P4 implies the postcondition.

{{ Inv: arr[: j] contains all non-y elements from arr_0[: i] and

arr[i :] = arr_0[i :] and length of arr = length of arr_0 }}

while (i != arr.length) {

...

}

{{ P4: ______________________________________________________________ }}

return j;

14 of 40

Task 1 – Tw-Y’s Removed

b) Fill in P4 using forward reasoning and then prove that P4 implies the postcondition.

{{ Inv: arr[: j] contains all non-y elements from arr_0[: i] and

arr[i :] = arr_0[i :] and length of arr = length of arr_0 }}

while (i != arr.length) {

...

}

{{ P4: Inv (arr[: j] contains all non-y elements from arr_0[: i] and

arr[i :] = arr_0[i :] and length of arr = length of arr_0) and

i = arr.length }}

return j;

15 of 40

Task 1 – Tw-Y’s Removed

b) Fill in P4 using forward reasoning and then prove that P4 implies the postcondition.

{{ Inv: arr[: j] contains all non-y elements from arr_0[: i] and

arr[i :] = arr_0[i :] and length of arr = length of arr_0 }}

while (i != arr.length) {

...

}

{{ P4: Inv (arr[: j] contains all non-y elements from arr_0[: i] and

arr[i :] = arr_0[i :] and length of arr = length of arr_0) and

i = arr.length }}

return j;

This gives us the postcondition as:

Since i = arr.length and arr.length = arr_0.length, i = arr_0.length. Thus, arr_0[: i] = arr_0[: arr_0.length] = arr_0. Since we have that arr[: j] contains all non-y elements from arr_0[: i], we see that arr[: j] contains all non-y elements from arr_0.

16 of 40

Task 1 – Tw-Y’s Removed

c) Fill in P2 using forward reasoning and Q2 using backward. Then, prove that P2 implies Q2.

{{ Inv: arr[: j] contains all non-y elements from arr_0[: i] and

arr[i :] = arr_0[i :] and length of arr = length of arr_0 }}

while (i != arr.length) {

if (arr[i] == y) {

} else {

...

}

i = i + 1;

}

17 of 40

Task 1 – Tw-Y’s Removed

c) Fill in P2 using forward reasoning and Q2 using backward. Then, prove that P2 implies Q2.

{{ Inv: arr[: j] contains all non-y elements from arr_0[: i] and

arr[i :] = arr_0[i :] and length of arr = length of arr_0 }}

while (i != arr.length) {

if (arr[i] == y) {

{{ P2: Inv (arr[: j] contains all non-y elements from arr_0[: i] and

arr[i :] = arr_0[i :] and length of arr = length of arr_0) and

i != arr.length, and arr[i] = y }}

} else {

...

}

i = i + 1;

}

18 of 40

Task 1 – Tw-Y’s Removed

c) Fill in P2 using forward reasoning and Q2 using backward. Then, prove that P2 implies Q2.

{{ Inv: arr[: j] contains all non-y elements from arr_0[: i] and

arr[i :] = arr_0[i :] and length of arr = length of arr_0 }}

while (i != arr.length) {

if (arr[i] == y) {

{{ P2: Inv (arr[: j] contains all non-y elements from arr_0[: i] and

arr[i :] = arr_0[i :] and length of arr = length of arr_0) and

i != arr.length, and arr[i] = y }}

{{ Q2: arr[: j] contains all non-y elements from arr_0[: i+1] and

arr[i+1 :] = arr_0[i+1 :] and length of arr = length of arr_0}}

} else {

...

}

i = i + 1;

}

19 of 40

Task 1 – Tw-Y’s Removed

c) Fill in P2 using forward reasoning and Q2 using backward. Then, prove that P2 implies Q2.

{{ P2: Inv (arr[: j] contains all non-y elements from arr_0[: i] and

arr[i :] = arr_0[i :] and length of arr = length of arr_0) and

i != arr.length, and arr[i] = y }}

{{ Q2: arr[: j] contains all non-y elements from arr_0[: i+1] and

arr[i+1 :] = arr_0[i+1 :] and length of arr = length of arr_0}}

The first part follows since:

Since arr[i :] = arr_0[i :], arr[i] = arr_0[i]. This gives us arr[i] = arr_0[i] = y, meaning arr_0[i] is not a non-y element. Since arr[: j] contains all non-y elements in arr_0[: i] and arr_0[i] = y, we also know that arr[: j] contains all non-y elements from arr_0[: i+1].

The second part of Q2 is implied by the second fact from P2 (since arr[i+1 :] is a sublist of arr[i :] and the same for arr_0).

The third fact is directly implied.

20 of 40

Task 1 – Tw-Y’s Removed

d) Fill in P3 using forward reasoning and Q3 using backward. Then, prove that P3 implies Q3.

{{ Inv: arr[: j] contains all non-y elements from arr_0[: i] and

arr[i :] = arr_0[i :] and length of arr = length of arr_0 }}

while (i != arr.length) {

if (arr[i] == y) {

...

} else {

arr[j] = arr[i];

j = j + 1;

}

i = i + 1;

}

21 of 40

Task 1 – Tw-Y’s Removed

d) Fill in P3 using forward reasoning and Q3 using backward. Then, prove that P3 implies Q3.

{{ Inv: arr[: j] contains all non-y elements from arr_0[: i] and

arr[i :] = arr_0[i :] and length of arr = length of arr_0 }}

while (i != arr.length) {

if (arr[i] == y) {

...

} else {

{{ P3: Inv (arr[: j] contains all non-y elements from arr_0[: i] and

arr[i :] = arr_0[i :] and length of arr = length of arr_0), and

i != len(arr) and arr[i] != y }}

arr[j] = arr[i];

j = j + 1;

}

i = i + 1;

}

22 of 40

Task 1 – Tw-Y’s Removed

d) Fill in P3 using forward reasoning and Q3 using backward. Then, prove that P3 implies Q3.

{{ Inv: arr[: j] contains all non-y elements from arr_0[: i] and

arr[i :] = arr_0[i :] and length of arr = length of arr_0 }}

while (i != arr.length) {

if (arr[i] == y) {

...

} else {

{{ P3: Inv (arr[: j] contains all non-y elements from arr_0[: i] and

arr[i :] = arr_0[i :] and length of arr = length of arr_0), and

i != len(arr) and arr[i] != y }}

{{ Q3: (arr[: j] ++ arr[i] contains all non-y elements from arr_0[: i+1] and

arr[i+1 :] = arr_0[i+1 :] and length of arr = length of arr_0) }}

arr[j] = arr[i];

j = j + 1;

}

i = i + 1;

}

23 of 40

Task 1 – Tw-Y’s Removed

d) Fill in P3 using forward reasoning and Q3 using backward. Then, prove that P3 implies Q3.

{{ P3: Inv (arr[: j] contains all non-y elements from arr_0[: i] and

arr[i :] = arr_0[i :] and length of arr = length of arr_0), and

i != len(arr) and arr[i] != y }}

{{ Q3: (arr[: j] ++ arr[i] contains all non-y elements from arr_0[: i+1] and

arr[i+1 :] = arr_0[i+1 :] and length of arr = length of arr_0) }}

The first fact follows since:

Since arr[i :] = arr_0[i :], arr[i] = arr_0[i]. Thus, arr[i] = arr_0[i] != y and arr[i] must be included in the non-y elements for arr_0[: i+1]. Since arr[: j] contains all non-y elements from arr_0[: i], concatenating arr[: j] ++ arr[i] would also contains all non-y elements from arr_0[: i + 1]. Thus, fact 1 holds.

The second part of Q3 is implied by the second fact from P3 (since arr[i+1 :] is a sublist of arr[i :]).

The third fact is directly implied.

24 of 40

Task 2 – Rally the Loops

/**

* Writes over each copy of y in A with the value z.

* @param A the array to replace values in

* @param y the value to be replaced in A

* @param z the value to replace y with in A

* @modifies A

* @effects A = A_0 with every instance of y replaced

* with a z

public void replace(int[] A, int y, int z) { .. }

In this problem, we’ll be implementing the following function:

25 of 40

Task 2 – Rally the Loops

int i = ____________________

// Inv: A[0 : i] = A_0[0 : i] with every y replaced with a z

// and A[i : ] = A_0[i : ]

while (________________________________________) {

}

Fill in the missing parts of the code, to make it correct with the given invariant:

26 of 40

Task 2 – Rally the Loops

int i = 0;

// Inv: A[0 : i] = A_0[0 : i] with every y replaced with a z

// and A[i : ] = A_0[i : ]

while ( i < A.length ) {

}

Fill in the missing parts of the code, to make it correct with the given invariant:

27 of 40

Task 2 – Rally the Loops

int i = 0;

// Inv: A[0 : i] = A_0[0 : i] with every y replaced with a z

// and A[i : ] = A_0[i : ]

while ( i < A.length ) {

if (A[i] == y) {

A[i] = z;

}

i++;

}

Fill in the missing parts of the code, to make it correct with the given invariant:

28 of 40

Task 2 – Rally the Loops

int i = ____________________

// Inv: A[0 : i] = A_0[0 : i] and A[i : ] = A_0[i : ] with

// every y replaced with a z

while (________________________________________) {

}

Fill in the missing parts of the code, to make it correct with the given invariant:

29 of 40

Task 2 – Rally the Loops

int i = A.length;

// Inv: A[0 : i] = A_0[0 : i] and A[i : ] = A_0[i : ] with

// every y replaced with a z

while ( i > 0 ) {

}

Fill in the missing parts of the code, to make it correct with the given invariant:

30 of 40

Task 2 – Rally the Loops

int i = A.length;

// Inv: A[0 : i] = A_0[0 : i] and A[i : ] = A_0[i : ] with

// every y replaced with a z

while ( i > 0 ) {

i--;

if (A[i] == y) {

A[i] = z;

}

Fill in the missing parts of the code, to make it correct with the given invariant:

31 of 40

Testing - Review

• Statement Coverage

Test every executable statement reachable by an allowed input

• Branch Coverage

For every conditional, test all branches for allowed inputs

• Loop Coverage

Every loop/recursive call must be tested on 0, 1, any 2+ iterations for allowed inputs

• Exhaustive Testing

Test all possible inputs for functions with <= 10 allowed inputs

32 of 40

Mutable Testing

Must also test that mutated values were updated correctly.

For ADT’s, check obj before and after method calls
When taking in parameters, make sure they are updated according to the spec

33 of 40

Task 3 – Test, Ice, Compression, Elevation

/**

* Join the two given lists into a single one

* @requires first != null, second != null

* @returns first concatenated with second

public static List<Integer> join(List<Integer> first,

List<Integer> second) {

List<Integer> newList = new ArrayList<>();

newList.addAll(first);

newList.addAll(second);

return newList;

}

a) First, consider a version of join, which does not mutate either argument:

34 of 40

Task 3 – Test, Ice, Compression, Elevation

public static List<Integer> join(List<Integer> first,

List<Integer> second) {

List<Integer> newList = new ArrayList<>();

newList.addAll(first);

newList.addAll(second);

return newList;

}

Fill in the missing parts of the JUnit test for join:

@Test

public void testJoin(){

List<Integer> list1 = new ArrayList<>(Arrays.asList(1, 2));

List<Integer> list2 = new ArrayList<>(Arrays.asList(3, 4));

assertEquals(________________________, join(list1, list2));

List<Integer> list3 = new ArrayList<>(Arrays.asList(1));

List<Integer> list4 = new ArrayList<>(Arrays.asList(2, 3, 4));

assertEquals(________________________, join(list3, list4));

}

35 of 40

Task 3 – Test, Ice, Compression, Elevation

public static List<Integer> join(List<Integer> first,

List<Integer> second) {

List<Integer> newList = new ArrayList<>();

newList.addAll(first);

newList.addAll(second);

return newList;

}

Fill in the missing parts of the JUnit test for join:

@Test

public void testJoin(){

List<Integer> list1 = new ArrayList<>(Arrays.asList(1, 2));

List<Integer> list2 = new ArrayList<>(Arrays.asList(3, 4));

assertEquals(Arrays.asList({1, 2, 3, 4}), join(list1, list2));

List<Integer> list3 = new ArrayList<>(Arrays.asList(1));

List<Integer> list4 = new ArrayList<>(Arrays.asList(2, 3, 4));

assertEquals(________________________, join(list3, list4));

}

36 of 40

Task 3 – Test, Ice, Compression, Elevation

public static List<Integer> join(List<Integer> first,

List<Integer> second) {

List<Integer> newList = new ArrayList<>();

newList.addAll(first);

newList.addAll(second);

return newList;

}

Fill in the missing parts of the JUnit test for join:

@Test

public void testJoin(){

List<Integer> list1 = new ArrayList<>(Arrays.asList(1, 2));

List<Integer> list2 = new ArrayList<>(Arrays.asList(3, 4));

assertEquals(Arrays.asList({1, 2, 3, 4}), join(list1, list2));

List<Integer> list3 = new ArrayList<>(Arrays.asList(1));

List<Integer> list4 = new ArrayList<>(Arrays.asList(2, 3, 4));

assertEquals(Arrays.asList({1, 2, 3, 4}), join(list3, list4));

}

37 of 40

Task 3 – Test, Ice, Compression, Elevation

/** Join the two given lists into a single one

* @requires first != null, second != null

* @requires first != second

* @modifies first

* @effects first is first_0 concatenated with second

public static void join(List<Integer> first,

List<Integer> second) {

first.addAll(second);

}

b) Next, consider the following version of join, which mutates first and does not return anything

Rewrite the JUnit test to use this new definition of join on the same inputs as above.

38 of 40

Task 3 – Test, Ice, Compression, Elevation

@Test

public void testJoin(){

}

39 of 40

Task 3 – Test, Ice, Compression, Elevation

@Test

public void testJoin(){

List<Integer> list1 = new ArrayList<>(Arrays.asList(1, 2));

List<Integer> list2 = new ArrayList<>(Arrays.asList(3, 4));

join(list1, list2);

assertEquals(Arrays.asList(1, 2, 3, 4), list1);

}

40 of 40

Task 3 – Test, Ice, Compression, Elevation

@Test

public void testJoin(){

List<Integer> list1 = new ArrayList<>(Arrays.asList(1, 2));

List<Integer> list2 = new ArrayList<>(Arrays.asList(3, 4));

join(list1, list2);

assertEquals(Arrays.asList(1, 2, 3, 4), list1);

List<Integer> list3 = new ArrayList<>(Arrays.asList(1));

List<Integer> list4 = new ArrayList<>(Arrays.asList(2, 3, 4));

join(list3, list4);

assertEquals(Arrays.asList(1, 2, 3, 4), list3);

}