1 of 6

CSE 331�Software Design & Implementation

​

Spring 2026

Section 5 – Arrays

2 of 6

Administrivia

  • HW4 released tonight - Due @ 11:59pm next Wed
  • Midterm next Friday (5/8)! More details on website

​

​

3 of 6

More 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 6

‘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 false if A[i] /= y for any 0 <= i < len(A)

// true otherwise

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

5 of 6

Array Mutation

  • Array mutation can change “for any” facts!

​

  • Ex:

​

{{ A[j] < A[j+1] for any 0 ≤ j ≤ 9 }}

A[0] = 100;

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

​

  • Old facts about A[0] could be invalidated!
    • Need to update the range of “for any” facts

6 of 6

Mutating Arrays (add/remove)

  • Adding to the end of an array

{{ P(A) }} {{ P(A ⧺ [100]) }}

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

{{ P(A_0) and A = A_0 ⧺ [100] }} {{ P(A) }}

​

  • Removing from the end of an array

{{ P(A) }} {{ P(A[ : len(A) - 1]) }}

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

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

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

​