Pure Scala¶

The input to Stainless is a purely functional subset of Scala, which we call Pure Scala. Constructs specific for Stainless are defined inside Stainless’s libraries in package stainless and its subpackages. Stainless invokes standard scalac compiler on the input file, then performs additional checks to ensure that the given program belongs to Pure Scala.

Pure Scala supports two kinds of top-level declarations:

Algebraic Data Type (ADT) definitions in the form of an abstract class and case classes/objects

abstract class MyList
case object MyEmpty extends MyList
case class MyCons(elem: BigInt, rest: MyList) extends MyList

Objects/modules, for grouping classes and functions

object Specs {
   def increment(a: BigInt): BigInt = {
      a + 1
   }

   case class Identifier(id: BigInt)
}

Booleans¶

Booleans are used to express truth conditions in Stainless. Unlike some proof assistants, there is no separation at the type level between Boolean values and the truth conditions of conjectures and theorems.

Typical propositional operations are available using Scala notation, along with a new shorthand for implication. The if expression is also present.

a && b
a || b
a == b
!a
a ==> b // Stainless syntax for boolean implication

Stainless uses short-circuit interpretation of &&, ||, and ==>, which evaluates the second argument only when needed:

a && b  === if (a) b else false

a || b  === if (a) true else b

a ==> b === if (a) b else true

This aspect is important because of:

evaluation of expressions, which is kept compatible with Scala

2. verification condition generation for safety: arguments of Boolean operations may be operations with preconditions; these preconditions apply only in case that the corresponding argument is evaluated.

termination checking, which takes into account that only one of the paths in an if expression is evaluated for a given truth value of the condition.

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.

abstract class MyType

An abstract class can be extended by other abstract classes.

Case Classes¶

The abstract root can also 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

Note

You can also define single case-class, for Tuple-like structures.

You can add invariants to case classes using a require clause, as follows:

case class Positive(value: BigInt = 0) {
  require(value >= 0)
}

For classes without type parameters, when all fields have a default value, Stainless generates a verification condition to check that the default instance respects the invariant. In this example, the verification condition will be seen as coming from an internal function called PositiveRequireForDefault.

Note

Invariants are only allowed to refer to fields of their class, and cannot call any methods on this (but calls to methods on their fields are allowed).

Case Objects¶

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

case object BaseCase extends MyType

Value Classes¶

One can define a value class just like in standard Scala, by extending the AnyVal class.

case class Positive(value: BigInt) extends AnyVal {
  @invariant
  def isPositive: Boolean = value >= 0
}

In the code block above, we also specify an invariant of the value class, using the @invariant annotation. Such invariants are subsequently lifted into a refinement type of the underlying type.

Note

Same remark as above: invariants are only allowed to refer to fields of their class.

Generics¶

Stainless supports type parameters for classes and functions.

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 can also be marked as co- or contra-variant, eg.

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

Methods¶

You can define methods in classes.

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)

It is possible to define abstract methods in abstract classes and implement them in case classes. Multiple layers of inheritance are allowed, as is the ability to override concrete methods.

abstract class A {
  def x(a: Int): Int
}

abstract class B extends A {
  def x(a: Int) = {
    require(a > 0)
    42
 }.ensuring { _ >= 0 }
}

case class C(c: Int) extends B {
  override def x(i: Int) = {
    require(i >= 0)
    if (i == 0) 0
    else c + x(i-1)
 }.ensuring( _ == c * i )
}

case class D() extends B

It is also possible to call methods of a superclass with the super keyword.

sealed abstract class Base {
  def double(x: BigInt): BigInt = x * 2
}

case class Override() extends Base {
  override def double(x: BigInt): BigInt = {
    super.double(x + 1) + 42
  }
}

Abstract methods may have contracts in terms of pre- and postconditions. The syntax uses ??? and is as follows:

abstract class Set[T] {
  def contains[T](t: T): Boolean

  def add[T](t: T): Set[T] = {
    require(!this.contains(t))
    (??? : Set[T])
 }.ensuring(res => res.contains(t))
}

You can then extend such abstract classes by concrete implementations, and Stainless will generate verification conditions to make sure that the implementation respects the specification.

