Last updated on Thursday, October 09, 2025

Week 4: Polymorphism, Proofs and Tests

Welcome to week 4 of CS-214 — Software Construction!

This exercise set is intended to help you practice lists, polymorphism, equational reasoning and testing.

As usual, ⭐️ indicates the most important exercises and questions; 🔥, the most challenging ones; and 🔜, the ones that are useful to prepare for future lectures. Exercises or questions marked 🧪 are intended to build up to concepts used in this week’s lab.

You do not need to complete all exercises to succeed in this class, and you do not need to do all exercises in the order they are written.

Polymorphism

Warm-up: Polymorphic Lists ⭐️

In previous exercises and labs, we used IntList for lists whose elements are integers. This week, we’ll move to polymorphic lists.

Polymorphic lists can be defined as an algebraic data type in the following way:

enum MyList[+A]:
  case Nil
  case Cons(x: A, xs: MyList[A])

We’ll use the above MyList type in this exercise.

def isEmpty: Boolean = this match
  case Nil => true
  case _   => false

def head: A = this match
  case Nil        => throw EmptyListException()
  case Cons(x, _) => x

def tail: MyList[A] = this match
  case Nil         => throw EmptyListException()
  case Cons(_, xs) => xs

Functions on Polymorphic Lists ⭐️

Part 1: Higher-order functions

Common Operators on Lists

In previous weeks, we have implemented higher-order functions on IntLists. For example, map was defined as:

def map(l: IntList)(f: Int => Int): IntList =
  l match
    case IntNil         => IntNil
    case IntCons(x, xs) => IntCons(f(x), map(xs)(f))

In contrast, the generic version of the function map (whose type consists of type parameters instead of concrete types like IntList and Int => Int) has the following signature:

def map[A, B](l: MyList[A])(f: A => B): MyList[B]

1. Based on the example above, write a generic signature for filter, foldRight, reduceRight, forall, exists, zip, and zipWith.

   Check Yourself

   def map[A, B](l: MyList[A])(f: A => B): MyList[B] =
     ???
   
   def filter[A](l: MyList[A])(p: A => Boolean): MyList[A] =
     ???
   
   def foldRight[A, B](l: MyList[A])(f: (A, B) => B, base: B): B =
     ???
   
   def reduceRight[A](l: MyList[A])(f: (A, A) => A): A =
     ???
   
   def forall[A](l: MyList[A])(p: A => Boolean): Boolean =
     ???
   
   def exists[A](l: MyList[A])(p: A => Boolean): Boolean =
     ???
   
   def zip[A, B](l1: MyList[A], l2: MyList[B]): MyList[(A, B)] =
     ???
   
   def zipWith[A, B, C](l1: MyList[A], l2: MyList[B])(op: (A, B) => C): MyList[C] =
     ???
   

   polymorphism/src/main/scala/poly/MyListOps.scala

2. In previous exercises, we had separate implementations for foldRight and foldRightList (we had to handle the cases of returning an integer and returning an IntList separately).

   Do we need to define a similar foldRightList on polymorphic lists?

   Check Yourself

   No, type variable B can be instantiated to MyList[Int].

3. Implement these eight higher-order functions (map plus all other ones above) on MyList using pattern matching.

Using List APIs

Use the list APIs to:

1. Implement function elementsAsStrings which converts every element of a list to a string (you may need the .toString function):

   def elementsAsStrings[A](l: MyList[A]): MyList[String] =
     ???
   

   polymorphism/src/main/scala/poly/MyListOps.scala

2. Reimplement functions from previous exercises on polymorphic lists:

   def length[A](l: MyList[A]): Int =
     ???
   
   def takeWhilePositive(l: MyList[Int]): MyList[Int] =
     ???
   
   def last[A](l: MyList[A]): A =
     ???
   

   polymorphism/src/main/scala/poly/MyListOps.scala

3. Adapt the string functions capitalizeString and wordCount to operate on lists of characters:

   val capitalizeString: MyList[Char] => MyList[Char] =
     TODO
   
   def wordCount(l: MyList[Char]): Int =
     ???
   

   polymorphism/src/main/scala/poly/MyListOps.scala

   Beware: the solution we gave in week 1 for wordCount doesn’t express itself naturally as a fold… 🔥 try to look for a different one!

   Strings and Lists

   Both String and List[Char] or MyList[Char] represent sequences of characters. However, it’s usually more efficient and convenient to use String for text processing and manipulation in Scala because String has optimized storage for texts and rich APIs tailored for text operations.

   Later this year, we will see a more general trait that covers both Lists and Strings. This will allow us to write unified code for both.

Part 2: More functions: flatMap and cross-product

flatMap

You may have come across flatMap, a powerful higher-order function that can be used to transform and flatten container datatypes, such as lists.

def flatMap[A, B](l: MyList[A])(f: A => MyList[B]): MyList[B] =
  ???

The idea of flatMap(f)(l) is:

• Map: apply a function f to each element of the list l, where f returns a list;
• Flatten: concatenate all the resulting lists into a single list.

For example,

object FlatMapExamples:
  val numbers: MyList[Int] = Cons(2, Cons(3, Nil))

  val mapped = map(numbers)((n: Int) =>
    Cons(n, Cons(n * 2, Nil))
  )
  // For simplicity, we write Cons as `::` in the results.
  // Result: (2 :: 4 :: Nil) :: (3 :: 6 :: Nil)

  val flatMapped = flatMap(numbers)((n: Int) =>
    Cons(n, Cons(n * 2, Nil))
  )
  // Result: 2 :: 4 :: 3 :: 6 :: Nil

1. Implement flatMap. You may use the append function that we included in the starting code.

2. Implement flatten using flatMap. flatten takes a list of lists, and returns the concatenation of all the lists list:

   def flatten[A](l: MyList[MyList[A]]): MyList[A] =
     ???
   

   polymorphism/src/main/scala/poly/MyListOps.scala

Cross product

The cross-product function, often referred to as the Cartesian product, produces all possible pairs (combinations) of elements from two lists.

def crossProduct[A, B](l1: MyList[A], l2: MyList[B]): MyList[(A, B)] =
  ???

For example, given a list of main dishes and a list of side dishes, we can use crossProduct to generate all possible meal combinations:

object CrossProductExamples:
  val mains = Cons("burger", Cons("Pizza", Cons("Pasta", Nil)))
  val sides = Cons("Salad", Cons("Soup", Nil))

  val meals = crossProduct(mains, sides)
  // Result:
  // ("burger", "Salad") :: ("burger", "Soup") :: ("Pizza", "Salad") ::
  // ("Pizza", "Soup") :: ("Pasta", "Salad") :: ("Pasta", "Soup") :: Nil

