Last updated on Sunday, November 09, 2025

Week 10: Contextual Abstraction and Mutation Reasoning

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

This exercise set is intended to help you explore mutation, reasoning about programs correctness, and work with contextual abstraction.

As usual, ⭐️ indicates the most important exercises and questions and 🔥 indicates the most challenging ones. 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.

Contextual Abstraction

Implicit Context ⭐️

You have seen in previous lab and exercises an enum for arithmetic expressions. Let’s augment it with a Let form:

enum Expr:
  case Num(value: Int)
  case Var(name: String)
  case Let(name: String, value: Expr, body: Expr)
  case Add(e1: Expr, e2: Expr)
  case Sub(e1: Expr, e2: Expr)
  case Mul(e1: Expr, e2: Expr)

Write an eval function for expressions of this type. You should not use any mutable or global variables or mutable collections.

def evaluate(e: Expr): Int =
  def recur(e: Expr)(using ctx: Map[String, Int]): Int = e match
    case _ => ???

  recur(e)(using Map.empty)

Let(”x”, e1, e2) should be evaluated like {val x = e1; e2}. You can assume that every Var(x) occurs in the body b of an enclosing Let(x, e, b).

For example, the following expression should evaluate to 4:

val e3 = Let("x", Let("y", Num(1), Add(Var("y"), Var("y"))), Mul(Var("x"), Var("x")))
evaluate(e3)

Serialization with implicits 🧪

In the webapp lab, we are using type class WireFormat[T] to represent encoding and decoding between JSON and a data type T.

In the original implementation, the type classes for different data types are defined as regular classes, which means, to use the instance of a type, we have to construct its format manually at every place.

In this exercise, your task is to use contextual abstractions to define instances of the type class WireFormat. They are defined in webapp/lib/shared/shared/src/main/scala/wires/Wires.scala.

First, you need to define the general encode and decode functions for wires at the top of the file:

def encodeWire[T](t: T)(using wt: WireFormat[T]): ujson.Value =
  ???

def decodeWire[T](js: ujson.Value)(using wt: WireFormat[T]): Try[T] =
  ???

With these two functions, you can call encode and decode functions without naming the using parameters.

Then, you need to modify the different instances of WireFormat. For example, the WireFormat[Boolean] was defined as:

object OldBooleanWire extends WireFormat[Boolean]:
  def encode(t: Boolean): Value = Bool(t)
  def decode(js: Value): Try[Boolean] = Try(js.bool)

It can be transformed to:

given WireFormat[Boolean] with
  def encode(t: Boolean): Value = Bool(t)
  def decode(js: Value): Try[Boolean] = Try(js.bool)

If you encounter any ambiguity error (this may happen when using decodeWire in a complex expression), you can specify the type argument explicitly. Try not to use summon to get the instance of a type class explicitly.

See Importing Givens for details about how to import given instances.

Mutation

Proofs of imperative algorithms (Hoare logic)

In this section, we will take a look at how we can make sure that imperative programs are actually correct.

This is related to what you did in the Specifications exercises, when you translated properties into code. Here you will perform a similar task, but you will also write invariants, which are properties that stay true throughout the execution of a program and help to prove that some properties hold.

Absolute value ⭐️

We will start with the absolute value function on Int with the following definition:

def abs(x: Int): Int = {
  if x < 0 then -x else x
} ensuring (res =>
  ???
)

What does this function guarantee? What is the condition that the result of the absolute value function must satisfy mathematically? Complete the ensuring above.

The max function ⭐️

Let us start with the max function on List[Int] and Array[Int]. You can choose which version you want to implement. We require that the list or the array is not empty.

def maxLoopArray(a: Array[Int]): Int =
  require(!a.isEmpty)
  ???

def maxLoopList(l: List[Int]): Int =
  require(!l.isEmpty)
  ???

def maxLoopArray(a: Array[Int]): Int =
  require(!a.isEmpty)
  var index = 1
  var max = a(0)
  while index < a.length do
    if a(index) > max then max = a(index)
    index += 1
  max

def maxLoopList(l: List[Int]): Int =
  require(!l.isEmpty)
  var list = l.tail
  var max = l.head
  while !list.isEmpty do
    if list.head > max then
      max = list.head
    list = list.tail
  max

