README.md

Leon 3.0

Getting Started

This section gives a very quick overview of how to build and use Leon; refer to the following sections if you wish (or need) more detailed information.

To build it, you will need, the following:

• Java Runtime Environment, from Oracle, e.g. Version 7 Update 5 (to run sbt and scala)
• Scala, from Typesafe, e.g. version 2.11.5
• sbt, at least version 0.13.1 (to build Leon)
• a recent GLIBC3 or later, works with e.g. apt-get (for Z3)
• GNU Multiprecision library, e.g. gmp3, works with e.g. apt-get (for Z3)

The following can be obtained from the web, but for convenience they are contained in the repository and are actually automatically handled by the default build configuration:

• ScalaZ3 hosted on GitHub
• The libz3 library from microsoft

To build, type this:

$ sbt clean
$ sbt package # takes a while
$ sbt script

Then you can try e.g.

$ ./leon ./testcases/verification/datastructures/RedBlackTree.scala

and get something like this:

  ┌──────────────────────┐
╔═╡ Verification Summary ╞════════════════════════════════════════════════════════════════════════╗
║ └──────────────────────┘                                                                        ║
║ add                        postcondition                         82:15   valid    Z3-f    0.061 ║
║ add                        precond. (call ins(x, t))             81:15   valid    Z3-f    0.004 ║
║ add                        precond. (call makeBlack(ins(x, t)))  81:5    valid    Z3-f    0.017 ║
║ balance                    match exhaustiveness                  90:5    valid    Z3-f    0.006 ║
║ balance                    postcondition                         101:15  valid    Z3-f    0.060 ║
║ blackBalanced              match exhaustiveness                  45:43   valid    Z3-f    0.003 ║
║ blackHeight                match exhaustiveness                  50:40   valid    Z3-f    0.004 ║
║ buggyAdd                   postcondition                         87:15   invalid  Z3-f    1.306 ║
║ buggyAdd                   precond. (call ins(x, t))             86:5    invalid  Z3-f    0.027 ║
║ buggyBalance               match exhaustiveness                  104:5   invalid  Z3-f    0.007 ║
║ buggyBalance               postcondition                         115:15  invalid  Z3-f    0.029 ║
║ content                    match exhaustiveness                  17:37   valid    Z3-f    0.083 ║
║ flip                       match exhaustiveness                  117:31  valid    Z3-f    0.004 ║
║ ins                        match exhaustiveness                  59:5    valid    Z3-f    0.004 ║
║ ins                        postcondition                         66:15   valid    Z3-f    1.385 ║
║ ins                        precond. (call ins(x, t.left))        62:37   valid    Z3-f    0.011 ║
║ ins                        precond. (call ins(x, t.right))       64:40   valid    Z3-f    0.012 ║
║ makeBlack                  postcondition                         77:14   valid    Z3-f    0.013 ║
║ redDescHaveBlackChildren   match exhaustiveness                  40:53   valid    Z3-f    0.004 ║
║ redNodesHaveBlackChildren  match exhaustiveness                  34:54   valid    Z3-f    0.004 ║
║ size                       match exhaustiveness                  22:33   valid    Z3-f    0.004 ║
║ size                       postcondition                         25:15   valid    Z3-f    0.048 ║
╟┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄╢
║ total: 22     valid: 18     invalid: 4      unknown 0                                     3.096 ║
╚═════════════════════════════════════════════════════════════════════════════════════════════════╝

Building Leon

Leon requires quite a few dependencies, and you will need to make sure everything is correctly set up before being able to build it. Leon is probably much easier to build on Unix-like plattforms. Not to say it is impossible to build on Windows. But some scripts used to run and test the system are shell script and you will need to manually port them to Windows if you wish to use Windows.

First you need a Java Runtime Environment. The most recent version should work. Simply follow the standard installation process (e.g. apt-get) for your system.

Next, you need the Simple Build Tool (sbt) which seems to be (as of today) the standard way to build Scala program. Again you should follow the installation procedure. You can also find information about sbt here. Sbt is quite a complex tool, so I would suggest looking at the getting started guide on the wiki page. However, if you just want to quickly build Leon and never look back, then the information provided here should be sufficient.

(This section is outdated for linux, but can be useful to adapt on Windows/Mac) Now you will have to build the ScalaZ3 project. You should follow the instructions given in the ScalaZ3 project. The ScalaZ3 is a Scala wrapper on the Z3 native library from Microsoft. It is used in Leon to make native call to Z3. The generated .jar from ScalaZ3 will be dependent on your own z3 native library, which you can obtain from here. However, the ScalaZ3 repository comes with 32 and 64 bits version for Linux and you should probably use those ones to make sure the version is compatible. You can install the Z3 native library in some standard system library path such as /usr/lib. You need to install the scalaz3.jar file in the "unmanaged" directory. The build system is configured to use any jar file in the "unmanaged" directory. Finally be aware that the Z3 library will come with its own set of dependencies, in particular you will need to have GMP. You will probably have to fight with a few errors before everything can finally work together.

Finally you can build Leon. Start sbt from a terminal to get an interactive sbt session. Then type:

> clean