Based on the code snippets developed in class, summaries and explanations in this document were drafted with the assistance of generative AI. The author verified all facts, revised the text for coherence, and takes full responsibility for the final content.

Week 3 Overview

The week starts with lightweight program contracts through tests, then moves to expression evaluation and a small interpreter with variables and a store.

1) A First Contract Through Tests: max

We begin with a tiny function and check its behavior by assertions. The key idea is that tests document expected behavior for normal and edge inputs.

def max(x: Int, y: Int): Int =
  // x > y rewritten as x - y > 0
  if x - y > 0 then x else y
end max

assert(max(0, 10) == 10)
assert(max(10, 0) == 10)
assert(max(5, 5) == 5)
assert(max(-1, 1) == 1)
assert(max(-1, -2) == -1)
assert(max(1, -1) == 1)

These assertions act as executable examples, but miss a critical bug in the implementation. Formal verification with Scala Stainless reveals the bug and provides a counterexample that we can add to our test suite.

assert(max(1879048191, -2147483646) == 1879048191)

Once we can state behavior for a simple function, we can move to a richer data model where equality itself is part of the contract.

2) Contract for Data: Rational Equality

The next activity introduces a Rational type and asks us to define semantic equality (fractions with the same value should compare equal).

case class Rational(n: Int, d: Int):
  override def equals(other: Any): Boolean = ???
end Rational

// expected behavior:
// Rational(9, 3) == Rational(6, 2)
// Rational(1, 2) == Rational(2, 4)
// Rational(6, 2) != Rational(8, 2)

Implemented naively misses division by zero and rounding in integer division; both are discovered by formal verification.

case class Rational(n: Int, d: Int):
  override def equals(other: Any): Boolean = other match
    case Rational(nn, dd) => n/d == nn/dd
    case _ => false
end Rational

Now that contracts cover both functions and data values, we transition to formal evaluation rules encoded as code.

3) Expression Language: Abstract Syntax

We define a tiny language of integer literals, addition, and identifiers.

type Value = Int

enum Expr:
  case N(n: Value)
  case Plus(l: Expr, r: Expr)
  case I(s: String)
end Expr

This syntax gives us the structure of programs. Next we need runtime context for identifiers.

4) Runtime Context: Store for Variables

Identifiers evaluate by lookup in a store (an environment map).

import Expr.*

type Store = Map[I, Value]

With syntax and runtime state in place, we can implement the interpreter.

5) Interpreter Rules as Scala Pattern Matching

The evaluator returns both a value and the (possibly updated) store.

def eval(e: Expr, s: Store): (Value, Store) =
  e match
    case N(n) =>
      (n, s)

    case Plus(l, r) =>
      val (v1, s1) = eval(l, s)
      val (v2, s2) = eval(r, s1)
      (v1 + v2, s2)

    case i: I =>
      val v = s.getOrElse(i, throw new IllegalStateException("Unknown variable " + i.s))
      (v, s)
end eval

Notice the left-to-right evaluation order in Plus: evaluate left expression first, then right expression using the resulting store.

6) Putting It Together

A final example constructs an expression, provides a store, and runs eval.

val expr = Plus(N(5), Plus(I("x"), N(7)))
val s = Map(I("x") -> 3)

val (result, _) = eval(expr, s)
// result = 15

Week 3 code snippets cover from behavioral contracts with assertions to a compositional interpreter that mirrors formal semantics.