We now ask you to write a loop invariant for the max function. As a reminder, a loop invariant is a boolean condition that stays true throughout all executions of the loop. In particular, the invariant is true before and after the loop, and therefore helps to prove the correctness of the loop.

You can use the take and forall functions on List , knowing that:

assert(l.take(n+1) == l.take(n) ++ List(l(n)))
assert(l.take(0).isEmpty)
assert(l.forall(x => true))

These functions also exist on Array and work in a similar way.

def maxLoopListWithInvariant(l: List[Int]): Int =
  require(!l.isEmpty)
  ???

def maxLoopArrayWithInvariant(a: Array[Int]): Int =
  require(a.size > 0)
  ???

The find function

Let us know take a look at the find function on List. The find function takes a predicate and a list and returns the first element of the list that satisfies the predicate. If no element satisfies the predicate, it returns None. We will use the following implementation:

def find(l: List[Int], p: Int => Boolean): Option[Int] = {
  def loop(l: List[Int]): Option[Int] =
    var li = l
    while !li.isEmpty do
      assert(true)
      if p(li.head) then
        return Some(li.head)
      li = li.tail
      assert(true)
    None
  loop(l)
}
  .ensuring(res => ???)

We want to prove that find is correct. Can you think of the post condition? If the function returns None, what should be true about the list? And if it returns Some(x), what should be true about x and the list?

First write the post condition of the function in the ensuring.

Then, we will write an invariant for the while loop. What should be true about the list at each iteration? Do we need a condition on the part of the list that was already visited?

Add your invariant condition in the asserts in the loop.

I can’t believe it can sort 🔥

In this exercise, we will analyze a sorting algorithm puzzle from a recent short paper. Here it is, implemented in Scala:

def swap(a: Array[Int], i: Int, j: Int): Unit =
  val tmp = a(i)
  a(i) = a(j)
  a(j) = tmp

def ICantBelieveItCanSort(a: Array[Int]): Unit =
  for i <- 0 until a.length do
    for j <- 0 until a.length do
      if a(i) < a(j) then
        swap(a, i, j)

It looks suspiciously similar to other sorting algorithms; for comparison, here is an insertion sort:

def insertionSort(a: Array[Int]): Unit =
  for i <- 1 until a.length do
    for j <- i until 0 by -1 do
      if a(j) < a(j - 1) then
        swap(a, j, j - 1)

… yet it’s not the same. In fact, this ICantBelieveItCanSort routine is not a good sorting algorithm — don’t use it! But it’s a good reasoning puzzle… why does it work? The authors write:

There is nothing good about this algorithm. It is slow – the algorithm obviously runs in $\Theta(n^2)$ time, whether worst-case, average-case or best-case. It unnecessarily compares all pairs of positions, twice. There seems to be no intuition behind it, and its correctness is not entirely obvious. You certainly do not want to use it as a first example to introduce students to sorting algorithms. It is not stable, does not work well for external sorting, cannot sort inputs arriving online, and does not benefit from partially sorted inputs.

You task is to understand why this algorithm correctly sorts its input array, and then write a proof of correctness for it. Coming up with the complete proof is hard; simply transcribing the proof provided by the authors would already be an excellent exercise.

def highlight(a: Array[Int], is: Int*) =
  a.toList.zipWithIndex.map((x, k) => if is.contains(k) then f"[$x]" else f" $x ").mkString(", ")

def ICantBelieveItCanSort_traced(a: Array[Int]): Unit =
  for i <- 0 until a.length do
    println(f">> i=$i")
    for j <- 0 until a.length do
      if a(i) < a(j) then
        println(f">  j=$j ${highlight(a, i, j)}")
        swap(a, i, j)
        println(f">  j=$j ${highlight(a, i, j)}")

Strongest postconditions

In this section, we will take a look at the concept of strongest postconditions to reason about programs behaviour, and ultimately correctness.

The strongest postcondition is the most restrictive condition on the output of a program, given that the input satisfies a given condition. Let us say we are analyzing the following function f:

