LITE's USER MANUAL(well, sort of...) |
Disclaimer: This is a prototype!! And this is all the documentation we currently have. Several basic supports are still either missing or ugly, e.g. pretty printer (ugly), compiler to executables (none). Use at your own risk.
x-MECH LITE is a verification tool. It reads a program written in a language called Lingu, annotated with a Hoare-style specification, and reduces the specification to a bunch of HOL formulas. These formulas, called verification conditions or vcs, can be verified in HOL. If they can be shown to be valid, they imply the correctness of the program in question.Lingu (which is also an acronyms of little language) is currently still an experimental language. It is an imperative language, and currently only sequential. It takes the opposite direction than recent languages like Java. Rather than trying to be rich, Lingu tries to stick to the basics. For example, Lingu does not offer any OO. Lingu is intended to be a prefered language to build reliable programs, because in exchange for being simple, a Lingu program is also much easier to verify than its, for example, Java counterpart. Right now, as we're still is the development phase, some language features are still missing in Lingu. We'll add them as we go.
Lingu includes a quite expressive sub-language to specify a Lingu program in the pre/post- conditions style. The x-MECH LITE tool also supports separate verification of various aspects, enabling user, for example, to just verify that a division by zero never occurs.
x-MECH LITE is part of a bigger umbrella project, which is also called x-MECH, whose aim is to develop a technology towards scalable program verification.
If you modify the AG sources of x-MECH LITE, you will also need the AG tool to rebuild the corresponding Haskell files. You should install AG tool yourself first.
Windows users can also make use of a pre-compiled AG which can be found in the directory buildersSection/tools/AG. If you use this executable, you don't have to install AG yourself (it is however not the most recent version of AG).
If you want to test x-MECH LITE in a Haskell interpreter (e.g. hugs or ghci), you need to set-up a number of things first:
lite-install-dir/generated
lite-install-dir/src
lite-install-dir/lib lite-install-dir/lib/constraintSolver
Using winhugs that comes with Hugs release Nov 2003 is not recommended. It is buggy.
reduce filenameAssuming the file filename contains a Lingu program along with its specification, it will then be reduced to verification conditions. The results of the reduction is saved by default to a file called filename.out.std. They will not be echoed to the screen. The tool will also produce the translation of these verification conditions to HOL. This is saved in filename.hout.std.
Example: reduce --aoc bls.ls
The option --aoc will produce verification conditions to guarantee that the program will not abort because it attemps to access an array beyond its range (the program may still behave incorrectly with respect to its post-condition however).
val LITEDir = "where-x-MECH LITE-is/hollib" ;
loadPath := !loadPath @ [LITEDir] ;
use (LITEDir ^ "/litemech.smx")
read_mechout "helloWorld.ls.hout.std"
setup_goals from_mech
We give the number of KPI's (HOL Primitive Inference-steps, x1000) to give some indication to the complexity of the proofs.
Very simple examples:
Used to demonstrate the reduction of array assignment.
Used to demonstrate the generation of initial assumption regarding the sizes of locally created arrays.
Simple examples:
An efficient (linear!) program to sort an array, assuming the array only consists of three kinds of values.
The directory examples contains some examples, including those listed above. Each example has its own subdirectory. Files with extension ls or lqs are Lingu programs ---these are programs you want to verify. Each example directory already contains files storing the results of the reduction by x-MECH LITE. You don't have to redo the reduction and can proceed to verification part, which is done in HOL. If you do want to see LITE in action (thus redoing the reduction), then just go to, for example, the gcd directory under the examples and do::
reduce gcd.lsIf you want to try the light-weight-verification reduction, try for example:
reduce --aoc bls.lsOn the bounded linear search example (in the directory examples/boundedLinearSearch). Note that the simpleDBupdate example requires the -q option to be turned on. This extends Lingu syntax with database queries:
reduce -q sde.lqsThe SQL extension is still an experimental feature.
To run the HOL proof of the example in directory X, start HOL from X. Then read the xxxProof.smx file from HOL. Command:
use "filename" ;(Note the quote and the semicolon!)
Have fun!!
Authors (Wishnu Prasetya, Ade Azurat)