You can also add implementations and assume that they are correct with respect to the specification of the abstract class, without having Stainless check the specification (e.g. if you want to use existing Scala data-structures inside). In that case, mark the concrete class with @extern (see Section Working With Existing Code for more info on @extern) or place the concrete implementation in files which are not inspected by Stainless (see e.g. https://github.com/epfl-lara/stainless-project.g8 for an example of how to setup such a hybrid project).

Copy Method¶

The copy method of classes with immutable fields is extracted as well, and ensures that the class invariant (if any) is maintained by requiring it to be satisfied as a precondition.

case class Foo(x: BigInt) {
  require(x > 0)
}

def prop(foo: Foo, y: BigInt) = {
  require(y > 1)
  foo.copy(x = y)
}

Note

The example above would not verify without the precondition in function prop, as Foo require its field x to be positive.

Initialization¶

In Pure Scala, initialization of val’s may not have future or self-references:

object Initialization {
  case class C(x: BigInt) {
    val y = x       // ok
    val z = y + x   // ok
    val a = b       // Error: "because field `a` can only refer to previous fields, not to `b`"
    val b = z + y   // ok
  }
}

Overriding¶

Stainless supports overriding methods with some constraints: * A val in an abstract class can only be overridden by a concrete class parameter. * Methods and lazy val``s in abstract classes can be overridden by concrete methods or ``lazy val’s (interchangably), or by a concrete class parameter, but not by a val.

Here are a few examples that are rejected by Stainless:

object BadOverride1 {
  sealed abstract class Abs {
    require(x != 0)
    val x: Int
  }

  // Error: "Abstract values `x` must be overridden with fields in concrete subclass"
  case class AbsInvalid() extends Abs {
    def x: Int = 1
  }
}

object BadOverride2 {
  sealed abstract class Abs {
    val y: Int
  }

  // Error: "Abstract values `y` must be overridden with fields in concrete subclass"
  case class AbsInvalid() extends Abs {
    val y: Int = 2
  }
}

object BadOverride3 {
  sealed abstract class AAA {
    def f: BigInt
  }

  // Error: "because abstract methods BadOverride3.AAA.f were not overridden by
  //         a method, a lazy val, or a constructor parameter"
  case class BBB() extends AAA {
    val f: BigInt = 0
  }
}

Default Parameters¶

Functions and methods can have default values for their parameters.

def test(x: Int = 21): Int = x * 2

assert(test() == 42) // valid

Type Definitions¶

Type Aliases¶

Type aliases can be defined the usual way:

object testcase {
  type Identifier = String

  def newIdentifier: Identifier = /* returns a String */
}

Type aliases can also have one or more type parameters:

type Collection[A] = List[A]

def singleton[A](x: A): Collection[A] = List(x)

Type Members¶

Much like classes can have field members and method members, they can also define type members. Much like other members, those can also be declared abstract within an abstract class and overridden in implementations:

case class Grass()

abstract class Animal {
  type Food
  val happy: Boolean
  def eat(food: Food): Animal
}

case class Cow(happy: Boolean) extends Animal {
  type Food = Grass
  def eat(g: Grass): Cow = Cow(happy = true)
}

Note: Like regular type aliases, type members can also have one or more type parameters.

Type members then give rise to path-dependent types, where the type of a variable can depend on another variable, by selecting a type member on the latter:

//                             Path-dependent type
//                                 vvvvvvvvvvv
def giveFood(animal: Animal)(food: animal.Food): Animal = {
  animal.eat(food)
}

def test = {
  val cow1 = Cow(false)
  val cow2 = giveFood(cow1)(Grass())
  assert(cow2.happy) // VALID
}

Specifications¶

Stainless supports three 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 }

Body Assertions¶

Assertions constrain intermediate expressions within the body of a function.

def foo(a: Int): Int = {
  val b = -a
  assert(a >= 0 || b >= 0, "This will fail for -2^31")
  a + 1
}

The error description (last argument of assert) is optional.

Expressions¶

Stainless supports most purely-functional Scala expressions:

Pattern matching¶

expr match {
  // Simple (nested) patterns:
  case CaseClass( .. , .. , ..) => ...
  case v @ CaseClass( .. , .. , ..) => ...
  case v : CaseClass => ...
  case (t1, t2) => ...
  case 42 => ...
  case _ => ...

  // can also be guarded, e.g.
  case CaseClass(a, b, c) if a > b => ...
}

Custom pattern matching with unapply methods are also supported:

object :: {
  def unapply[A](l: List[A]): Option[(A, List[A])] = l match {
    case Nil() => None()
    case Cons(x, xs) => Some((x, xs))
  }
}

def empty[A](l: List[A]) = l match {
  case x :: xs => false
  case Nil() => true
}

Values¶

val x = ...

val (x, y) = ...

val Cons(h, _) = ...

Note

The latter two cases are actually syntactic sugar for pattern matching with one case.

Inner Functions¶

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

Local and Anonymous Classes¶

Functions and methods can declare local classes, which can close over the fields of the enclosing class, as well as the parameters of the enclosing function or method.

abstract class Foo {
  def bar: Int
}

def makeFoo(x: Int): Foo = {
  case class Local() extends Foo {
    def bar: Int = x
  }
  Local()
}

Note

Functions and methods which return an instance of a local class must have an explicit return type, which will typically be that of the parent class. Otherwise, a structural type will be inferred by the Scala compiler, and those are currently unsupported.

Anonymous classes with an explicit parent are supported as well:

abstract class Foo {
  def bar: Int
}