def f(x: BigInt): BigInt = {
  require(x > 0)
  x + 1
} ensuring (res => ???)

Note that we are using BigInt, which represents natural numbers, so we don’t have to worry about overflows.

We are looking for a condition sp such that f returns a value that satisfies sp if the input x satisfies the precondition x > 0. Moreover, we want sp to be the most restrictive (“strongest”) possible.

So:

def f(x: BigInt): BigInt = {
  require(x > 0)
  x + 1
} ensuring (res => res > 1)

In this example, the strongest postcondition is x => x > 1. Indeed, for all x > 0, f returns a value that is greater than 1. Moreover, we cannot find a more restrictive condition.

We can also think of the strongest postcondition in terms of set of values for the input and output. Let us call the set of values that satisfy the precondition P and a set of values that satisfy the postcondition Q. Then, the strongest postcondition is the smallest set of values Q such that for all x in P, f(x) is in Q. In our example, P = {x | x > 0} and Q = {x | x > 1}.

Strongest postcondition calculations are useful to check specifications: if we have a precondition (require) and a postcondition (ensuring) for a given program, then we can check that the postcondition follows from the precondition by checking that the strongest postcondition implies the stated postcondition. Formally, it is:

assert(if sp(x) then ensuring(x) else false)

or

$$ \forall x: x \in Q \implies x \in S $$

where $S$ is the set of all outputs permitted by the user-supplied ensuring clause.

Strongest postcondition for pure functions

Now that we know what a strongest postcondition is, let us find one for the following functions:

def f1(x: BigInt): BigInt = {
  require(x > 0)
  2 * x
} ensuring (y => ???)

def f2(x: BigInt): BigInt = {
  require(x > 2 && x <= 10)
  if x < 5 then BigInt(0) else x
} ensuring (res => ???)

def f3(x: BigInt): BigInt = {
  require((x > 0 && x < 9) || (x >= 20 && x < 26))
  if x < 6 then x + 1
  else if x < 23 then 3 * x
  else -2 * x
} ensuring (y => ???)

Try to think of arguments as symbolic values rather than concrete. This means that you should think of x as a variable containing a natural number constrained by the precondition. Then you go through the code and for each new condition, you create a new condition to a mental set. When you encounter a modification or return statement, you also add a condition to the one of the branch you are in, connected with a conjunction. At then end, you can take a disjunction of the conditions you created for each branch.

This technique can be implemented mechanically, and this is called Symbolic Execution. It can be used in practice to prove postconditions of programs.

Strongest postcondition for imperative functions

Now, let us take a look at imperative functions — try to find the strongest postconditions of these programs!

def imperativeF1(x: BigInt): BigInt = {
  require(x >= -1 && x <= 4)
  var y = x
  var z = BigInt(1)
  if y > 0 then z *= 4
  if y < 4 then z *= 2
  if y % 2 == 0 then z -= 3

  z
} ensuring (z => ???)

def imperativeF2(x: BigInt): BigInt = {
  require(x >= -5 && x <= 5)
  var y = x
  var z = BigInt(0)
  while y * y > 0 do
    z += 1
    if y > 0 then y -= 1
    else y += 1
  z
} ensuring (z => ???)

Bottom-up merge sort: saving memory with mutation ⭐️

Bottom-up merge sort is a variant of merge sort that uses a different algorithm to merge two sorted lists. In the functional programming paradigm, we have used the foldt trick. In the imperative paradigm, we will use mutation on Arrays. This variant will be in-place meaning that we will directly modify the input array instead of creating a new one.

The benefit of having an in-place algorithm is that we do not need to allocate a new array for each merge. This saves memory and is more efficient. However, it is more difficult to implement and to reason about. This algorithm will be a good exercise to practice imperative programming and to see how mutation can be used to save memory. It will allocate a new array only once, at the beginning of the algorithm.

For this exercise, we will sort Arrays of size $2^k$ for some $k \in \mathbb{N}$. This is not a limitation of the algorithm, but it will simplify the implementation.

The idea is the following, with an array a of length $n = 2^k$ for some $k \in \mathbb{N}$:

