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.

System Requirement

  1. HOL4 Theorem Prover, release Kananaskis 2. Note that HOL also requires MOSML --this is explained in HOL's instalation document.
  2. Win2000,NT,XP; UNIX.

User's Instalation

Developer's Instalation

To build x-MECH LITE, see the UNIX User's Instalation above. If you're on Windows you will need cygwin or some other makefile-enabler utility.

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:

  1. Extend the search path of hugs/ghci with these:
    lite-install-dir/generated
    lite-install-dir/src
    lite-install-dir/lib lite-install-dir/lib/constraintSolver
  2. Turn on the +o option (overlapping instance)

  3. Hugs should be called with -98 option.

Using winhugs that comes with Hugs release Nov 2003 is not recommended. It is buggy.

Using x-MECH LITE

  1. Use x-MECH LITE to generate the verification conditions (VCs) for a given specification. Suppose you have a file called helloWorld.ls in directory c:/tmp, containing the specification of some uPL program. Here are the steps to generate the VCs:

    1. Look in the bin directory of your x-MECH LITE. There is a file called reduce.exe. To use it, just call the program from your command shell. If you don't give any argument it will print a help information explaining its use.

    2. The simplest use of reduce is just:
      reduce filename
      Assuming 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.

    3. You can also call reduce with options. Check out its help screen for available options. Options can be entered before or after the filename argument.

      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).

  2. Verify the generated VCs. The correctness of the VCs implies the correctness of the original specification. The VCS will be verified in HOL. To start the verification:

    1. Start HOL

    2. Add the location of x-MECH LITE theories to HOL search-path:
      val LITEDir = "where-x-MECH LITE-is/hollib" ;
      loadPath := !loadPath @ [LITEDir] ;

    3. Read the file x-MECH LITE.smx:
      use (LITEDir ^ "/litemech.smx")

    4. Read the file helloWorld.ls.hout.std generated by x-MECH LITE:
      read_mechout "helloWorld.ls.hout.std"

    5. Setup the goals:
      setup_goals from_mech

    6. Now the goals are ready, and you can proceed with verifying them using HOL. Look into the file xmechLib.sml in hollib to see what kind of x-MECH LITE-specific proof utilities available (currently only a few), such as a tactic to remove markers, or a tactic to remove x-MECH LITE quasi-constants.

Examples

Currently, we only have simple examples :)

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:

Simple examples:

Running the examples

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.ls
If you want to try the light-weight-verification reduction, try for example:
reduce --aoc bls.ls
On 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.lqs
The 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)