• Implement crossProduct using map and flatMap.

Permutations

The distinctPairs function produces all pairs of two distinct elements from a given list. That is, all possible two-elements combinations where the elements are different.

def distinctPairs[A](items: MyList[A]): MyList[(A, A)] =
  ???

For example:

object PermutationsExamples:
  val items = Cons('a', Cons('b', Cons('c', Nil)))
  val pairs = distinctPairs(items)
  // Result:
  // ("a", "b") :: ("a", "c") :: ("b", "a") :: ("b", "c") ::
  // ("c", "a") :: ("c", "b") :: Nil

Implement distinctPairs using flatMap. You can assume elements in the input are not repeated (i.e. the same element cannot appear twice in the input).

Option Type ⭐

In last week’s exercises, we used a custom type LookupResult for the result of looking up in a context:

enum LookupResult:
  case Ok(v: Int)
  case NotFound

It’s always good to explore the Scala standard library. After all, why use a custom type when there is something suitable in the standard library?

Can you find a suitable type for LookupResult?

One suitable choice is already given by the title: the Option type!

Part 1. Basic Usage

The basic usage of the Option type is as the return type of functions that might not always return a valid value.

Implement findFirstEvenNumber to return the first even number in the list, or None if there isn’t one.

def findFirstEvenNumber(l: MyList[Int]): Option[Int] =
  ???

Part 2. Drawing Parallels with List in Standard Library

Notice that Option also has map, flatMap, filter just like List. Do you know why?

In this part, we use the List (scala.collection.immutable.List) from the standard library.

You can compare the definition of map, flatMap and filter in the standard library List methods with Option’s. Do the definitions line up? What’s the difference between the definitions on scala.collection.immutable.List and our custom polymorphic lists poly.MyList?

1. Implement parseStringToInt and findSquareRoot. Then, define findSquartRootFromString to chain these two functions to parse a string and find its square root.

   def parseStringToInt(s: String): Option[Int] =
     ???
   
   def findSquareRoot(n: Int): Option[Double] =
     ???
   
   def findSquareRootFromString(s: String): Option[Double] =
     ???
   

   polymorphism/src/main/scala/poly/RevisitOption.scala

2. 🔜 Given a list of strings representing integers:

   val numberStrings: List[String] = List("1", "2", "star", "4")
   

   Try to use map to convert them into integers. What issues do you face?

   Now, use the member method flatMap of scala.collection.immutable.List and the parseStringToInt function to safely convert them.

   val numbers =
     TODO
   

   polymorphism/src/main/scala/poly/RevisitOption.scala

   Check Yourself 🔥

   Can you do the same trick using our custom lists poly.MyList and definition of flatMap instead? Why or why not?

   Solution

   No.

   The fact that we can line up List and Option easily is because in the standard library, both List and Option are subtypes of IterableOnce, and signatures of useful methods make use of the supertype InterableOnce. For example, the signature of flatMap in List is def flatMap[B](f: A => IterableOnce[B]): List[B].

   We will cover this more advanced API at two points later in the course: first to introduce comprehensions, and then more generally monads.

FoldLeft and Tail Recursion 🧪

We say that a function is tail recursive if the last thing it does along all of its code paths is to call itself. For example, the following function is not tail recursive:

def length0(l: MyList[Int]): Int = l match
  case Nil         => 0
  case Cons(x, xs) => 1 + length0(xs)

Indeed, after calling itself recursively, the function length0 adds one to its own result.

In contrast, the inner loop function below is tail recursive:

def lengthTR(l: MyList[Int]): Int =
  def length(l: MyList[Int], prefixLength: Int): Int = l match
    case Nil         => prefixLength
    case Cons(x, xs) => length(xs, prefixLength + 1)
  length(l, 0)

Indeed, it does not do anything further after calling itself with an incremented prefixLength. This property allows the compiler to optimize the recursion completely: the function named length above will in fact be converted to a simple for loop by the compiler.

🔜 We will learn much more about tail recursion in week 11.

Reasoning about tail recursion

Use the substitution method to evaluate length0 and lengthTR on various inputs. Do they return the same thing? Can you conjecture an equation relating the inner length function to length0?

Sum

1. Is the following function tail-recursive?

   def sum0(l: MyList[Int]): Int = l match
     case Nil         => 0
     case Cons(x, xs) => x + sum0(xs)
   

   polymorphism/src/main/scala/poly/MyListOps.scala

2. What happens if you uncomment and run the following test, which runs sum0 on a list with 50000 elements?

   // test("sum0: large list"):
   //   assertEquals(sum0(manyNumbers1), N)
   

   polymorphism/src/test/scala/poly/MyListOpsTest.scala

3. Can you think of a tail-recursive way to write sum?

   def sum1(l: MyList[Int]): Int =
     // @tailrec // Uncomment this line.
     def sum(l: MyList[Int], acc: Int): Int =
     ???
     sum(l, 0)
   

   polymorphism/src/main/scala/poly/MyListOps.scala

   In Scala, the @tailrec annotation is a directive for the compiler, indicating that the annotated method should be tail-recursive. If the method is not tail-recursive, the compiler will raise a compile-time error.

4. What happens if you run sum1 with a very long list?

FoldLeft

Similar to foldRight, foldLeft processes the list from the leftmost (head) element to the rightmost element.

The main difference between foldLeft and foldRight is that foldLeft is typically implemented using tail recursion, while foldRight is the opposite.

1. Define foldLeft:

   // @tailrec // Uncomment this line.
   def foldLeft[A, B](l: MyList[A])(base: B, f: (B, A) => B): B =
     ???
   

   polymorphism/src/main/scala/poly/MyListOps.scala

2. Define sum0Fold using foldRight, define sum1Fold using foldLeft:

   def sum0Fold(l: MyList[Int]): Int =
     ???
   def sum1Fold(l: MyList[Int]): Int =
     ???
   

   polymorphism/src/main/scala/poly/MyListOps.scala

3. Reimplement reverseAppend using foldLeft:

   def reverseAppend[A](l1: MyList[A], l2: MyList[A]): MyList[A] =
     ???
   

   polymorphism/src/main/scala/poly/MyListOps.scala