• Create an array of the same length $n$ that we will name b.
• Do successive runs of length $1$, $2$, $4$, …, $2^k$ where $2^k \leq n$. Denote width the length of such a run.
• For each run of width width:
  • We will merge the two subarrays of length width / 2 into the array b.
  • We will then copy the content of b into a.
• Once we have merged all the runs of width width, we copy the content of b into a and double the width and start again until the whole array is merged.

Here is an example of execution of this merge-sort algorithm, with the array [15, 4, 18, 11]:

• Allocating b = [0, 0, 0, 0]
• The array a contains runs of length 1: [15, 4, 18, 11]
  • Runs are [15], [4], [18], [11]
• Merging the runs of length 1 into b to produce runs of length 2: [4, 15, 11, 18]
• Writing b into a: [4, 15, 11, 18]
• The array a contains runs of length 2: [4, 15, 11, 18]
  • Runs are [4, 15], [11, 18]
• Merging the runs of length 2 into b to produce runs of length 4: [4, 11, 15, 18]

You can see that the array is sorted at the end.

The implementation will be divided into two parts:

• A function sort that will do the successive runs and merge them.
• A function merge that will merge two consecutive runs of length k from an array into a run of length 2*k, written to another array.

You can start from the following template:

def sort(original: Array[Int]): Array[Int] =
  val n = original.length

  ???

def merge(a: Array[Int], b: Array[Int], indexLeft: Int, width: Int) =
  ???

merge is a function that will take three extra arguments:

• indexLeft corresponds to the index of the first element of the left run.
• width corresponds to the width of a run.

In other words, the left run is a[indexLeft: indexLeft + width), the right run is a[indexLeft + width: indexLeft + 2 * width) and the merged run should be b[indexLeft: indexLeft + 2 * width), where [a:b) means from index a (included) to index b (excluded).

Logging

Logger

When running code, it can be useful to print what is going on for debugging. In order to do so, let us define a trait Logger:

trait Logger:
  def log(message: String, depth: Int = 0): Unit

logger.log("= Head of the tree")
logger.log("= Sub-element", 1)
logger.log("= Sub-sub-element", 2)
logger.log("= Sub-element", 1)
logger.log("= Sub-sub-element 1", 2)
logger.log("= Sub-sub-element 2", 2)

= Head of the tree
  = Sub-element
    = Sub-sub-element
  = Sub-element
    = Sub-sub-element 1
    = Sub-sub-element 2

recursion.ListOpsTests:
  + length: empty list 0.008s
  + length: list with 2 elements 0.0s
  + length: list with 4 elements 0.0s
  …
anagrams.AnagramsSuite:
  + computeOccurrenceList: abcd (3pts) 0.032s
  + computeOccurrenceList: Robert (3pts) 0.0s
  …

Let’s implement a LoggerBuffered that will accumulate messages in a private buffer mutable field as the following:

class LoggerBuffered extends Logger:
  // private var ???

  def log(message: String, depth: Int = 0): Unit =
    ???
  def getOutput: String =
    ???

Adding logs to eval

Let’s refer to a simple evaluator for the following ADT:

enum Expr:
  case Constant(a: Int)
  case Add(a: Expr, b: Expr)
  case Sub(a: Expr, b: Expr)

and implement the function that evaluates such an expression, but for every expression that is evaluated, you need to log every performed operation using the given Logger l:

def eval(e: Expr, l: Logger, depth: Int = 0): Int =
  ???

And here is an example: the following snippet

val l = new LoggerBuffered
eval(Add(Add(Constant(1), Constant(2)), Constant(3)), l)
l.getOutput

generates

Add(Constant(1),Constant(2)) + Constant(3) ->
  Constant(1) + Constant(2) ->
    Constant(1) = 1
    Constant(2) = 2
  = 3
  Constant(3) = 3
= 6

Adding logs to a stack interpreter

A practical foldLeft ⭐️

In this exercise, you will write an interpreter for a small stack language. We already saw this concept in the exercises about polymorphism in week 4. This version is a bit different though.

The language offers the following operations:

enum Operation:
  case Push(n: Int)
  case Add
  case Sub

type Program = List[Operation]

This language then offers constant integer values, as well as addition and subtraction operations.

