If you are interested in reading through some larger examples, the code snippets include links to a theorem prover project implemented in Scala.

Class and Companion Object

Examples of uses of object and companion objects in a large Scala project:

• Implementation of code locations for error messages of a parser: Region
• Parser errors and factory methods to create them: ParseException
• A string to abstract syntax tree converter (also illustrates implicit conversions): StringConverter
• Finite, infinite, and cofinite set implementations with symbolic method names: SetLattice

Expressions, Conditionals

Non-Strict Function Arguments

In Java, we can use objects with methods to defer evaluation. In order to make updates to local variables visible, we have to use heap-allocated references (does not work with stack-allocated primitive values).

public class Expressions {
  // A modifiable heap-allocated int
  private static class RefInt {
    public int n;
    public RefInt(int n) { this.n = n; }    
    @Override
    public String toString() {
      return Integer.valueOf(n).toString();
    }
  }

  // A "function" that can be run
  private static class F {
    private int result;
    private RefInt n;
    private int i;
    public F(int result, RefInt n, int i) {
      this.result = result;
      this.n = n;
      this.i = i;
    }

    public int run() {
      n.n = i;
      return result;
    }
  }

  private static int fcond(Boolean b, F t, F f) {
    return b ? t.run() : f.run();
  }

  public static void main(String[] args) {
    RefInt x = new RefInt(0);
    RefInt y = new RefInt(0);

    var z = fcond(
      new java.util.Random().nextInt() % 2 == 0,
      new F(111, x, 1),
      new F(222, y, 2)
    );
    System.out.println(String.format("x=%s, y=%s, z=%s", x, y, z));    
  }
}

In C/C++, we can use function pointers as arguments to defer evaluation of expensive computations. Unfortunately, the C standard does not allow nested functions: side-effects like updating local variables are not possible, but we can update global variables in that way.

#include <stdbool.h>
#include <stdlib.h>
#include <stdio.h>
#include <time.h>

int x = 0;
int y = 0;

int f1() {
  x = 1;  
  return 111;
}

int f2() {
  y = 2;
  return 222;
}

int fcond(bool b, int (*t)(), int (*f)()) {
  return b ? t() : f();
}

int main(int argc, char** argv) {
  srand(time(NULL));
  int z = fcond(
    rand() % 2 == 0,
    f1,
    f2
  );
  printf("x=%d, y=%d, z=%d\n", x, y, z);
  return 0;
}

In non-idiomatic Scala, we can implement the object-oriented Java solution using more concise syntax (exploiting var class arguments):

object Expressions:

  class RefInt(var n: Int):
    override def toString() = n.toString

  class F(val result: Int, val n: RefInt, val i: Int):
    def run(): Int = 
      n.n = i
      result
    end run
  end F

  def fcond(b: Boolean, t: F, f: F) : Int =
    if b then t.run() else f.run()
  end fcond

  def main(args: Array[String]) =
    var x : RefInt = new RefInt(0)
    var y : RefInt = new RefInt(0)

    var z = fcond(
      scala.util.Random().nextInt % 2 == 0,
      new F(111, x, 1),
      new F(222, y, 2)
    )
    println(s"x=$x, y=$y, z=$z")    
  end main
end Expressions

Idiomatic Scala uses function arguments or thunks to achieve the same effect; those are allowed to access local variables, which entirely eliminates the need for a modifiable heap-shared integer container:

object Expressions:
  def fcond2(b: Boolean, t: () => Int, f: () => Int) : Int =
    if b then t() else f()

  def fcond3(b: Boolean, t: => Int, f: => Int) : Int =
    if b then t else f

  def main(args: Array[String]) =
    var x = 0
    var y  = 0

    fcond2(scala.util.Random().nextInt % 2 == 0,    
      () => { x = 1; 111 },
      () => { y = 2; 222 }
      )
    println(s"x=$x, y=$y, z=$z")
    
    x = 0
    y = 0
    fcond3(scala.util.Random().nextInt % 2 == 0,
      { x = 1; 111 },
      { y = 2; 222 }
      )
    println(s"x=$x, y=$y, z=$z")
  end main

end Expressions

Examples

Examples of uses of expressions and non-strict evaluation in a large Scala project:

• A startup (main) class for a theorem prover with command line options KeYmaeraXCore
• Thunks in exceptions: method inContext

Contracts

Examples of uses of contracts in a large Scala project:

• Consistency checks in a lemma database Lemma, LemmaDBBase

Formal Semantics

Syntax

Below is a grammar for integer expressions. The non-terminal symbol Number is not expanded further, it is assumed to define the usual syntax of signed integer literals.

Expr ::= Number
       | Expr '+' Expr 
       | Expr '-' Expr 
       | Expr '*' Expr 
       | '(' Expr ')'

Rules

Below are reduction rules for our language of integer expressions. The store \(\xi\) is irrelevant in this language without variables and just passed on unmodified.

Define the Semantics of Multiplication

Analogous to addition and subtraction, define the reduction rule for multiplication.

\(\frac{}{\langle \mathtt{e}_1 \mathtt{*} \mathtt{e}_2,\xi\rangle \Downarrow \langle ~~~~~~~~~~~~ \rangle}\text{\tiny(Mul)}\)

Solution: Semantics of Multiplication

Annotate Rules

Annotate the missing rule names in the reduction of \(\mathtt{(2*3)}\) to its integer value.

Solution: Annotate Rules

Fill in the Proof

Reduce the expression \(\mathtt{(2*3) * 4}\) to its integer value.

Solution: Evaluate Expression

Solutions

Solution: Semantics of Multiplication

\(\frac{\langle \mathtt{e}_1,\xi \rangle \Downarrow \langle v_1,\xi \rangle ~~ \langle \mathtt{e}_2,\xi \rangle \Downarrow \langle v_2,\xi \rangle}{\langle \mathtt{e}_1 \mathtt{*} \mathtt{e}_2,\xi\rangle \Downarrow \langle v_1 \cdot v_2,\xi\rangle}\text{\tiny(Mul)}\)

Solution: Annotate Rules

Solution: Evaluate Expression