FV: Practical Exercise 3: Software verification with SPARK

This practical exercise gets you to write some postconditions and loop invariants for simple SPARK programs and then run the SPARK prover GNATprove to formally verify that you have got these assertions correct.

Installing GNATprove

You can download compressed tar archives (.tar.gz files) that contain GNATprove compiled for Linux, macOS (x86_64) and Windows from this site.  The following instructions tell you how to install GNATprove in your DICE Linux file space. 

  1. Download the file gnatprove-x86_64-linux-12.1.0-1.tar.gz to your DICE home directory, here assumed to be /home/s1234567.

  2. Unpack the compressed archive file with

    tar xzf gnatprove-x86_64-linux-12.1.0-1.tar.gz

    This unpacks the archive into directory gnatprove-x86_64-linux-12.1.0-1.

    The unpacked archive takes up just under 1GB of file space. On DICE, you can check how much space you have available using the AFS command

    fs listquota -human

    Guidance is available to help you free up space in your DICE account if you do not have enough.

  3. In order to conveniently use gnatprove, add the directory containing the GNATprove binary to your PATH environment variable.  Use the command

    export PATH=/home/s1234567/gnatprove-x86_64-linux-12.1.0-1/bin:$PATH

    with /home/s1234567/ replaced with where-ever you unpack the .tar.gz archive.

    You can put this command in a startup file such as .bashrc or .benv on DICE, or you can put it in its own file and just source that file when you want to make the SPARK tools available to run.

If you have your own Linux machine or an x86-based Mac, the installation instructions should be similar. On recent versions of macOS, you might get an error message saying that gnatprove cannot be opened because the developer cannot be verified. In this case, running the command

xattr -d com.apple.quarantine bin/gnatprove

from the gnatprove-x86_64-linux-12.1.0-1 directory should enable you to run GNATprove. It is not known if the x86 binary can run on Macs with Apple silicon. If you have success here, please add a post on Piazza.

Checking SPARK assertions with GNATprove

GNATprove 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: for example, one can write --prover=cvc4,altergo.  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. Argument level is set to statistics, the most verbose level, in the provided project files.
  • --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.

SPARK Exercises

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

unzip lab1.zip

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

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

  • AdaCore's interactive learning platform.   This is a good place to start.  Of particular relevance is the Introduction to SPARK course. You might also wish to skim the courses Introduction to Ada and Ada for the C++ or Java Developer.
  • 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.
  • AdaCore's SPARK page.  This provides a non-technical introduction to SPARK and, at its foot, links to reference resources on SPARK.  Of particular relevance is the SPARK 2014 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.
  • Articles on SPARK in the AdaCore blog, discussing the adoption of SPARK at NVIDIA, for example.
License
All rights reserved The University of Edinburgh