Basic Usage of Why3
Back to SPARK 2014 page for critical systems
- 11 November 2016: If you are using a machine in the linux lab with machine
name cs-linux-lab?? (where ?, ? are digits), then please run again the setup procedure
(you need to do it only once).
- These machines have a slightly newer version of why3.
- Alternatively you can replace the file callwhy3
in your directory ~/bin by this file: callwhy3
Make sure you make it executable
- 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.
- On machines with machine name cs-linux-lab?? (where ?, ? are digits)
you will get at the moment several error messages of the form
File "/usr/local/src/why3/why3TheoriesForSparkAda/_gnatprove_standard.mlw", line 135, characters 8-26: axiom round_single_bound does not contain any local abstract symbol
You can ignore these error messages.
- 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.
- On linux machines of the form cs-linux-lab?? (where ?, ? are digits) you need to
click on the tab "Task" on the right pane in order to see those conditions (again at the
- 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.