4. Implement countEven and totalLength using foldLeft. CountEven takes a list of integers and returns the number of even integers in the list; totalLength takes a list of strings and returns the sum of each string’s length.

   val countEven: MyList[Int] => Int =
     TODO
   
   val totalLength: MyList[String] => Int =
     TODO
   

   polymorphism/src/main/scala/poly/MyListOps.scala

Currying and Composition

CurriedZipWith

Use map and zip to implement the curried version curriedZipWith of zipWith.

// A polymorphic method:
def foo[A](xs: MyList[A]): MyList[A] = ???

// A polymorphic function value:
val bar = [A] => (xs: MyList[A]) => foo(xs)

val curriedZipWith: [A, B, C] => ((A, B) => C) => MyList[A] => MyList[B] => MyList[C] =
  TODO

Polymorphic Composition 🔥

1. In previous exercises we defined a function compose to compose functions f: Int => Double and g: Double => String. Generalize this function to arbitrary pairs of types, using polymorphic argument types.

2. What is the neutral element for the generalized compose?

3. In previous exercises, we defined andLifter and notLifter for functions on Int. To make it more general, we can define andLifter for functions of arbitrary input types:

   def andLifter[A](f: A => Boolean, g: A => Boolean): A => Boolean =
     a => f(a) && g(a)
   

   polymorphism/src/main/scala/poly/fun.scala

   … and we can generalize further! Look at the following four functions; do they have anything in common?

   def orLifter[A](f: A => Boolean, g: A => Boolean): A => Boolean =
     a => f(a) || g(a)
   def sumLifter[A](f: A => Int, g: A => Int): A => Int =
     a => f(a) + g(a)
   def listConcatLifter[A, B](f: A => MyList[B], g: A => MyList[B]): A => MyList[B] =
     a => f(a) ++ g(a)
   

   polymorphism/src/main/scala/poly/fun.scala

   Write a binaryLifter higher-order function to capture the common pattern above, and use it to rewrite all four lifters that we’ve seen up to this point.

   def binaryLifter[A, B, C](f: A => B, g: A => B)(op: (B, B) => C): A => C =
     ???
   

   polymorphism/src/main/scala/poly/fun.scala

   def andLifter1[A](f: A => Boolean, g: A => Boolean) =
     ???
   
   def orLifter1[A](f: A => Boolean, g: A => Boolean) =
     ???
   
   def sumLifter1[A](f: A => Int, g: A => Int) =
     ???
   
   def listConcatLifter1[A, B](f: A => MyList[B], g: A => MyList[B]) =
     ???
   

   polymorphism/src/main/scala/poly/fun.scala

4. Similarly, we can implement a unaryLifter to generate lifters like notLifter. Can you tell which function unaryLifter essentially is?

Abstracting over recursion: recursors and inductions principles 🔥

The story of CS-214 is one of increasingly modular code: at this point, we’ve learned to abstract over functions (HOFs), types (polymorphism) and now we’ll even see how to abstract over effects.

As a little introduction to abstracting over effects, let’s see how to abstract over what happens when we make a recursive call.

A weak recursor for simple recursion

When we do a proof by induction on numbers, lists, or trees, we use an “induction principle” to separately consider the base case (0, empty list, leaf) and the inductive case ($n + 1$, h :: t, Branch(l, r)). In the inductive case, the induction principle gives us an induction hypothesis IH: in weak induction this hypothesis gives us a proof for our direct predecessors ($n$, t, l and r), and in strong induction it gives us a proof for all “smaller” objects (smaller numbers, shorter lists, smaller trees).

When we write recursive functions, we also have a base case (0, empty list, leaf, …) and an inductive case ($n + 1$, h :: t, Branch(l, r)), but we don’t typically use a general “recursion principle”. Let’s remediate that!

Formally, a (weak) recursion principle (or recursor) for a type T is one that allows to define functions over T by providing multiple non-recursive functions: one for each base case, and one for each recursive case (taking as arguments the result of the recursive call on the direct children/predecessors of the current value).

For example, the function wow below:

def wow(n: Int): String =
  if n == 0 then "" // base case
  else "!" + wow(n - 1) // recursive case

… can be rewritten like this:

val wowComb: Int => String = natRec("")(acc => "!" + acc)

… using the following natRec combinator:

def natRec[T](baseCase: => T)(recCase: T => T)(n: Int): T =
  if n == 0 then baseCase
  else recCase(natRec(baseCase)(recCase)(n - 1))

1. How would you define the function even using natRec?

   def even(n: Int): Boolean =
     if n == 0 then true // base case
     else !even(n - 1) // recursive case
   

   polymorphism/src/main/scala/poly/Combinator.scala

   val evenComb: Int => Boolean =
     cs214.TODO
   

   polymorphism/src/main/scala/poly/Combinator.scala

2. Write a weak recursion principle for, List[T], and Tree[T] defined below. They should be such that you can define the following functions using them:

   val increment =
     listRec[Int, List[Int]](Nil)((h, acc) => h + 1 :: acc)
   

   polymorphism/src/main/scala/poly/Combinator.scala

   val allPositive =
     listRec[Int, Boolean](true)((h, acc) => h > 0 && acc)
   

   polymorphism/src/main/scala/poly/Combinator.scala

3. Use these combinators to define a few additional functions, to get a feel of how they work.

4. Do you know listRec and treeRec under a different name?

5. What would a strong recursion principle look like?

Proofs on Lists and Trees

Proofs on lists

Composition of maps ⭐️

Prove that the following equivalence holds by using inductive reasoning:

∀ (l: List[T]),
  l.map(f).map(g) === l.map(f `andThen` g)

(∀ is short for “for all”, so the statement above says: “for all lists l of type List[T], l.map(f).map(g) equals l.map(f `andThen` g)”.)

Here are the relevant axioms for this proof:

1. Nil.map(f) === Nil
2. (x :: xs).map(f) === f(x) :: (xs.map(f))
3. (f `andThen` g)(x) === g(f(x))

Be very precise in your proof:

• Make sure to state what you want to prove, and what your induction hypothesis is, if any.
• Clearly state which axiom you use at each step, and when/if you use the induction hypothesis.
• Use only one axiom / hypothesis at each step: applying two axioms requires two steps.
• Underline the part of each expression on which you apply the axiom or hypothesis at each step.

A more complicated proof (FP midterm 2016)

We want to implement a function sum(list: List[Int]): Int, which returns the sum of the elements of a list of Int-s. We can easily specify that function as follows:

(1)  sum(Nil) === 0
(2)  sum(x :: xs) === x + sum(xs)

We can implement sum using foldLeft:

def betterSum(list: List[Int]): Int =
  list.foldLeft(0)(add)

