Language Reference

Scaffolding

Leon supports two kinds of top-level declarations:

1. ADT definitions in the form of an abstract class and case classes/objects

   abstract class Foo
   case class Bar(a: Int) extends Foo
   case object Gee extends Foo

2. Objects/modules, for grouping classes and functions

   object Specs {
      def foo(a: Int) = {
         a + 1
      }
   
      case class Foo(a: Int)
   }

## Algebraic Data Types

### Abstract classes
ADT roots need to be defined as abstract, unless the ADT is defined with only one case class/object. Unlike in Scala, abstract classes cannot define fields or constructor arguments.
```scala
abstract class MyType

Case classes

This abstract root can be extended by a case-class, defining several fields:

case class MyCase1(f: Type, f2: MyType) extends MyType
case class MyCase2(f: Int) extends MyType

Case objects

It is also possible to defined case objects, without fields:

case object BaseCase extends MyType

Note: You can also define single case-classes:

case class MySingleCase(f: Int)

## Generics

Leon supports type parameters for classes and functions.

```scala
object Test {
abstract class List[T]
case class Cons[T](hd: T, tl: List[T]) extends List[T]
case class Nil[T]() extends List[T]

def contains[T](l: List[T], el: T) = { ... }
}

Note: Type parameters are always invariant. It is not possible to define ADTs like:

abstract class List[T] case class Cons[T](hd: T, tl: List[T]) extends List[T] case object Nil extends List[Nothing]

> Leon in fact restricts type parameters to "simple hierarchies", where subclasses define the same type parameters in the same order.

## Methods

You can currently define methods in ADT roots:
```scala
abstract class List[T] {
def contains(e: T) = { .. }
}
case class Cons[T](hd: T, tl: List[T]) extends List[T]
case object Nil extends List[Nothing]

def test(a: List[Int]) = a.contains(42)

Specifications

Leon supports two kinds of specifications to functions and methods:

Preconditions

Preconditions constraint the argument and is expressed using require. It should hold for all calls to the function.

def foo(a: Int, b: Int) = {
  require(a > b)
  ...
}

Postconditions

Postconditions constraint the resulting value, and is expressed using ensuring:

def foo(a: Int): Int = {
  a + 1
} ensuring { res => res > a }

Expressions

Leon supports most purely-functional Scala expressions:

Pattern matching

... match {
   // Simple (nested) patterns:
   case CaseClass( .. , .. , ..) => ...
   case v @ CaseClass( .. , .. , ..) => ...
   case v : CaseClass => ...
   case (t1, t2) => ...
   case _ => ...
   // can also be guarded, e.g.
   case CaseClass(a, b, c) if a > b => ...
}

Values

val x = ...

val (x, y) = ...

Inner functions

def foo(x: Int) = {
  val y = x + 1
  def bar(z: Int) = {
     z + y
  }
  bar(42)
}

Predefined types and their methods/operators

TupleX

val x = (1,2,3)
val x = 1 -> 2 // alternative Scala syntax for Tuple2
x._1 // 1

Boolean

• a && b
• a || b
• a == b (If and only if)
• !a

Int

• a + b
• a - b
• -a
• a * b
• a / b
• a % b (a modulo b)
• a < b
• a <= b
• a > b
• a >= b
• a == b

Note: Integers are treated as mathematical integers (arbitrary size, no overflow).

Set

val s1 = Set(1,2,3,1)
val s2 = Set[Int](1,2)

• s1 ++ s2 (Set union)
• s1 & s2 (Set intersection)
• s1 -- s2 (Set difference)
• s1 subsetOf s2
• s1 contains 42

Array

val a = Array(1,2,3)

• a(index) (Array access)
• a.apply(index) (Array access)
• a.updated(index, value) (Returns new updated array)
• a.length (Array size)

Map

val  m = Map[Int, Boolean](42 -> false)

• m(index) (Map access)
• m.apply(index) (Map access)
• m isDefinedAt index
• m contains index
• m.updated(index, value) (Returns the new updated map)