Basic Usage of Why3

• Why3 will be installed later once it has been covered in the lectures. Please come back later.
• The following pages will be updated to the installation of why3 once it has been finalised.
• Please study the file Basic Terminology 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 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 right side
  • If you click on the verification condition the prover is run on all subconditions.
• 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.