def add(a: Int, b: Int): Int = a + b

However, that implementation is not obviously correct. We would like to prove that it is correct for all lists of integers. In other words, we want to prove that

list.foldLeft(0)(add) === sum(list)

for all lists of integers.

In addition to the specification of sum (axioms 1-2), you may use the following axioms:

(3)  Nil.foldLeft(z)(f) === z
(4)  (x :: xs).foldLeft(z)(f) === xs.foldLeft(f(z, x))(f)
(5)  add(a, b) === a + b
(6)  a + b === b + a
(7)  (a + b) + c === a + (b + c)
(8)  a + 0 === a

Axioms 3-5 follow from the implementations of foldLeft and add. Axioms 6-8 encode well-known properties of Int.+: commutativity, associativity, and neutral element.

Your task: Prove the following lemma by structural induction:

∀ (l: List[Int]) (z: Int), l.foldLeft(z)(add) === z + sum(l)

From that lemma, we can (with the help of axioms 6 and 8) derive that the implementation of betterSum is correct by substituting 0 for z in the lemma. You are not asked to do that last bit.

A hard proof on foldLeft and foldRight 🔥

We have now seen two list-traversal functions. One, from left to right, called foldLeft; and another, from right-to-left, called foldRight. In this exercise, we’ll see how to relate them to each other.

Let’s look back at the definitions of foldLeft and foldRight:

def foldLeft[A, B](base: B, f: (B, A) => B)(l: List[A]): B = l match
  case Nil         => base
  case Cons(x, xs) => foldLeft(f(base, x), f)(xs)

def foldRight[A, B](f: (A, B) => B, base: B)(l: List[A]): B = l match
  case Nil         => base
  case Cons(x, xs) => f(x, foldRight(f, base)(xs))

Let’s see what they have in common on a concrete example:

• Using the substitution method, reduce the expression foldLeft(base, f)(a :: b :: c :: d :: Nil) for an arbitrary function f and arbitrary values a, b, c, d. Similarly, reduce the expression foldRight(g, base)(a :: b :: c :: d :: Nil) for an arbitrary function g and arbitrary values a, b, c, d.

  Solution

    foldLeft(base, f)(a :: b :: c :: d :: Nil)
  = foldLeft(f(base, a), f)(b :: c :: d :: Nil)
  = foldLeft(f(f(base, a), b), f)(c :: d :: Nil)
  = foldLeft(f(f(f(base, a), b), c), f)(d :: Nil)
  = foldLeft(f(f(f(f(base, a), b), c), d), f)(Nil)
  = f(f(f(f(base, a), b), c), d)
  

    foldRight(g, base)(a :: b :: c :: d :: Nil)
  = g(a, foldRight(g, base)(b :: c :: d :: Nil))
  = g(a, g(b, foldRight(g, base)(c :: d :: Nil)))
  = g(a, g(b, g(c, foldRight(g, base)(d :: Nil))))
  = g(a, g(b, g(c, g(d, foldRight(g, base)(Nil)))))
  = g(a, g(b, g(c, g(d, base))))
  

• Based on the example above, conjecture a relation between foldLeft and foldRight.

  Solution

  Given type A and B, for any list l: List[A], base value base: B and function f: (A, B) => B, the result of foldRight(f, base)(l) is the same as foldLeft(base, (x, y) => f(y, x))(reverse(l)).

Now, let’s prove this property!

Similar to the above exercises, we can specify foldLeft, foldRight and reverse as follows:

(1) Nil.foldLeft(z)(g) === z
(2) (x :: xs).foldLeft(z)(g) === xs.foldLeft(g(z, x))(g)
(3) Nil.foldRight(f)(z) === z
(4) (x :: xs).foldRight(f)(z) === f(x, xs.foldRight(f)(z))
(5) Nil.reverse === Nil
(6) (x :: xs).reverse === xs.reverse ++ (x :: Nil)
(7) Nil ++ l === l
(8) (x :: xs) ++ l === x :: (xs ++ l)

Your task: Prove the following lemma (called fold_left_rev_right) by structural induction:

fold_left_rev_right: ∀ [A, B] (l: List[A]) (f: (A, B) => B) (z: B),
  l.reverse.foldRight(f)(z) === l.foldLeft(z)((b: B, a: A) => f(a, b))

Simple Stack Machine Interpreter 🔥

A stack machine uses a last-in, first-out (LIFO) stack to hold short-lived temporary values. Assume the values are integers. Then, a stack can be viewed as a list of integers:

type Stack = List[Int]

Most of a stack machine’s instructions assume that operands will be from the stack, and results placed in the stack. We consider a simple stack machine that only supports the following instructions:

• Push(v): Push an integer v into the top of the stack;
• Pop: Pop out the top of the stack;
• Add, Minus, Mul, Div: Pop out the top two elements of the stack, use them as operands of the operation, then push the result back to the stack.

Exceptions:

• For Div, a DividedByZeroException exception should be thrown when the divisor is zero.
• A NotEnoughOperandsInStackException exception should be thrown when the stack doesn’t have enough values for any instruction.

A program is a list of instructions:

type Program = List[Instruction]

For example, consider the expression A * (B - C) + (D + E), written in reverse Polish notation as A B C - * D E + +. Compiling and running this on a simple stack machine would take the form:

 Program         # stack contents (leftmost = top = most recent):
 Push(A)         #           A
 Push(B)         #     B     A
 Push(C)         # C   B     A
 Minus           #     B-C   A
 Mul             #           A*(B-C)
 Push(D)         #     D     A*(B-C)
 Push(E)         # E   D     A*(B-C)
 Add             #     D+E   A*(B-C)
 Add             #           A*(B-C)+(D+E)

(The example is taken from Wikipedia.)

In this section, your task is to implement a simple stack machine interpreter. That is, implement a method interpProg which takes an initial stack and a program, then returns the stack after execution of the program. Assume you have access to a function interpInst function, which computes the new state of a stack given the old state and a single instruction. You must use foldLeft to implement it.

def interpProg(stack: Stack, program: Program): Stack =
  ???

Now, you need to implement the interpInst function:

  def interpInst(stack: Stack, inst: Instruction): Stack =
    ???

Proofs on trees

In this part, we’ll focus on structural induction on trees. We’ll also see how to write proofs about arbitrary structurally recursive functions, not just map, fold, and other functions for which axioms were given by the problem statement.

We’ll use a Expr type similar to the one from the calculator lab as our motivating example. For simplicity, we remove the Div and Neg case and use BigInt for the numbers. Here is the definition of Expr:

