Class and Companion Object

Examples

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

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

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

Pattern Matching

Pattern matching works with assignments:

(result: List[Int]) =>
  val x1 :: x2 :: x3 :: _ = result
  x1 <= x2 && x2 <= x3

Explicit match and case pattern matching is more commonplace:

(result: List[Int]) => result match
  case x1 :: x2 :: x3 :: _ =>
    x1 <= x2 && x2 <= x3

In a pattern matching expression, the first matching case is evaluated:

def f (xs: List[Int]) = xs match
  case _ => "Any list"
  case x :: Nil => s"One element $x$
end f
  
f(List(1, 2, 3)) // "Any list"
f(List(1))       // "Any list"! The first case matches.

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