tutorial.rst

Tutorial: Sorting

This tutorial shows how to:

• use ensuring, require, and holds constructs
• learn the difference between Int and BigInt
• use the choose construct for synthesis and constraint solving
• define lists as algebraic data types
• use sets and recursive function to specify data structures
• synthesize insertion into a sorted list
• synthesize sorting on lists
• repair an incorrect function

We assume that the user is using the web interface. The functionality is also available (possibly with less convenient interface) from the command line, see :ref:`gettingstarted`.

Warm-up: Max

As a warm-up we define and debug a max function in Leon and specify its properties. Leon uses Scala constructs require and ensuring to document preconditions and postconditions of functions. However, in addition to checking these conditions at run-time (which standard Scala does), Leon can analyze the specifications statically and prove them for all executions, or automatically find inputs for which the conditions fail. Moreover, it can use specifications for constraint execution, synthesis, and repair.

Consider the following definition inside an object TestMax.

object TestMax {
  def max(x: Int, y: Int): Int = {
    val d = x - y
    if (d > 0) x
    else y
  } ensuring(res =>
    x <= res && y <= res && (res == x || res == y))
}

A Leon program consists of one or more modules delimited by object and class declarations. The code of max attempts to compute maximum of two given arguments by subtracting them. If the result is positive, it returns the first one, otherwise, it returns the second one.

To specify the correctness of the computed result, we use the ensuring clause. In this case, the clause specifies that the result is larger than x and than y, and that it equals to one of them. The construct ensuring(res => P) denotes that, if we denote by res the return value of the function, then res satisfies the boolean-valued expression P. The name res we chose is an arbitrary bound variable (even though we often tend to use res).

We can evaluate this code on some values by writing parameterless functions and inspecting what they evaluate to. The web interface will display these results for us.

def test1 = max(10, 5)
def test2 = max(-5, 5)
def test3 = max(-5, -7)

The code seems to work correctly on the example values. However, Leon automatically finds that it is not correct, showing us a counter-example inputs, such as

x -> -1639624704
y -> 1879048192

We may wish to define a test method

def test4 = max(-1639624704, 1879048192)

whose evaluation indeed results in ensuring condition being violated. The problem is due to overflow of 32-bit integers, due to which the value d becomes positive, even though x is negative and thus smaller than the large positive value y. As in Scala, the Int type denotes 32-bit integers with the usual signed arithmetic operations from computer architecture and the JVM specification.

To use unbounded integers, we simply change the types to BigInt, obtaining a program that verifies (and, as expected, passes all the test cases).

def max(x: BigInt, y: BigInt): BigInt = {
  val d = x - y
  if (d > 0) x
  else y
} ensuring(res =>
  x <= res && y <= res && (res == x || res == y))

As a possibly simpler specification, we could have also defined the reference implementation

def rmax(x: BigInt, y: BigInt) = {
  if (x <= y) x else y
}

and then used as postcondition of max simply

ensuring (res =>  res == rmax(x,y))

In general, Leon uses both function body and function specification when reasoning about the function and its uses. Thus, we need not repeat in the postcondition those aspects of function body that follow directly through inlining the function, but we may wish to state those that require induction to prove.

The fact that we can use functions in preconditions and postconditions allows us to state fairly general properties. For example, the following lemma verifies a number of algebraic properties of max.

def max_lemma(x: BigInt, y: BigInt, z: BigInt): Boolean = {
  max(x,x) == x &&
  max(x,y) == max(y,x) &&
  max(x,max(y,z)) == max(max(x,y), z) &&
  max(x,y) + z == max(x + z, y + z)
} holds

Here holds operator on the function body is an abbreviation for the postcondition stating that the returned result is always true, that is, for

ensuring(res => res==true)

As a guideline, we typically use holds to express such algebraic properties that relate multiple invocations of functions, whereas we use ensuring to document property of an arbitrary single invocation of a function. Leon is more likely to automatically use the property of a function if it is associated with it using ensuring than using an external lemma.

Going back to our buggy implementation of max on Int-s, an alternative to using BigInt-s is to decide that the method should only be used under certain conditions, such as x and y being non-negative. To specify the conditions on input, we use the require clause.

def max(x: Int, y: Int): Int = {
  require(0 <= x && 0 <= y)
  val d = x - y
  if (d > 0) x
  else y
} ensuring (res =>
  x <= res && y <= res && (res == x || res == y))

This program verifies and indeed works correctly on non-negative 32-bit integers as inputs. Curiously, if we instead require x and y to be non-positive (a seemingly symmetrical specification) , the resulting program

def max(x: Int, y: Int): Int = {
  require(x <= 0 && y <= 0)
  val d = x - y
  if (d > 0) x
  else y
} ensuring (res =>
  x <= res && y <= res && (res == x || res == y))

breaks with the counterexample

x -> 0
y -> -2147483648

The reason is that there is one more negative Int than the positive Int-s, so the subtraction can still overflow in this particular case.

In the sequel we will mostly use BigInt types.

Sorting Two Elements

As a step towards sorting, let us specify a function that sorts two mathematical integers. Here is what we need to write.

import leon.lang._
import leon.lang.synthesis._
object Sort {
  def sort2(x : BigInt, y : BigInt) = choose{(res: (BigInt,BigInt)) =>
    Set(x,y) == Set(res._1, res._2) && res._1 <= res._2
  }
}

We use import to include core constructs that are specific to Leon. Note that, with the definitions in leon._ packages, Leon programs should also compile with the standard Scala compiler. In that sense, Leon is a proper subset of Scala.

Our initial function that "sorts" two mathematical integers is named sort2. Namely, it accepts two arguments, x and y, and returns a tuple, which we will here denote res, which stores either (x,y) or (y,x) such that the first component is less than equal the second component.

Note that we use BigInt to denote unbounded mathematical integers.

As usual in Scala, we write res._1 for the first component of the return tuple res, and res._2 for the second component of the tuple.

The specification says that the set of arguments is equal to the set consisting of the returned tuple elements. The notation Set(x1,x2,...,xN) denotes

\{ x_1, \ldots, x_N \}

that is, a finite set containing precisely the elements x1, x2,..., xN.

Finally, the choose construct takes a variable name (here, res) denoting the value of interest and then gives, after the => symbol, a property that this value should satisfy. We can read choose{(x:T) => P} as