Formal Verification: Lab exercises with SPARK

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.

SPARK 2014 Home page. SPARK 2014 is the version of SPARK used on this course. The resources section of this site has a number of articles on the use of SPARK.
Articles on SPARK in the AdaCore blog.
AdaCore University. This site includes online courses on Ada and SPARK. Of particular relevance are the first 3 lessons of the SPARK 2014 Course. Lessons include videos you can watch and slides you can download.
Further introductory resources on Ada
- Ada - A Crash Course by Peter Chapin.
- Quick Ada by Dale Stanbrough. This dates from 2000 and is for Ada 95. While SPARK 2014 is based on Ada 2012, the basics we use are pretty much the same as they were with Ada 95.
- Ada for the C++ or Java Developer by Quentin Ochem.
AdaCore documentation. Documentation here includes the SPARK Toolset User's Guide which describes the extra features SPARK has that Ada doesn't, how to run the GNATprove prover, and gives guidelines on writing and using SPARK.
AdaCore GNAT Community home page for academic and open source users of GNAT and SPARK tools. Visit here to download free GPL-licensed versions of the tools.

Getting started

Currently the GNAT Ada and SPARK tools are installed on student.compute. You will need to log in to this machine to use the tools.
When ssh'ing to student.compute, include option -Y. This avoids some cut-and-paste problems with the GPS IDE.
At a terminal shell, run
module add GNAT module add SPARK
to add directories containing the the tool executables to your current PATH.
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 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.

swap.adb: Complete and check a suitable post-condition.
search_arr_zero.adb: Complete the loop invariant. Check it is correct.
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.
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.

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.
max.adb: complete both the loop invariant and loop variant, using GNATprove to check they are correct.

Solutions

Solutions will be posted here after students have had a chance to work through labs.

Last modified: 14:00 Fri 16 Feb 2018

Home : Teaching : Courses : Fv