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 Getting Started.
Warm-up: Max¶
As a warm-up illustrating verification, we define and debug a max function and specify its properties. Leon uses Scala constructs require and ensuring to document preconditions and postconditions of functions. Note that, 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, if they are wrong, automatically find inputs for which the conditions fail. (Moreover, it can execute specifications alone without the code, it can do 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) y else x
}
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.
Question: What if we restrict the inputs to max to be a) non-positive, or b) strictly negative? Modify the require clause for each case accordingly and explain the behavior of Leon.
In the sequel we will mostly use BigInt types.
Let us now look at synthesis. Suppose we omit the implementation of max, keeping the specification in the ensuring clause but using only a placeholder ???[BigInt] indicating we are looking for an unknown implementation of an integer type.
def max(x: BigInt, y: BigInt): BigInt = {
???[BigInt]
} ensuring(res => (res == x || res == y) && x <= res && y <= res)
Leon can then automatically generate an implementation that satisfies this specification, such as
if (y <= x) {
x
} else {
y
}
This is remarkable because we have much more freedom in writing specifications: we can explain the intention of the computation using a conjunction of orthogonal properties, and still obtain automatically an efficient implementation.
As a remark, an expression with missing parts in Leon is an abbreviation for Leon’s choose construct. Using choose we can write the above example as
def max(x: BigInt, y: BigInt): BigInt = choose((res:BigInt) =>
(res == x || res == y) && x <= res && y <= res)
We explain choose in more detail through our subsequent examples.
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.Set
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
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
choose x of type T such that P
Here, we are interested in computing a result res tuple such that the set of elements in the tuple is the same as {x,y} and that the elements are in ascending order in the tuple. The specification thus describes sorting of lists of length two. Note that the result is uniquely specified, no matter what the values of x and y are.
Evaluating exppressions containing choose¶
Leon’s built-in evaluator also works for choose constructs. To see it in action in the web interface, just define a function without parameters, such as
def testSort2 = sort2(30, 4)
Hovering over testSort2 should display the computed result (4,30). (From Command Line Options, use –eval.)
Thanks to the ability to execute choose constructs Leon supports programming with fairly general constraints. Executing the choose construct is, however, expensive. Moreover, the execution times are not very predictable. This is why it is desirable to eventually replace your choose constructs with more efficient code. Leon can automate this process in some cases, using synthesis.
Synthesizing Sort for Two Elements¶
Instead of executing choose using a constraint solver during execution, we can alternatively instruct Leon to synthesize a function corresponding to choose. The system then synthesizes a computation that satisfies the specification, such as, for, example:
def sort2(x : BigInt, y : BigInt): (BigInt, BigInt) = {
if (x < y)
(x, y)
else
(y, x)
}
Depending on the particular run, Leon may also produce a solution such as
def sort2(x : BigInt, y : BigInt): (BigInt, BigInt) = {
if (x < y) {
(x, y)
} else if (x == y) {
(x, x)
} else {
(y, x)
}
}
This code performs some unnecessary case analysis, but still satisfies our specification. In this case, the specification of the program output is unambiguous, so all programs that one can synthesize compute the same results for all inputs.
Remarks on Uniqueness¶
Let us give a name to the specification for sort2.
def sort2spec(x: BigInt, y: BigInt, res: (BigInt, BigInt)): Boolean = {
Set(x,y) == Set(res._1, res._2) && res._1 <= res._2
}
We can then prove that the result is unique, by asking Leon to show the following function returns true for all inputs for which the require clause holds.
def unique2(x: BigInt, y: BigInt,
res1: (BigInt, BigInt),
res2: (BigInt, BigInt)): Boolean = {
require(sort2spec(x,y,res1) && sort2spec(x,y,res2))
res1 == res2
}.holds
In contrast, if we define the corresponding specification for three integers
def sort3spec(x: BigInt, y: BigInt, z: BigInt, res: (BigInt, BigInt, BigInt)): Boolean = {
Set(x,y,z) == Set(res._1, res._2, res._3) &&
res._1 <= res._2 && res._2 <= res._3
}
Then uniqueness of the solution is the following conjecture:
def unique3(x: BigInt, y: BigInt, z: BigInt,
res1: (BigInt, BigInt, BigInt),
res2: (BigInt, BigInt, BigInt)): Boolean = {
require(sort3spec(x,y,z,res1) && sort3spec(x,y,z,res2))
res1 == res2
}.holds
This time, however, Leon will report a counterexample, indicating that the conjecture does not hold. One such counterexample is 0, 1, 1, for which the result (0, 0, 1) also satisfies the specification, because sets ignore the duplicates, so
Set(x,y,z) == Set(res._1, res._2, res._2)
is true. This shows that writing specifications can be subtle, but Leon’s capabilities can help in the process as well.
Question: Write the specification that requires the output triple to be strictly sorted using the < relation. Use choose to define the corresponding sort3 function. Try executing such specifications for example inputs. What happens if you execute it when two of the elements are equal? Write the require clause to enforce the precondition that the initial elements are distinct. Formulate in Leon the statement that for triples of distinct elements the result of strictly ordering them is unique and try to prove it.
Interactive Exploration of Program Space¶
For larger programs, the search may take too long to find the solution and Leon will time out. In such cases, instead of invoking automated search, you can invoke Leon in the mode where the user directs each synthesis step to be provided. This is a great way to understand the rules that Leon currently has available for performing synthesis.
In the web interface, select on the synthesis task for sort2 specification using the choose construct and select Explore instead of the automated Search. You can then navigate the space of programs interactively. Select the Inequality split between the two input variables. The system will apply this inference rule, and transform the program with one choose into a program that performs case analysis and then performs choose in each branch. For individual branches we can try to resolve them using the CEGIS synthesis rule, which searches for small expressions and tries to find the one that satisfies the specification. We can use Equivalent Inputs and Unused Inputs as needed, since they are generally a good idea to apply. Once all sub-goals are resolved, select Import Code. Note that you can import any of the intermediate steps in exploration: the program with choose is valid in Leon, and it can even be executed, thanks to run-time constraint solving for the cases containing choose.
Question: Use interactive exploration to synthesize sort3 function by performing inequality splits in the interactive interface. Given three variables, you will need to perform inequality splits on their pairs until the tuple to be returned is known thanks to the tests performed in the code. This is a somewhat tedious process, but relatively easy, and the result is guaranteed to be correct.
Defining Lists and Their Properties¶
We next consider sorting an unbounded number of elements. For this purpose, we define a data structure for lists of integers. Leon has a built-in data type of parametric lists, see Leon Library, but here we define our own variant instead.
Lists¶
We use a recursive algebraic data type definition, expressed using Scala’s case classes.
sealed abstract class List
case object Nil extends List
case class Cons(head: BigInt, tail: List) extends List
We can read the definition as follows: the set of lists is defined as the least set that satisfies them:
- empty list Nil is a list
- if head is an integer and tail is a List, then Cons(head,tail) is a List.
Each list is constructed by applying the above two rules finitely many times. A concrete list containing elements 5, 2, and 7, in that order, is denoted
Cons(5, Cons(2, Cons(7, Nil)))
Having defined the structure of lists, we can move on to define some semantic properties of lists that are of interests. For this purpose, we use recursive functions defined on lists.
Size of a List¶
As the starting point, we define size of a list.
def size(l: List) : BigInt = (l match {
case Nil => 0
case Cons(x, rest) => 1 + size(rest)
})
The definition uses pattern matching to define size of the list in the case it is empty (where it is zero) and when it is non-empty, or, if its non-empty, then it has a head x and the rest of the list rest, so the size is one plus the size of the rest. Thus size is a recursive function. A strength of Leon is that it allows using such recursive functions in specifications.
It makes little sense to try to write a complete specification of size, given that its recursive definition is already a pretty clear description of its meaning. However, it is useful to add a consequence of this definition, namely that the size is non-negative. The reason is that Leon most of the time reasons by unfolding size, and the property of size being non-negative is not revealed by such unfolding. Once specified, the non-negativity is easily proven and Leon will make use of it.
def size(l: List) : BigInt = (l match {
case Nil => 0
case Cons(x, rest) => 1 + size(rest)
}) ensuring(res => res >= 0)
Sorted Lists¶
We define properties of values simply as executable predicates that check if the property holds. The following is a property that a list is sorted in a strictly ascending order.
def isSorted(l : List) : Boolean = l match {
case Nil => true
case Cons(_,Nil) => true
case Cons(x1, Cons(x2, rest)) =>
x1 < x2 && isSorted(Cons(x2,rest))
}
Insertion into Sorted List¶
Consider the following specification of insertion into a sorted list, which is a building block for an insertion sort.
def sInsert(x : BigInt, l : List) : List = {
require(isSorted(l))
l match {
case Nil => Cons(x, Nil)
case Cons(e, rest) if (x == e) => l
case Cons(e, rest) if (x < e) => Cons(x, Cons(e,rest))
case Cons(e, rest) if (x > e) => Cons(e, sInsert(x,rest))
}
} ensuring {(res:List) => isSorted(res)}
Leon verifies that the returned list is indeed sorted. Note how we are again using a recursively defined function to specify another function. We can introduce a bug into the definition above and examine the counterexamples that Leon finds.
Being Sorted is Not Enough¶
Note, however, that a function such as this one is also correct.
def fsInsert(x : BigInt, l : List) : List = {
require(isSorted(l))
Nil
} ensuring {(res:List) => isSorted(res)}
So, our specification may be considered weak, because it does not say anything about the elements.
Using Size in Specification¶
Consider a stronger additional postcondition property:
size(res) == size(l) + 1
Does it hold? If we try to add it, we obtain a counterexample. A correct strengthening, taking into account that the element may or may not already be in the list, is the following.
size(l) <= size(res) && size(res) <= size(l) + 1
Using Content in Specification¶
A stronger specification needs to talk about the content of the list.
def sInsert(x : BigInt, l : List) : List = {
require(isSorted(l))
l match {
case Nil => Cons(x, Nil)
case Cons(e, rest) if (x == e) => l
case Cons(e, rest) if (x < e) => Cons(x, Cons(e,rest))
case Cons(e, rest) if (x > e) => Cons(e, sInsert(x,rest))
}
} ensuring {(res:List) =>
isSorted(res) && content(res) == content(l) ++ Set(x)}
To compute content, in this example we use sets (even though in general it might be better in general to use bags i.e. multisets).
def content(l: List): Set[BigInt] = l match {
case Nil => Set()
case Cons(i, t) => Set(i) ++ content(t)
}
Sorting Specification and Running It¶
Specifying sorting is in fact very easy.
def sortMagic(l : List) = {
???[List]
} ensuring((res:List) =>
isSorted(res) && content(res) == content(l))
We can execute such a sort.
def mm = sortMagic(Cons(20, Cons(5, Cons(50, Cons(2, Nil)))))
obtaining the expected Cons(2, Cons(5, Cons(20, Cons(50, Nil)))). Note that the function actually removes duplicates from the input list.
Synthesizing Sort¶
By asking the system to synthesize the choose construct inside magicSort, we may obtain a function such as the following, which gives us the natural insertion sort.
def sortMagic(l : List): List = {
l match {
case Cons(head, tail) =>
sInsert(head, sortMagic(tail))
case Nil => Nil
}
}
Going back and Synthesizing Insertion¶
In fact, if we have a reasonably precise enough specification of insert, we can synthesize the implementation. To try this, remove the body of sInsert and replace it with ???[List] denoting an unknown value of the given type.
def sInsert(x : BigInt, l : List) : List = {
require(isSorted(l))
???[List]
} ensuring {(res:List) =>
isSorted(res) && content(res) == content(l) ++ Set(x)}
Leon can then synthesize the missing part, resulting in a similar body to the one we wrote by hand originally.
Repairing an Incorrect Function¶
You may notice that synthesis can take a long time and fail. Often we do produce some version of the program, but it is not correct according to a specification. Consider the following attempt at sInsert.
def sInsert(x : BigInt, l : List) : List = {
require(isSorted(l))
l match {
case Nil => Cons(x, Nil)
case Cons(e, rest) => Cons(e, sInsert(x,rest))
}
} ensuring {(res:List) =>
isSorted(res) && content(res) == content(l) ++ Set(x)}
Leon reports a counterexample to the correctness. Instead of trying to manually understand the counterexample, we can instruct the system to repair this solution. If Leon can reuse parts of the existing function, it can be much faster than doing synthesis from scratch. Leon automatically finds test inputs that it uses to localize the error and preserve useful existing pieces of code. In this case, Leon repairs the above function into the one equivalent to the original one, by doing a case split and synthesizing two new cases, resulting in the following equivalent function.
def sInsert(x : BigInt, l : List): List = {
require(isSorted(l))
l match {
case Nil => Cons(x, Nil)
case Cons(e, rest) =>
if (x < e) Cons(x, l)
else if (x == e) Cons(x, rest)
else Cons(e, sInsert(x, rest))
} ensuring { (res : List) =>
isSorted(res) && content(res) == content(l) ++ Set[BigInt](x) }
This completes the tutorial. To learn more, check the rest of this documentation and browse the examples provided with Leon.