Assignment 3

Submission: Upload a single .zip file named u{Student ID}.zip (e.g., u6880517.zip) to MS Teams Classroom.

Typesetting. For written questions, typeset your answers and produce a PDF named hw3.pdf; place it at the top level of your zip. We do not accept scanned or handwritten submissions. Proper typesetting means math symbols — summations, fractions, inequalities — are rendered with correct notation, bounds, and spacing, as you would see in a textbook.

Coding logistics. Your submission is graded by a script before any human reviews it. The script is unforgiving, so follow these instructions exactly:

  • Name each source file exactly as specified in the task and place it at the top level of your zip — no subdirectories.
  • Use the exact function, class, and interface names given.

AI Usage Policy. Before you begin, remind yourself of the AI usage policy and guideline on the course website. In brief: Don’t offload your learning and thinking to AI. Use AI to help you learn.

Loops & Numerical Computation (6 pts)

Written question — answer in your PDF.

Consider the Kotlin code below. We have already fleshed out a loop invariant for you. Your task is to add Hoare logic justifications so that we have a proof that mult returns the product of x and y. You may be inspired by worked examples from class.

// precondition: x >= 0 && y >= 0
fun mult(x: Int, y: Int): Int {
    var k = x; var n = y; var res = 0
    while (k != 0) { // loop_invariant: x * y == k * n + res
        if (k % 2 == 1) res = res + n
        k /= 2
        n *= 2
    }
    return res
}
// post-condition: returns x * y

Loop Invariant: Average (9 pts)

Written question — answer in your PDF.

The function below computes the average of two integers \(a\) and \(b\), i.e., \(\frac{a+b}{2}\).

// precondition: a, b ∈ ℤ,  a ≤ b
fun avg(a: Int, b: Int): Double {
    var x = 2 * a; var y = 2 * b     // { x = 2a ∧ y = 2b } ①
    while (x < y) {
    // loop_invariant: x + y = 2(a+b)  ∧  ∃ k ∈ ℤ, y − x = 2k ≥ 0
        // { ∃ x₀,y₀,k₀: x=x₀ ∧ y=y₀ ∧ y₀−x₀=2k₀ ≥ 0 } ②
        x++; y--
        // { x = x₀+1 ∧ y = y₀−1 } ③
    }
    // { x = y ∧ x = a+b } ④
    return x / 2.0
} // post-condition: returns (a+b)/2

Each numbered assertion ①–④ is a claim about the program state at that point in the execution.

(i) Initialization. Prove that the loop invariant holds before the first iteration — that is, derive it from assertion ①.

(ii) Preservation. Prove that the loop invariant is preserved by each iteration. Specifically, assume the invariant holds at the top of the loop and the loop condition x < y holds (captured in assertion ②). Show that after executing x++; y--, the invariant still holds (assertion ③ → invariant).

(iii) Termination. Prove that the loop terminates after finitely many steps. State a suitable variant (a quantity that strictly decreases on each iteration and is bounded below), prove it decreases on every iteration, and conclude that the loop must terminate. Determine exactly how many iterations the loop executes in terms of \(a\) and \(b\).

Loop Invariant: Average, Again (12 pts)

Written question — answer in your PDF.

The function below is an upgrade of avg from above. It drops the restriction \(a \leq b\) and handles arbitrary integers.

// precondition: a, b ∈ ℤ
fun fullAvg(a: Int, b: Int): Double {
    var x = 2 * a; var y = 2 * b
    while (x < y) { x++; y-- }
    while (y < x) { y++; x-- }
    return x / 2.0
} // postcondition: returns (a+b)/2

For each loop, state a loop invariant, prove initialization and preservation, and identify assertions that hold immediately after the loop exits. Then prove the postcondition. Additionally, prove that both loops terminate (be sure to state a variant for each).

Specification and Correctness (12 pts)

Written question — answer in your PDF.

Consider the following function:

/**
 * Removes duplicate integers from a list, preserving order of first appearance.
 */
fun removeDuplicates(lst: List<Int>): List<Int>

(i) Formal specification. Write a formal specification using the format, like we did in previous questions:

// precondition:  ...
// postcondition:   ...

Your postcondition clause must fully characterize the output: which elements appear, how many times, and in what order.

(ii) Implementation correctness. It turns out a teammate of yours proposes:

fun removeDuplicates(lst: List<Int>): List<Int> {
    return lst.toSet().toList()
}

Does this implementation satisfy your spec? Check each clause of your postcondition systematically. If it does not, identify the violated clause and suggest a fix.

(iii) Generalization. Now suppose the function signature is changed to accept List<Number> instead of List<Int>, allowing a mix of numeric types such as [1, 2.0, 1]. Does this require changes to your precondition or postcondition? Rewrite the spec for the generalized version, being precise about how equality is defined. (Hint: For floating-point numbers, direct equality testing is almost always a bad idea—most often, two numbers \(x\) and \(y\) are treated as equal if their difference \(|a - b|\) is very small, say, \(< 10^{-7}\).)

