Verification¶
Software verification aims at making software safer. In its typical use case, it is a tool that takes as input the source code of a program with specifications as annotations and attempt to prove — or disprove — their validity.
One of the core module of Leon is a verifier for the subset of Scala described in the sections Pure Scala and XLang. In this section we describe the specification language that can be used to declare properties of programs, as well as the safety properties automatically checked by Leon. We also discuss how Leon can be used to prove mathematical theorems.
Verification conditions¶
Given an input program, Leon generates individual verification conditions corresponding to different properties of the program. A program is correct if all of the generated verification conditions are valid. The validity of some conditions depends on the validity of other conditions — typically a postcondition is valid assuming the precondition is valid.
For each function, Leon attempts to verify its contract, if there is one. A contract is the combination of a precondition and a postcondition. A function meets its contract if for any input parameter that passes the precondition, the postcondition holds after executing the function. Preconditions and postconditions are annotations given by the user — they are the specifications and hence cannot be inferred by a tool and must be provided.
In addition to user-provided contracts, Leon will also generate a few safety verification conditions of its own. It will check that all of the array accesses are within proper bounds, and that pattern matching always covers all possible cases, even given complex precondition. The latter is different from the Scala compiler checks on pattern matching exhaustiveness, as Leon considers information provided by (explicit or implicit) preconditions to the match expression.
Postconditions¶
One core concept in verification is to check the contract of functions. The most important part in a contract is the postcondition. The postcondition specifies the behaviour of the function. It takes into account the precondition and only asserts the property of the output when the input satisfies the precondition.
Formally, we consider a function with a single parameter (one can generalize the following for any number of parameters):
def f(x: A): B = {
require(prec)
body
} ensuring(r => post)
where, \(\mbox{prec}(x)\) is a Boolean expression with free variables contained in \(\{ x \}\), \(\mbox{body}(x)\) is an expression with free variables contained in \(\{ x \}\) and \(\mbox{post}(x, r)\) is a Boolean expression with free variables contained in \(\{ x, r \}\). The types of \(x\) and \(r\) are respectively A and B. We write \(\mbox{expr}(a)\) to mean the substitution in \(\mbox{expr}\) of its free variable by \(a\).
Leon attempts to prove the following theorem:
If Leon is able to prove the above theorem, it returns valid for the function f. This gives you a guarantee that the function f is correct with respect to its contract.
However, if the theorem is not valid, Leon will return a counterexample to the theorem. The negation of the theorem is:
and to prove the validity of the negation, Leon finds a witness \(x\) — a counterexample — such that the precondition is verified and the postcondition is not.
The general problem of verification is undecidable for a Turing-complete language, and the Leon language is Turing-complete. So Leon has to be incomplete in some sense. Generally, Leon will eventually find a counterexample if one exists. However, in practice some program structures require too many unrollings and Leon is likely to timeout (or being out of memory) before finding the counterexample. When the postcondition is valid, it could also happen that Leon keeps unrolling the program forever, without being able to prove the correctness. We discuss the exact conditions for this in the chapter on Leon’s algorithms.
Preconditions¶
Preconditions are used as part of the contract of functions. They are a way to restrict the input to only relevant inputs, without having to implement guards and error handling in the functions themselves.
Preconditions are contracts that the call sites should respect, and thus are not checked as part of verifying the function. Given the following definition:
def f(x: A): B = {
require(prec)
body
}
For each call site in the whole program (including in f itself):
...
f(e)
...
where the expression \(\mbox{e}(x)\) is an expression of type A with free variables among \(\{ x \}\). Let us define the path condition on \(x\) at that program point as \(\mbox{pc}(x)\). The path condition is a formula that summarizes the facts known about \(x\) at that call site. A typical example is when the call site is inside an if expression:
if(x > 0)
f(x)
The path condition on \(x\) would include the fact that \(x > 0\). This path condition is then used as a precondition of proving the validity of the call to \(\mbox{f}\). Formally, for each such call site, Leon will attempt to prove the following theorem:
Leon will generates one such theorem for each static call site of a function with a precondition.
Note
Leon only assumes an open program model, where any function could be called from outside of the given program. In particular, Leon will not derive a precondition to a function based on known information in the context of the calls, such as knowing that the function is always given positive parameters. Any information needed to prove the postcondition will have to be provide as part of the precondition of a function.
Loop invariants¶
Leon supports annotations for loop invariants in XLang. To simplify the presentation we will assume a single variable \(x\) is in scope, but the definitions generalize to any number of variables. Given the following program:
(while(cond) {
body
}) invariant(inv)
where the Boolean expression \(\mbox{cond}(x)\) is over the free variable \(x\) and the expression \(\mbox{body}(x, x')\) relates the value of \(x\) when entering the loop to its updated value \(x'\) on loop exit. The expression \(\mbox{inv}(x)\) is a Boolean formula over the free variable \(x\).
- A loop invariant must hold:
- when the program enters the loop initially
- after each completion of the body
- right after exiting the loop (when the condition turns false)
Leon will prove point (1) and (2) above. Together, and by induction, they imply that point (3) holds as well.
Array access safety¶
Leon generates verification conditions for the safety of array accesses. For each array variable, Leon carries along a symbolic information on its length. This information is used to prove that each expression used as an index in the array is strictly smaller than that length. The expression is also checked to be positive.
Pattern matching exhaustiveness¶
Leon verifies that pattern matching is exhaustive. The regular Scala compiler only considers the types of expression involved in pattern matching, but Leon will consider information such as precondition to formally prove the exhaustiveness of pattern matching.
As an example, the following code should issue a warning with Scala:
abstract class List
case class Cons(head: Int, tail: List) extends List
case object Nil extends List
def getHead(l: List): Int = {
require(!l.isInstanceOf[Nil])
l match {
case Cons(x, _) => x
}
}
But Leon will prove that the pattern matching is actually exhaustive, relying on the given precondition.
Pretty-printing¶
If a global function name ends with “toString” with any case, has only one argument and returns a string, this function will be used when printing verification examples. This function can be synthesized (see the synthesis section). For example,
def intToString(i: Int) = "#" + i.toString + ",..."
def allIntsAreLessThan9(i: Int) = i <= 9 holds
It will display the counter example for allIntsAreLessThan9 as:
Counter-example: #10,...