Basic Usage of SPARK Ada
Back to SPARK 2014 page for critical systems
- Please study the file
in Linux explaining the basic terminology of Linux
such as directory, ~/bin etc.
- Follow the instructions for setting up SPARK Ada and why3 for
usage from the file manager.
- We assume that you have successfully created an example in SPARK Ada
involving verification conditions and successfully executed the Prove
all command of SPARK Ada on it.
- Navigate using the filemanager to your project and then to the
subdirectory gnatprove (which was generated by SPARK Ada).
- That directory contains a file filename.mlw for each Ada file with
name filename.ads or filename.adb in your
project which has verification conditions.
- Note that you need to look at the file with the same name as your SPARKAda file (except for the extension).
- A left click on a file with extension .mlw will open why3 for that file.
- There are two main windows the left one containing lots of green ticks.
These are conditions which are trivially proved.
- At the bottom of it you find some items containing a brown question mark.
- If you left click on it you get a subdirectory for each of those items
"VC for ..."
- If you click on that you see in the top right corner some code which contains the generated verification conditions, where the most important part happens
at the very end.
- When you click on it you see some split items which are labelled by
e.g. "precondition", "postcondition" etc.
These are your conditions.
- You can run a theorem prover such as CVC3, CVC4 or Z3 (don't use Coq
unless you know Coq) by clicking on a button on the
- If you click on the verification condition the prover is run on all
- The why3 system is good for helping you understand what happens if SPARK Ada
couldn't prove your conditions.
Therefore, if SPARK Ada didn't prove a condition, look for the ones which
after pressing a prover, don't get a green tick.
- You can then look for any reasons why this was not proved.
- The goal is at the very end and the main parts of the formula
occur as axioms near the end.
- Now check why the goal doesn't follow from the axioms near the end,
and how this corresponds to your program.