Implementing removeDuplicates (10 pts)

Save your work in RemoveDuplicates.kt and RemoveDuplicatesTest.kt.

Implement removeDuplicates from the previous problem — use the List<Int> signature and the spec you wrote in part (i) of that problem as your contract.

fun removeDuplicates(lst: List<Int>): List<Int> {
    // your code here
}

Your implementation must satisfy your spec. Furthermore, write a JUnit test suite in RemoveDuplicatesTest.kt that verifies your implementation.

Finally, analyze the running time of your implementation in terms of \(n = \) lst.size. State and justify a \(\Theta\) bound.

Spec-Driven Testing (15 pts)

Written question — answer in your PDF. However, all JUnit tests for this question will be shown in the PDF and also kept in SearchTest.kt; they must be real/valid Kotlin.

Below is a specification and signature for a search function:

// precondition:  arr is a list of integers sorted in non-decreasing order
// postcondition: if target appears in arr, returns an index i such that arr[i] == target;
//                otherwise, returns -1;
//                does not modify arr
fun search(arr: List<Int>, target: Int): Int

(i) Equivalence partitioning. Using the principle of equivalence partitioning, identify at least 5 distinct input partitions. For each partition, describe it in plain English, explain why all inputs in it behave the same way, and write one representative JUnit test:

@Test
fun `target present in the middle of the list`() {
    val result = search(listOf(1, 3, 5, 7, 9), 5)
    assertEquals(2, result)
}

note: Include your JUnit test in both the PDF writeup and in the specified file.

(ii) Boundary conditions. Identify at least 2 boundary conditions at the edges of your partitions. Explain why boundaries deserve their own tests even when they fall within an existing partition, then write a JUnit test for each.

note: Include your JUnit test in both the PDF writeup and in the specified file.

(iii) AI engagement. Prompt an AI assistant as follows (substituting the spec above):

“Here is a specification for a search function: [paste spec]. What input partitions would you use to test this function? Are there any edge cases I might have missed?”

Write a 1/2-page reflection covering: which partitions the AI identified that you had already found; which it found that you missed (add these to your test suite); which you found that it missed and why you think it overlooked them; and what this tells you about using AI as a testing tool — what it does well and where human judgment remains essential.

Include your AI conversation in your PDF.

Bounded Stack (20 pts)

Written question — answer in your PDF. However, all JUnit tests for this question will be shown in the PDF and also kept in BoundedStackTest.kt; they must be real/valid Kotlin.

A stack is a data structure that operates on the last-in, first-out (LIFO) principle: the item most recently added is always the first to be removed. Think of a stack of cafeteria trays — you always take from the top and always place new trays on top. The three core operations are:

  • push — place an item on top of the stack
  • pop — remove and return the top item
  • peek — inspect the top item without removing it

A bounded stack adds a fixed maximum capacity: once full, no further items may be pushed.

Below is a partial Kotlin implementation. You will specify, reason about, and test it.

class BoundedStack(val capacity: Int) {
    private val data = mutableListOf<Int>()

    /** Add item to the top of the stack. */
    fun push(item: Int): Unit { TODO() }

    /** Remove and return the top item. */
    fun pop(): Int { TODO() }

    /** Return the top item without removing it. */
    fun peek(): Int { TODO() }

    /** Return true if the stack has no elements. */
    fun isEmpty(): Boolean { TODO() }

    /** Return true if the stack has reached capacity. */
    fun isFull(): Boolean { TODO() }

    /** Return the number of elements currently in the stack. */
    fun size(): Int { TODO() }
}

(i) Representation invariants. State at least 3 representation invariants for BoundedStack — properties that must hold for every valid instance at all times, before and after every public method call. Write them as precise logical statements, e.g.:

INV1: 0 <= data.size <= capacity

(ii) Specifications. Write a full precondition / postcondition specification for push and pop. Your postconditions must go beyond “the invariants are preserved” — show concretely how the state changes while keeping each invariant intact.

(iii) Invariant-driven testing.

  • For each invariant from (i), write at least one JUnit test that would fail if that invariant were violated by a buggy implementation. Briefly explain the reasoning for each test.
  • Write a single test that exercises a push → push → pop → push sequence and asserts that all invariants hold after each step using intermediate assertions.
  • For each precondition-violating input identified in your specs, write a JUnit test using assertThrows verifying that the implementation throws an appropriate exception. Justify your choice of exception type.

(iv) Bug analysis. A classmate submits this implementation of pop:

fun pop(): Int {
    return data.last()  // does not remove the item
}

Which of your invariants (if any) does this violate, and under what conditions? Which of your tests from (iii) catches this bug — and if none do, write a new test that does.