enum Expr:
  case Number(value: BigInt)
  case Var(name: String)
  case Add(e1: Expr, e2: Expr)
  case Minus(e1: Expr, e2: Expr)
  case Mul(e1: Expr, e2: Expr)

… and of evaluate, written here with a function context. Notice that we return a BigInt (not an Option[BigInt]) for simplicity, which means that undefined variables have a default value (and that there are no overflows, since we’re using BigInt):

def evaluate(ctx: String => BigInt, e: Expr): BigInt = e match
  case Number(value) => value
  case Var(name)     => ctx(name)
  case Add(e1, e2)   => evaluate(ctx, e1) + evaluate(ctx, e2)
  case Minus(e1, e2) => evaluate(ctx, e1) - evaluate(ctx, e2)
  case Mul(e1, e2)   => evaluate(ctx, e1) * evaluate(ctx, e2)

To reason about arithmetic in the rest of this exercise, use the following axioms:

• ZeroPlusZero
0 + 0 === 0
• CommuPlus
a + b === b + a
• CommuMul
a * b === b * a
• BoolEq
(a == b) === true ⇔ a === b
• TrueAnd
a && b === true ⇔ ((a === true) and (b === true))

Warm up: mirror

Let’s warm up with a simple operation, mirror:

def mirror(e: Expr): Expr = e match
  case Number(value) => Number(value)
  case Var(name)     => Var(name)
  case Add(e1, e2)   => Add(mirror(e2), mirror(e1))
  case Minus(e1, e2) => Minus(mirror(e2), mirror(e1))
  case Mul(e1, e2)   => Mul(mirror(e2), mirror(e1))

mirror mirrors the left and right children of an expression tree. For example, mirror(Add(Number(1), Number(2))) is Add(Number(2), Number(1)).

Writing axioms from definitions

We have seen three ways to reason about the execution of code until now:

1. The substitution method with concrete variables, to understand how code works on a specific input;
2. Applying rewrite rules (such as MapCons or IH), to prove properties valid for all inputs;
3. The substitution method with variables, to reason about strongest postconditions.

In formal proofs we applied only (2), rewrite rules, but these techniques are related: uses of the substitution method can be converted into applications of rewrite rules. For example, for evaluate, applying the substitution method gives us the following axioms for all value, name, e1, and e2:and are given:

• EvalNumber:
  evaluate(ctx, Number(value)) === value
• EvalVar:
  evaluate(ctx, Var(name)) === ctx(name)
• EvalAdd:
  evaluate(ctx, Add(e1, e2)) === evaluate(ctx, e1) + evaluate(ctx, e2)
• EvalMinus:
  evaluate(ctx, Minus(e1, e2)) === evaluate(ctx, e1) - evaluate(ctx, e2)
• EvalMul:
  evaluate(ctx, Mul(e1, e2)) === evaluate(ctx, e1) * evaluate(ctx, e2)

Write similar axioms for the function mirror above.

Proving properties of mirror ⭐️

Does mirror preserve the value of its input expression? That is, can we prove eval(ctx, mirror(e)) == eval(ctx, e)?

If yes, write a proof of this fact using structural induction on e. If not, give a counterexample (a value for e and ctx such that the theorem does not hold, then conjecture a theorem that does hold and prove it).

Verification of static analyzers ⭐️

Let’s continue our program proofs journey by looking at a static analyzer. A static analyzer is a program that checks a property of another program.

For example, the following static analyzer checks whether the input expression e always evaluate to 0:

def zeroExpr(e: Expr): Boolean = e match
  case Number(value) => value == 0
  case Var(_)        => false
  case Add(e1, e2)   => zeroExpr(e1) && zeroExpr(e2)
  case Minus(e1, e2) => zeroExpr(e1) && zeroExpr(e2)
  case Mul(e1, e2)   => zeroExpr(e1) && zeroExpr(e2)

It correctly identifies that Add(Number(0), Mul(Number(0), Number(0))) is always zero by returning true, and it returns false for Add(Number(0), Mul(Number(1), Number(0))).

We can write this property formally as P(e) === ∀ ctx. evaluate(ctx, e) == 0.

A static analyzer is sound if all programs for which it returns true have the property (in other words, it has no false positives):

• Soundness: ∀ e. zeroExpr(e) == true ⇒ P(e).
  Or equivalently: ∀ e. ¬P(e) ⇒ zeroExpr(e) == false

It is complete if it identifies all programs that have the property (in other words, there are no false negatives: all programs for which it returns false do not have the property).

• Completeness: ∀ e. P(e) ⇒ zeroExpr(e) == true.
  Or equivalently: ∀ e. zeroExpr(e) == false ⇒ ¬P(e).

1. Write rewriting rules for zeroExpr.

2. Is zeroExpr complete? Is it sound? For each of these properties, provide either a counterexample if the property is wrong, or a proof if it’s correct.

Computer-checked proofs

In previous exercises, you were asked to write proofs about functional code. These proofs allow you to mathematically express and verify your beliefs about programs. However, who checks your proofs?

You and your peers may indeed have faced issues where the proof was incorrectly checked or completely invalidated due to a small mistake. Writing proofs can be tedious and error-prone, and correctly grading them even more so!

Further, while writing the proofs, you’re never sure if you’re correct. If only the computer could check the proof for you and provide feedback. This is indeed possible! In this exercise, we’ll see such an interface and attempt to check some proofs we’ve already seen.

The proof syntax is intended to be close to what you would write on paper, but with your IDE providing hints along the way. While you’re writing your proof, you can instead now have it checked by the computer and get some live feedback!

For example, let’s try to prove (Nil ++ Nil).map(single) === Nil using the following axioms:

(1) Nil.map(f) === Nil
(2) (x :: xs).map(f) === f(x) ::: xs.map(f)
(3) Nil.flatten === Nil
(4) (xs :: xss).flatten === xs ++ xss.flatten
(5) Nil ++ ys === ys
(6) (x :: xs) ++ ys === x :: (xs ++ ys)
(7) single(x) === x :: Nil

The axioms provided are true for all values of the variables, they are implicitly universally quantified as before. Let’s say in the paper proof, we write each step in the form x === y by Rule:

    (Nil ++ Nil).map(single)
=== Nil.map(single) by 5
=== Nil by 1

Now it’s time to use the computer to check this proof!

At the top of the file MapSingleFlatten.scala, you can find:

