Formal Verification: Lab exercises with SPARK

Updates

SPARK & Ada resources

In reading these resources, remember for this course you are expected to be able to read basic SPARK programs similar to those seen in lectures and exercises here and write SPARK verification constructs such as assertion pragmas, preconditions, postconditions and loop invariants.

Getting started

  1. Currently the GNAT Ada and SPARK tools are installed on student.compute and the DICE machines in the Forrest Hill 1.B19 lab. You will need to log in to one of these machines to use the tools.

    If ssh'ing to student.compute, include option -Y. This avoids some cut-and-paste problems with the GPS IDE.

  2. At a terminal shell, run

    module add GNAT
    module add SPARK

    to add directories containing the the tool executables to your current PATH.

  3. If you are using the default DICE GNOME-based window manager, the GPS IDE tool might have problems displaying certain pop-up windows. To avoid this, run at a terminal shell the command

    gsettings set org.gnome.settings-daemon.plugins.xsettings overrides "{'Gtk/DialogsUseHeader':<0>}"

    You only ever have to do this once: this setting is remembered permanently. If you need to undo it for some reason, run

    gsettings reset org.gnome.settings-daemon.plugins.xsettings overrides

    This is not a problem with the alternate KDE window manager.

Running GNATprove from the command line

GNATprove is the main tool for statically checking assertions in SPARK files. It translates SPARK source files to the Why3 intermediate language, runs the Why3 tool to generate verification conditions (VCs) and runs one or more SMT solvers to try to prove those VCs.

Type

gnatprove -Pproject.gpr -u sparkfile.adb

to run GNATprove with project file project.gpr on SPARK source file sparkfile.adb. The provided project files contain some useful default switches for GNATprove.

Switches of interest include

--prover=s[,s]*
Specifies which SMT solvers to use. By default cvc4 is used. Alternatives are altergo and z3. One or more solvers can be specified. Try specifying all if cvc4 can't prove all VCs.
--timeout=n
Timeout in seconds for an attempt of an SMT solver to prove a VC. The default is 1. Try 5 or 10 if all VCs are not proved with the default.
-h
Help. See the full range of options.
-f
Force proof of all VCs, even those previously proved. GNATprove remembers VCs proved in previous runs and will not try proving VCs again if they are the same. This switch is included in the provided project files.
--report=level
Amount of information presented about VC proofs. See help for alternatives. Argumentlevel is set to statistics, the most verbose level, in the provided project files. previously proved. GNATprove remembers VCs proved in previous runs and will not try proving VCs again if they are the same.
--proof=g
Set the mode for generation of VCs. By default one VC is generated per check. Sometimes though, the SMT solvers are more easily able to prove VCs when they are split into components. If you set g to progressive, GNATprove first tries using provers on the unsplit VC and, if that fails, tries the provers on each split component, one by one.
Sometimes you might want to run

gnatprove -Pproject.gpr --clean

to completely clean out the intermediate files created by GNATprove. For example, GNATprove remembers which prover successfully last proved each VC and will use that prover again rather than trying in turn provers listed using the --prover switch.

Using the GPS IDE to run GNATprove

Type

gps -Pproject.gpr

to start up GPS using project file project.gpr.

To make available the full range of options when running with GNATprove, switch to the advanced user profile in menu Edit ⟩ Preferences ⟩ SPARK, by changing the value of User profile from Basic to Advanced.

To have GNATprove both do flow analysis and try proving assertions, select the file and use menu SPARK ⟩ Prove File.

Compiling and running programs

At the command line, type

gnatmake -Pproject.gpr sparkfile.adb

to run the GNAT compiler, binder and linker with project file project.gpr on main file sparkfile.adb. As with other project building utilities, GNATmake figures out which files sparkfile.adb depends on, and, as needed, it will compile those too and include them in the binding and linking process.

The provided project files are configured to write an executable file to the current directory with the name of the provided sparkfile.adb without the extension. To run the executable, type

./sparkfile

Occasionally, GNATmake does not realise it has work to do (e.g. if you rebuild with different switch options). In such cases, you can run

gnatclean -Pproject.gpr sparkfile.adb

to delete all the intermediate files and the executable file, forcing GNATmake to start from scratch next time you run it.

Exercises

Lab 1

Download this file lab1.tar to some directory in your DICE file-space and unpack it using the command

tar xf lab1.tar

This will create a directory lab1 containing the following files you need to complete and experiment with. The project file is proj.gpr, so use switch -Pproj.gpr when running GPS or GNATprove.

  1. swap.adb: Complete and check a suitable post-condition.
  2. search_arr_zero.adb: Complete the loop invariant. Check it is correct.
  3. map_arr_incr.adb: Complete the loop invariant. Check it is correct. Hint: you need the loop invariant to express not only which array elements have been incremented but also which are still the same as they were when the loop was entered.
  4. search_arr_max.adb: Complete the loop invariant. Check it is correct.
Also provided for reference is the file validate_arr_zero.adb. This is one of the examples from the SPARK verification features lecture.

Lab 2

The files for this lab are in lab2.tar. Again the project file is name proj.gpr.
  1. binary_search.adb: complete both the loop variant and the loop invariant. Use GNATprove to check they are correct.

    Compile and run the tests provided in test_search.adb. The proj.gpr file includes a compiler switch -gnata which enables assertion checking. Try adding a bug to one or more of the assertions in binary_search.ads or binary_search.adb and see if one of the tests picks up the bug. Also see if a bug in the input data (e.g. not sorted) or in the code causes an assertion failure.

    Generally, testing is a helpful step when debugging assertions.

  2. max.adb: complete both the loop invariant and loop variant, using GNATprove to check they are correct.

Solutions

Solutions are in files lab1-soln.tar and lab2-soln.tar.

Point to note include:

  1. In Lab 1 map_arr_incr.adb concerning incrementing the elements of an array, the invariant needs to specify both the segment of the array that is unchanged and the segment that is unchanged.
  2. In Lab 2 max.adb concerning finding the maximum element of an array by less conventional means, there are at least a couple of ways to approach phrasing the invariant.
    1. Specify how one of the array indexes is a maximum of the elements of the array between the array start and the first index and between the second index and the array end. This is the approach taken in the provided solution.
    2. Specify that the maximum of the array is contained in the array segment between the two indexes.

Last modified: 14:00 Thu 6 Apr 2017


Home : Teaching : Courses : Fv 

Informatics Forum, 10 Crichton Street, Edinburgh, EH8 9AB, Scotland, UK
Tel: +44 131 651 5661, Fax: +44 131 651 1426, E-mail: school-office@inf.ed.ac.uk
Please contact our webadmin with any comments or corrections. Logging and Cookies
Unless explicitly stated otherwise, all material is copyright © The University of Edinburgh