For example, the arithmetic expression 1 + 2 - 3 + 4 would be expressed by the following Program:

val p = List(Push(1), Push(2), Add, Push(3), Sub, Push(4), Add)

We will write a stack machine based interpreter for this language.

A stack machine interpreter uses a stack and reads the tokens from a Program (i.e., a list of operations) one after the other. For each operation, it performs the following:

• if it is a Push(n) value, it pushes the value n on the stack.
• if it is an Add operation, it pops two elements of the stack, adds them and pushes the result back on the stack.
• if it is a Sub operation, it pops two elements of the stack, subtracts them and pushes the result back on the stack.

After reading the whole program, the stack should contain a single element, which is the result of the program.

Recursive

Let us start by writing a recursive version of the interpreter. To start, you will implement a function that takes a stack (in this case, it is represented by a List[Int]) and one Operation and returns a new stack. The returned stack corresponds to the state of the stack after the operation has been executed:

  def evalOp(stack: Stack, op: Operation): Stack =
    ???

No, write two copies of the recursive version of the eval function which interprets an entire program, starting with an empty stack: one using plain recursion without calling higher-order list functions, and one with foldLeft:

  def eval(p: List[Operation]): Stack =
    ???

Now imperative 🔥

Write down the operations that the recursive algorithm performs, step by step, on an example. How does the stack evolve? Can you replicate this behavior with a mutable Stack from the Scala library?

  def eval(p: List[Operation]): Stack[Int] =
    ???

Adding logs ⭐️

In this step, we will add logging to the interpreter. The goal is to log every operation that is performed on the stack. For example, the following instructions:

Push(1), Push(2), Add, Push(3), Sub, Push(4), Add

should log the following:

Push(1) →
  Stack: 1
Push(2) →
  Stack: 2 1
Add →
  Stack: 3
Push(3) →
  Stack: 3 3
Sub →
  Stack: 0
Push(4) →
  Stack: 4 0
Add →
  Stack: 4

It’s to you how to implement the logging: the only requirements is that you should log the operation that is performed and the stack at each step.

You are free to use either the recursive or the imperative version of the interpreter.

Debugging expressions with side effects

We will study stateful code in depth in week 10. Since some of you have already started using vars, however, here is an exercise on this topic.

Pure expressions can be evaluated in any order. Given def f(x: Int) = x + 1, you can substitute f(1) with 1 + 1 whenever you like and it doesn’t affect the final result.

On the other hand, the evaluation order matters for expression with side effects. Think about a function g that prints a message: in the program g("Hello "); g("world!"), it’s important that g("Hello ") be evaluated before g("world!"), otherwise "world!Hello " will printed instead of "Hello world!".

Reminder: Scala uses the call-by-value evaluation strategy by default.

upgradeUserToVip

Someone is writing a user-management program for a supermarket like Aligro. It maintains two global lists: users contains all users, vipUsers contains the VIP users. Any VIP user is in the users list as well.

var users: IntList = IntCons(101, IntCons(102, IntCons(103, IntNil())))
var vipUsers: IntList = IntCons(102, IntNil())

createNewUser takes a user ID and creates a new user using this ID. It returns true if the new user was successfully created, and false if the ID was already in use (in that case, the user database is left unmodified).

def createNewUser(id: Int): Boolean =
  if contains(users, id) then false
  else
    users = IntCons(id, users)
    true

createNewVipUser is similar to createNewUser, but it creates a new VIP user if it’s not already a VIP. Like createNewUser, it returns true if a new VIP user was successfully created.

def createNewVipUser(id: Int): Boolean =
  if contains(vipUsers, id) then false
  else
    vipUsers = IntCons(id, vipUsers)
    true

Finally, upgradeUserToVip takes a user ID, and if this ID indeed belongs to a user and this user is not a VIP yet, it upgrades the user to VIP. It returns true if the upgrade was successful.

def upgradeUserToVip(id: Int): Boolean =
  val canCreateNewVipUser = createNewVipUser(id)
  contains(users, id) && canCreateNewVipUser

1. This program contains a bug. What’s the bug?

2. Fix the bug.

© 2023–2025 EPFL. All rights reserved.