• declarations of available variables:

  val f: T => List[T] = ListFunctionVariable("f")
  val x: T = Variable("x")
  val xs: List[T] = ListVariable("xs")
  val ys: List[T] = ListVariable("ys")
  val xss: List[List[T]] = ListVariable("xss")
  

  equational-reasoning/src/main/scala/itp/MapSingleFlatten.scala

• predefined axioms:

  object Axioms:
    object Map:
      val NilCase = Axiom(Nil.map(f) === Nil)
      val ConsCase = Axiom((x :: xs).map(f) === f(x) :: xs.map(f))
  
    object Flatten:
      val NilCase = Axiom(Nil.flatten === Nil)
      val ConsCase = Axiom((xs :: xss).flatten === xs ++ xss.flatten)
  
    object Append:
      val NilCase = Axiom(Nil ++ ys === ys)
      val ConsCase = Axiom((x :: xs) ++ ys === x :: (xs ++ ys))
  
    object Single:
      val NilCase = Axiom(single(x) === x :: Nil)
  end Axioms
  

  equational-reasoning/src/main/scala/itp/MapSingleFlatten.scala

These can be accessed like any other Scala object. A proof looks like:

// example of a theorem applying a single rule
val exampleRuleApplication = Theorem(Nil.map(f) === Nil):
  Nil.map(f)
    === Nil ==< Map.NilCase

Noted that in each step x === y by Rule, by has been replaced by the smooth ==< operator. If you have ligatures enabled in your IDE, the theorem should look like this:

You can optionally see instructions on enabling ligatures in VSCode here.

Our previous paper proof on (Nil ++ Nil).map(single) === Nil can be translated to Scala as follows:

// example of a theorem applying two rules successively
val multipleRuleApplication = Theorem((Nil ++ Nil).map(single) === Nil):
  (Nil ++ Nil).map(single)
    === Nil.map(single)  ==< Append.NilCase
    === Nil              ==< Map.NilCase

You can run the examples with sbt runMain itp.examples, or just sbt run and then selecting itp.examples at the prompt. Running the file should print:

[info] running (fork) itp.examples
[info] Proved Theorem exampleRuleApplication: (Nil.map(f) === Nil)
...
[info] Proved Theorem multipleRuleApplication: ((Nil ++ Nil).map(single) === Nil)
...

Woohoo 🥳! Your proof now comes with a computer-checked certificate of correctness. If you alter the proof step a bit to be incorrect, attempting Nil.map(single) === xss ==< Map.NilCase:

[info] running (fork) itp.examples
...
[info] java.lang.IllegalArgumentException: requirement failed:
[info] MapSingleFlatten.scala:53 : proof step failed:
[info] 	LHS: Nil.map(single)
[info] 	RHS: xss
[info] Cannot be justified with the statement: (Nil.map(single) === Nil)
...

pointing out the equality you were attempting to prove, the rule applied, and the file and line of the failed proof.

While changing the proof, you can use ~runMain itp.examples in sbt to re-run automatically whenever you change the proof.

Starting with Proofs ⭐️

You can run the warm-up exercises as ~runMain itp.startingWithProofs in sbt.

Proofs with Axioms

Based on the provided axioms, complete the proof nilAppend:

val nilAppend = Theorem((x :: Nil) ++ Nil === (x :: Nil)):
  (x :: Nil) ++ Nil
  ???

You can look at the examples multipleRuleExample and usingAssumption for more syntax.

Proofs with Assumptions

Based on the provided axioms and assumptions, complete the proof concatNilFlatten:

val assumption = xs ++ Nil === Nil ++ xs

val concatNilFlatten = Theorem(
  assumption ==> ((xs ++ Nil.flatten) === xs)
):
  ???

What happens if you alter the assumption statement? What if you do not put the assumption in the theorem statement?

Restating and readability

Writing a list like x :: y :: Nil can certainly be annoying, but since we are just using Scala, we can define a familiar alias:

// convenient syntax for lists
// eg: List(x, y)
def List[A](xs: A*): List[A] =
  if xs.isEmpty then Nil
  else xs.head :: List(xs.tail*)

To the proof, List(x, y) and x :: y :: Nil are exactly the same thing, and so this does not affect how the proof checker sees our terms at all.

As neat as aliases and notations are most of the time, when mixed in with other terms, they can sometimes become hard to read. For example,

List(x) ++ Nil
  === x :: (Nil ++ Nil) ==< Axiom((x :: xs) ++ ys === x :: (xs ++ ys))

is not immediately obvious to understand, as the axiom uses x :: xs, while our statement has List(x). So, for both readability and to display the author’s intention, it is often worthwhile to perform “restate” steps in a proof, writing the same statement, but in a more understandable form:

List(x) ++ Nil
  === (x :: Nil) ++ Nil ==< ???
  === x :: (Nil ++ Nil) ==< Axiom((x :: xs) ++ ys === x :: (xs ++ ys))

The “restate” step, while not necessary, expands the definition of List(_) to allow for better readability for humans. In the end, the goal of a proof is to ascertain yourself about mathematical statements, and to share those results with other humans, who may use the proof to then convince themselves. It is worthwhile to adapt your proof to display your train of thought.

Given that, how do we justify our “restate” step, what goes in the place of ???. In fact, since we are just writing x === x ==< Rule, this statement is true regardless of the rule we provide. To be clear about our intentions, we say that this statement follows from reflexivity, and define this as Restate.

// if we are simply rewriting a step, we can say it follows from reflexivity
// note that adding x === x as an axiom does not change anything
// as it is already true
val Restate = Axiom(xs === xs)

For example:

// example of how to use Restate (which is just True)
// effectively, x === x always holds! 
// we write it as Restate to emphasize our intention
val rewritingTerms = Theorem(xs === xs):
  xs
    === xs ==< Restate

And we can adapt this into a larger example:

// an example to how we can unfold visual definitions 
// to emphasize terms in a proof
val unfoldingDefs = Theorem(List(x) ++ Nil === List(x)):
  List(x) ++ Nil
    // we are simply rewriting the Scala definition of List(_)
    // the proof would work just fine without it, 
    // but proofs aren't written just for computers, 
    // there's human readability and convenience to consider!
    === (x :: Nil) ++ Nil ==< Restate
    === x :: (Nil ++ Nil) ==< Append.ConsCase
    === x :: Nil          ==< Append.NilCase
    === List(x)           ==< Restate

Proof of MapSingleFlatten ⭐️

Based on the provided axioms, prove the statement:

xs.map(single).flatten === xs

for all lists xs. The proof is done in two parts, by induction, same as on paper.

