LAB 01 : Introduction to leon
We will introduce you to the Leon online interface to verify programs.
The Web interface is accessible at:
A tentative self-contained release is available here:
This packaged version has been tested for x86_64 and OSX 64b, we would love to hear from you if it works or fails on your setup.
Once extracted, you can use leon as follows:
$ cd path/to/extracted/ $ ./leon --xlang examples/01_Introduction.scala
You can specify one function in particular to analyze using the –functions parameter:
$ ./leon --functions=contains --xlang examples/01_Introduction.scala
Another impotant option is the –timeout one which limits the time (in seconds) a solver can spend on a verification condition.
$ ./leon --functions=contains --xlang --timeout=1 examples/01_Introduction.scala
If you experience errors such as: java.util.NoSuchElementException: None.get , make sure you included the –xlang option.