def makeFoo(x: Int): Foo = new Foo {
  def bar: Int = x
}

Note

Anonymous classes cannot declare more public members than their parent class, ie. the following is not supported:

abstract class Foo {
  def bar: Int
}

def makeFoo(x: Int): Foo = new Foo {
  def bar: Int = x
  def hi: String = "Hello, world"
}

Predefined Types¶

TupleX¶

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

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 32bits integers and are subject to overflows.

BigInt¶

val a = BigInt(2)
val b = BigInt(3)

-a
a + b
a - b
a * b
a / b
a % b // a modulo b
a < b
a > b
a <= b
a >= b
a == b

Note

BigInt are mathematical integers (arbitrary size, no overflows).

Real¶

Real represents the mathematical real numbers (different from floating points). It is an extension to Scala which is meant to write programs closer to their true semantics.

val a: Real = Real(2)
val b: Real = Real(3, 5) // 3/5

-a
a + b
a - b
a * b
a / b
a < b
a > b
a <= b
a >= b
a == b

Note

Real have infinite precision, which means their properties differ from Double. For example, the following holds:

def associativity(x: Real, y: Real, z: Real): Boolean = {
  (x + y) + z == x + (y + z)
} holds

While it does not hold with floating point arithmetic.

Set¶

import stainless.lang.Set // Required to have support for Sets

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

s1 ++ s2 // Set union
s1 & s2  // Set intersection
s1 -- s2 // Set difference
s1 subsetOf s2
s1 contains 42

Functional Array¶

val a = Array(1,2,3)

a(index)
a.updated(index, value)
a.length

Map¶

import stainless.lang.Map // Required to have support for Maps

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

m(index)
m isDefinedAt index
m contains index
m.updated(index, value)
m + (index -> value)
m + (value, index)
m.get(index)
m.getOrElse(index, value2)

Function¶

val f1 = (x: Int) => x + 1                 // simple anonymous function

val y  = 2
val f2 = (x: Int) => f1(x) + y             // closes over `f1` and `y`
val f3 = (x: Int) => if (x < 0) f1 else f2 // anonymous function returning another function

list.map(f1)      // functions can be passed around ...
list.map(f3(1) _) // ... and partially applied

Note

No operators are defined on function-typed expressions, so specification is currently quite limited.

Unsigned integers¶

stainless.math.Unsigned provides the unsigned integer types UByte, UShort, UInt and ULong, of 8, 16, 32 and 64 bits. They are supported for verification, by GenC (where they become uint8_t, …, uint64_t) and on the JVM, with the same semantics.

These examples are taken from Unsigned2.scala.

import stainless.math.Unsigned._

// Unsigned values are written with conversions from `Int`, `Long` or `BigInt` literals
val x1: UByte = 145.toUByte
val big: ULong = BigInt("18446744073709551615").toULong
assert(big == ULong.MaxValue)

val x2: Byte = x1.toByte // reinterpretation of the bits of an unsigned value as a signed value
assert(x2 == (-111: Byte))

// and conversely
assert(x2.toUByte == x1)

// Unsigned values can be converted to larger unsigned types (zero-extension)
val x4: UShort = x1.toUShort
assert(x4 == 145.toUShort)

// or to smaller unsigned types (truncation).
val x5: UByte = 401.toUShort.toUByte
assert(x5 == 145.toUByte) // 401 % 2^8 == 145

// Conversions to larger signed types preserve the value
assert(x1.toInt == 145)

// Signed values are sign-extended before being reinterpreted as unsigned values
assert(x2.toUShort == 65425.toUShort) // 2^16 - 111

// Constants for the minimum and maximum values
assert(UByte.MaxValue == 255.toUByte)
assert(UByte.MinValue == 0.toUByte)

Arithmetic operations (+, -, *, unary -) and << wrap around, comparisons, / and % are unsigned, and >>> is a logical shift (there is no >>). The shift amount is read as an unsigned value, and shifting by the size of the type or more yields 0. toBigInt returns the represented (non-negative) integer, which is convenient in specifications. Arrays are indexed with Ints: use a(i.toInt) for an unsigned index i.

On the JVM, the unsigned types are opaque type aliases of the signed types of the same size, which hold the same bits. The Scala compiler therefore rejects comparing an unsigned value with == to a number of another type: write x == 200.toUByte rather than x == 200. For the same reason, toString (and string interpolation) shows the signed value: use toStringUnsigned instead. Stainless treats toStringUnsigned as an uninterpreted function (it is @extern): it can be used in verified code, but nothing is known about its result, except that it only depends on its argument.

There are no implicit conversions to the unsigned types: literals are written with the conversions from the signed types and from BigInt (200.toUByte, 4000000000L.toUInt, BigInt("18446744073709551615").toULong), which Stainless extracts as literals when they are in the range of the type. Out of range, these conversions truncate their argument (300.toUByte is 44).