As before, the proofs can be run and checked with ~runMain itp.theorems in sbt.

Base Case

First, complete the base case without assumptions:

// Base Case
val singleNil = Theorem(Nil.map(single).flatten === Nil):
  Nil.map(single).flatten
  ???

Inductive Case

Finally, complete the inductive case with the provided induction hypothesis:

// Induction Hypothesis
val IH = xs.map(single).flatten === xs

// Inductive Case
val singleInduct = Theorem(
  IH ==> ((x :: xs).map(single).flatten === (x :: xs))
):
  (x :: xs).map(single).flatten
  ???

Background: proof checking

Proof checking is often a surprisingly complicated task. Many tools have been developed to help with this, called proof assistants. As the name suggests, these often provide more information than just checking your proofs, nudging you along the way. Some popular proof assistants are Rocq, Lean, and Isabelle. A list of related tools can be found at EuroProofNet/Tools.

Our little proof checking interface is based on an in-house proof assistant written in Scala, called Lisa. Lisa is provided with the exercises as a JAR file in lib/. The syntax provided is a small subset of Lisa’s proof capabilities, i.e. restricted to equality proofs on lists. Lisa uses Set Theory as its mathematical foundations, and so does not have an inherent notion of types at all! The types available to you here are an imitation of Scala lists that generate expression trees, which are internally converted to Lisa expressions after erasing some of the type information.

There are many tactics and algorithms involved in expanding the equality proof from a single equality step you may write. Finally, these are reduced to some simple steps understood by Lisa’s core, the kernel. These are the rules of first-order logic as a sequent calculus. Limiting the core of the system to simple rules and building everything else on top of these allows you to be certain that your proofs are checked with confidence at the end!

In the rest of this exercise set, we practice some more proofs in this style.

Associativity of List Concatenation

The following are axioms that follow from the definition of ++:

val NilCase   = Axiom((Nil ++ xs) === xs)
val ConsCase  = Axiom(((x :: xs) ++ ys) === (x :: (xs ++ ys)))

Using these axioms, use induction to prove the associativity law.

Base Case

val baseCase = Theorem(
  (Nil ++ ys) ++ zs === Nil ++ (ys ++ zs)
):
  ???

Inductive Case

val IH = (xs ++ ys) ++ zs === xs ++ (ys ++ zs)

val inductiveCase = Theorem(
  IH ==>
    ((x :: xs) ++ (ys ++ zs) === ((x :: xs) ++ ys) ++ zs)
):
  ???

Factoring out formulas

Proofs are chains of formulas and the justification of their equivalence. We can, in principle, define our own functions that manipulate formulas. In particular, our associativity condition can be parameterized by the expression that stands for the first list using the following function on expression trees representing formulas.

def assocFor(v: List[T]): PredicateFormula[List[T]] =
  (v ++ ys) ++ zs === v ++ (ys ++ zs)

// Theorems for base case and inductive case using assocFor shorthand
???

Use this abbreviation, rewrite the statements of the base case and inductive case to make them shorter.

Reversing Concatenation

Use the axioms that define reverse, as well as the previously proven associativity law as an axiom

object Append:
  val NilCase   = Axiom((Nil ++ xs) === xs)
  val ConsCase  = Axiom(((x :: xs) ++ ys) === (x :: (xs ++ ys)))
  val Assoc     = Axiom((xs ++ ys) ++ zs === xs ++ (ys ++ zs))
  val NilEnd    = Axiom((xs ++ Nil) === xs)

object Reverse:
  val NilCase   = Axiom(Nil.reverse === Nil)
  val ConsCase  = Axiom((x :: xs).reverse === xs.reverse ++ List(x))

to show

(xs ++ ys).reverse === (ys.reverse ++ xs.reverse)

We have defined abbreviation List(x) to stand for x :: Nil.

Base Case

val baseCase = Theorem(
  (Nil ++ ys).reverse === (ys.reverse ++ Nil.reverse)
):
  ???

Inductive Case

val IH = 
  ???

val inductiveCase = Theorem(
  IH ==>
    (((x :: xs) ++ ys).reverse
      === ys.reverse ++ (x :: xs).reverse)
):
  ???

Reversing Reversal

We will next use several previously proven theorems as axioms:

object Append:
  val NilCase = Axiom((Nil ++ xs) === xs)
  val ConsCase = Axiom(((x :: xs) ++ ys) === (x :: (xs ++ ys)))
  val Assoc = Axiom((xs ++ ys) ++ zs === xs ++ (ys ++ zs))
  val NilEnd = Axiom((xs ++ Nil) === xs)

object Reverse:
  val NilCase = Axiom(Nil.reverse === Nil)
  val ConsCase = Axiom((x :: xs).reverse === xs.reverse ++ List(x))
  val AppendCase = Axiom((xs ++ ys).reverse === (ys.reverse ++ xs.reverse))

// if we are simply rewriting a step, we can say it follows from reflexivity
// note that adding x === x as an axiom does not change anything
// as it is already true
val Restate = Axiom(xs === xs)

to show that reversing the list twice gives us back the original list:

xs.reverse.reverse === xs

Base Case

val baseCase = Theorem(
  Nil.reverse.reverse === Nil
):
  ???

Inductive Case

val IH = (xs.reverse.reverse === xs)
  ???

val inductiveCase = Theorem(
  IH ==>
    ((x :: xs).reverse.reverse === (x :: xs))
):
  ???

Trees with inOrder Traversal ⭐️

Trees are also amenable to equational proofs. We can do proofs by induction by assuming a property of two subtrees, left, right and proving that it holds for the overall tree Node(left, x, right).

In this exercise, we only show how to use equational proofs on a non-recursive function. However, the function uses list concatenation, so we will need to make use of the previously proven associativity of concatenation.

Specifically, we wish to prove that balancing a binary tree using a rotation operation preserves the order of elements. The rotation we consider is the following transformation:

          q                         p
         / \                       / \
        p   c       ====>         a   q
       / \                           / \
      a   b                         b   c

To compute the list associated with a tree we use the function inOrder that computes the list associated with the elements of the tree.

The property we wish to prove corresponds to applying inOrder to both sides of the transformation pictured above.

Node(Node(a, p, b), q, c).inOrder === Node(a, p, Node(b, q, c)).inOrder

The behavior of inOrder as well as the other relevant axioms is the following:

object InOrder:
  val EmptyCase   = Axiom(Empty.inOrder === Nil)
  val NodeCase    = Axiom(Node(left, x, right).inOrder 
                        === left.inOrder ++ (List(x) ++ right.inOrder))

