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 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 (a subtraction overflow) and provides a counterexample that we can add to our test suite.

assert(max(0, -2147483648) == -2147483646)

Adding a contract further increases confidence:

def max(x: Int, y: Int): Int = {
  // x > y rewritten as x - y > 0
  if x - y > 0 then x else y
} ensuring {
  (result: Int) => result == (if x > y then x else y)
}

Verification with Scala Stainless identifies that the implementation is not equivalent to the contract.

3) Expression Language: Abstract Syntax

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

type Value = Int

enum Expr:
  case Number(n: Value)
  case Plus(l: Expr, r: Expr)
  case Par(e: Expr)
  case Ident(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[Ident, 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. The function signature eval(e: Expr, s: Store) : (Value, Store) directly reflects the form of judgments in the class’s operational semantics. The function body lists one case per rule of the semantics.

def eval(e: Expr, s: Store) : (Value, Store) = e match
  case Number(n) => (n, s)
  case Par(f) =>
    // val (v, s1) = eval(f, s)
    // (v, s1)
    eval(f, s)
  case Plus(e1, e2) =>
    val (v1, s1) = eval(e1, s)
    val (v2, s2) = eval(e2, s1)
    (v1+v2, s2)
  case Ident(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 e = Plus(Number(3), Number(4))
val (v, _) = eval(e, Map.empty)
println(v)
// result = 7

Instantiating the algebraic datatype using its constructors is inconvenient. We introduce a + operator for expressions:

extension (e: Expr)
  def +(that: Expr) = Plus(e, that)

val e = Number(3) + Number(4)

Next, we abbreviate turning integer literals into numbers with an extension method of Int:

extension (n: Int)
  def n = Number(n)

val e = 3.n + 4.n

Finally, we add implicit conversion from Int to Expr and an operator +~ to avoid + of integers (3+4 is integer addition, not addition of Expr) and thus force implicit conversion.

extension (e: Expr)
  def +(that: Expr) = Plus(e, that)
  // to force implicit type conversion from Int to Expr
  def +~(that: Expr) = e + that

extension (n: Int)
  def n = Number(n)

given Conversion[Int, Expr]:
  def apply(x: Int) = Number(x)

val e = 3 +~ 4 // 3.n + 4 // 3.n + 4.n //Number(3) + Number(4) // Plus(Number(3), Number(4))
val (v, _) = eval(e, Map.empty)
println(v)

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