intro.rst

Introduction

The Leon system aims to help developers build verified Scala software. It encourages using a small set of core Scala features, but provides unique automation functionality. In particular, Leon can

• verify statically that your program confirms to a given specification and that it cannot crash at run-time
• repair a program for you to ensure that the above holds
• automatically execute and synthesize working functions from partial input/output specifications and test cases.

Leon and Scala

Leon attempts to strike a delicate balance between the convenience of use on the one hand and the simplicity of reasoning on the other hand. Leon primarily supports programs written in :ref:`Pure Scala <purescala>`, a purely functional subset of Scala. This fragment is at the core of the functional programming paradigm and lies at the intersection of functional languages such as Scala, Haskell, ML, and fragments present in interactive theorem provers such as Isabelle and Coq. Thus, if you do not already know Scala, learning the Leon subset should be easier as it is a smaller language. The :ref:`Pure Scala <purescala>` features are at the core of the Leon system. They are considered as primitives and get a personalized treatment in the solving algorithms of Leon. Leon's algorithms can map this fragment into the first-order language of SMT (satisfiability modulo theory) solvers, enabling efficient automated reasoning. Moreover, thanks to the use of scalac front end, Leon supports implicits and for comprehensions (which also serve as a syntax for monads in Scala). Leon also comes with a simple library of useful data types, which are designed to work well with automated reasoning and Leon's language fragment.

In addition to this pure fragment, Leon supports the :ref:`XLang <xlang>` extension, which enables Leon to work on a richer subset of Scala, including imperative features. Features introduced by :ref:`XLang <xlang>` are handled by translation into Pure Scala concepts. They are often more than just syntactic sugar, because some of them require significant modification of the original program, such as introducing additional parameters to a set of functions. As an intended aspect of its current design, Leon's language currently does not provide a default encoding of e.g. concurrency with a shared mutable heap, though it might support more manageable forms of concurrency in the future. For practical reasons, Leon programs can also call out into general Scala code, which needs to be used with care as it is a form of "foreign function interface" into the general world of Scala.

If you would like to use Leon now, check the :ref:`Getting Started <gettingstarted>` section and try our :ref:`Tutorial <tutorial>`. To learn more about the functionality that Leon provides, read on below.

Software Verification

Leon started out as a program verifier for :ref:`Pure Scala <purescala>`. It would collect a list of top level functions written in Pure Scala, and verifies the validity of their contracts. Essentially, for each function, it would prove that the postcondition always hold, assuming a given precondition does hold. A simple example:

def factorial(n: Int): Int = {
  require(n >= 0)
  if(n == 0) {
    1
  } else {
    n * factorial(n - 1)
  }
} ensuring(res => res >= 0)

Leon generates a postcondition verification condition for the above function, corresponding to the predicate parameter to the ensuring expression. It attempts to prove it using a combination of an internal algorithm and external automated theorem proving. Leon will return one of the following:

• The postcondition is valid. In that case, Leon was able to prove that for any input to the function satisfying the precondition, the postcondition will always hold.
• The postcondition is invalid. It means that Leon disproved the postcondition and that there exists at least one input satisfying the precondition and such that the postcondition does not hold. Leon will always return a concrete counterexample, very useful when trying to understand why a function is not satisfying its contract.
• The postcondition is unknown. It means Leon is unable to prove or find a counterexample. It usually happens after a timeout or an internal error occurring in the external theorem prover.

Leon will also verify for each call site that the precondition of the invoked function cannot be violated.

Leon supports verification of a significant part of the Scala language, described in the sections :ref:`Pure Scala <purescala>` and :ref:`XLang <xlang>`.

Program Synthesis

As seen with verification, specifications provide an alternative and more descriptive way of characterizing the behavior of a function. Leon defines ways to use specifications instead of an actual implementation within your programs:

• a choose construct that describes explicitly a value with a specification. For instance, one could synthesize a function inserting into a sorted list by:

def insert1(in: List, v: BigInt) = {
  require(isSorted(in1))
  choose { (out: List) =>
    (content(out) == content(in1) ++ Set(v)) && isSorted(out)
  }
}

• a hole (???) that can be placed anywhere in a specified function. Leon will fill it with values such that the overall specification is satisfied. This construct is especially useful when only a small part of the function is missing.

def insert2(in: List, v: BigInt) = {
  require(isSorted(in1))
  in match {
    case Cons(h, t) =>
      if (h < v) {
        Cons(h, in)
      } else if (h == v) {
        in
      } else {
         ???[List]
      }
    case Nil =>
      Nil
  }
} ensuring { out =>
  (content(out) == content(in1) ++ Set(v)) && isSorted(out)
}

Given such programs, Leon can:

1) Execute them: when the evaluator encounters a choose construct, it solves the constraint at runtime by invoking an SMT solver. This allows some form of constraint solving programming.

2) Attempt to translate specifications to a traditional implementation by applying program synthesis. In our case, Leon will automatically synthesize the hole in insert2 with Cons(h, insert2(v, t)). This automated translation is described in further details in the section on :ref:`synthesis <Synthesis>`.

Program Repair

Leon can repair buggy :ref:`Pure Scala <purescala>` programs. Given a specification and an erroneous implementation, Leon will localize the cause of the bug and provide an alternative solution. An example:

def moddiv(a: Int, b: Int): (Int, Int) = {
  require(a >= 0 && b > 0);
  if (b > a) {
    (1, 0) // fixme: should be (a, 0)
  } else {
    val (r1, r2) = moddiv(a-b, b)
    (r1, r2+1)
  }
} ensuring {
  res =>  b*res._2 + res._1 == a
}

Invoking leon --repair --functions=moddiv will yield:

...
[  Info  ] Found trusted solution!
[  Info  ] ============================== Repair successful: ==============================
[  Info  ] --------------------------------- Solution 1: ---------------------------------
[  Info  ] (a, 0)
[  Info  ] ================================= In context: =================================
[  Info  ] --------------------------------- Solution 1: ---------------------------------
[  Info  ] def moddiv(a : Int, b : Int): (Int, Int) = {
             require(a >= 0 && b > 0)
             if (b > a) {
               (a, 0)
             } else {
               val (r1, r2) = moddiv(a - b, b)
               (r1, (r2 + 1))
             }
           } ensuring {
             (res : (Int, Int)) => (b * res._2 + res._1 == a)
           }

Repair assumes a small number of localized errors. It first invokes a test-based fault localization algorithm, and then a special synthesis procedure, which is partially guided by the original erroneous implementation. For more information, see the section on :ref:`Repair <repair>`.