object Append:
  val NilCase     = Axiom((Nil ++ xs) === xs)
  val ConsCase    = Axiom(((x :: xs) ++ ys) === (x :: (xs ++ ys)))
  val Assoc       = Axiom(((xs ++ ys) ++ zs) === (xs ++ (ys ++ zs)))

Direct Proof

Try to prove the theorem in a single proof from left to right. Our solution has 7 steps.

val rotationInvariance = Theorem(
  Node(Node(a, p, b), q, c).inOrder === Node(a, p, Node(b, q, c)).inOrder
):
  ???

Proof Using Lemmas

Sometimes it can be difficult to see how to construct a left to right proof directly. Of course, we can write the lines of the proof in any order; once we are done, we can ask the system to check the resulting proof. But we can do even more. We can prove individual equations for parts of the transformation, then combine them into a larger one. Such proof may not be as pretty or even as short, but it may better reflect your problem-solving strategy.

In our example, it makes sense to try to expand, on both sides, the application of inOrder as much as the input tree reveals. Try to compose your proof using several lemmas, including the following ones. You may need to define some lemmas on your own as well.

val lemma1 = Theorem(
  Node(Node(a, p, b), q, c).inOrder
    === (a.inOrder ++ (List(p) ++ b.inOrder)) ++ (List(q) ++ c.inOrder)
):
  ???

val lemma2 = Theorem(
  Node(a, p, Node(b, q, c)).inOrder
    === (a.inOrder ++ (List(p) ++ (b.inOrder ++ (List(q) ++ c.inOrder))))
):
  ???

  ???

val rotationInvarianceFromLemmas = Theorem(
  Node(Node(a, p, b), q, c).inOrder === Node(a, p, Node(b, q, c)).inOrder
):
  ???

Tests

Tests are a key part of robust software development, and the best way to get proficient at testing is to write tests for your own code. For more focused training, however, we provide a few exercises below. Happy hacking!

Understanding different kinds of tests

1. Think of an event in your life that you had to rehearse or train for:

   • Which components of your preparation were most like unit tests (focusing on a single, minimal aspect)?
   • Which components were more similar to integration tests (focusing on a subsystem and exercising it from end to end)?
   • Which were more like system tests (exercising the whole system in conditions as close as possible to the real event)?
   • Was there any monitoring (detecting issues as they happen)?

2. Classify the following tests into monitoring, unit tests, integration tests, system tests, and acceptance tests.

   1. Your dishwasher reports that it is low on salt.
   2. Your induction stove turns off due to a spill.
   3. A phone repair tech checks that all pixels on your phone screen are working by displaying a uniform-white picture.
   4. You make sure that your baking powder still works by pouring a bit of vinegar or a bit of hot water on it.
   5. While developing a robot, you make sure that your path-planning software works by running it in a simulator.
   6. Your phone indicates that you are low on space.
   7. You practice for a test by attempting to complete a mock exam within the allocated time.
   8. You demo your newly built robot to investors at a tech fair.

Debugging, testing, and refactoring all in one 🔥

In an attempt at making a boids callback better, we have implemented a quadtree data structure to hold boid collections. Quadtrees are a two-dimensional analogue of binary search trees: they are used to organize point clouds in a way that supports quick filtering and lookups (in boids, this would allow us to quickly determine which boids are close to each other, in much less time than a linear filter of all boids). You can see the complete implementation in src/main/scala/tests/QuadTree.scala.

Unfortunately, the lab release date is fast approaching (edit: passed), and we still haven’t written unit tests nor integration tests, let alone documentation. There’s even a missing function, contains!

Worse: one of our SAs reports that our implementation sometimes loses boids, and sometimes gets into an infinite loop. Oh, and there also seem to be performance problems.

Your task: help us fix it! We need to do the following:

1. implement the missing function;
2. add a documentation string to each function;
3. add pre- and postconditions (require and ensuring) where relevant;
4. write unit tests (testing a single function) and integration tests (testing collection of functions) to ensure that the quadtree works correctly;
5. fix any bugs and performance issues that may pop up.

Oh, and when you’re done: patch boids to use the tree!

You will most likely find it useful to work with others. Don’t hesitate to create a thread on Ed to share documentation, tests, bugs, or ideas.

Good luck! Some tips:

• Unit tests, for a structure like this one, would be tests that call a single function on a quadtree and check that it has changed exactly as expected.
• Integration tests, on the other hand, would combine multiple operations on the tree, such as an insertion followed by a contains check.

Writing Good Tests ⭐

Your company just completed the implementation of its most advanced app ever: printList 2025 Pro printer, and the first release just shipped to clients who had pre-ordered it. printList was sold as structured and indexed formatter for printing lists.

The function prints a header (<start>), the first three elements of the list with specific labels (“1st”, “2nd”, “3rd”), followed by all remaining elements prefixed with their corresponding label and a suffix th. In the first release, numbers past 5 all get a th suffix, even 21, 22, 23, etc. A closing line (<end>) is printed at the end.

If the list is empty, it prints <empty> instead.

Unfortunately, it does not seem to be working as expected. An angry customer wrote:

I cannot believe this passed QA. When I feed it a list like ['apple', 'banana', 'cherry', 'date', 'elderberry'], it just goes completely off the rails. It prints, but not the way your documentation promised. The program even crashes on some inputs. I spent 45 minutes trying to make sense of the output and ended up rewriting half of it myself. Is this what I paid for?

You have been tasked with fixing the bug(s?) ASAP.

1. Convert the description of the user-submitted bug into a failing test and confirm that it fails by running sbt test.

2. Apply the debugging method step by step to find the bug(s). For each bug:

   1. Write one or more regression unit tests that fail because of the bug.
   2. Fix the code.
   3. Confirm your fix by checking that all your regression tests (including the ones you wrote for the previous issues if any) pass.
   Hint

   Play with manual inputs in the worksheet, find failing inputs and then debug one by simplifying the source to pinpoint the problem. In other words: follow the debugging guide!

   def printList[T](list: List[T]): Unit =
     if list.isEmpty then
       println("<empty>")
     println("<start>")
     println("1st element: " + list(0))
     println("2nd element: " + list(1))
     println("3rd element: " + list(2))
     for (item, i) <- list.zipWithIndex.drop(3) do
       println(f"${i}th element: $item")
     println("<end>")
   

   tests/src/main/scala/debugging/PrintList.scala

3. How many distinct issues were there?

© 2023–2025 EPFL. All rights reserved.