The first step in using Why3 is to write a suitable input file. When one wants to learn a programming language, one starts by writing a basic program. Here is our first Why3 file, which is the file examples/logic/hello_proof.why of the distribution. It contains a small set of goals.
|theory HelloProof "My very first Why3 theory" goal G1 : true goal G2 : (true -> false) /\ (true \/ false) use import int.Int goal G3: forall x:int. x*x >= 0 end|
Any declaration must occur inside a theory, which is in that example called HelloProof and labeled with a comment inside double quotes. It contains three goals named G1,G2,G3. The first two are basic propositional goals, whereas the third involves some integer arithmetic, and thus it requires to import the theory of integer arithmetic from the Why3 standard library, which is done by the use declaration above.
We don’t give more details here about the syntax and refer to Chapter 2 for detailed explanations. In the following, we show how this file is handled in the Why3 GUI (Section 1.2) then in batch mode using the why3 executable (Section 1.3).
The graphical interface allows to browse into a file or a set of files, and check the validity of goals with external provers, in a friendly way. This section presents the basic use of this GUI. Please refer to Section 6.3 for a more complete description.
The GUI is launched on the file above as follows.
why3 ide hello_proof.why
When the GUI is started for the first time, you should get a window that looks like the screenshot of Figure 1.1.
The left column is a tool bar which provides different actions to apply on goals. The section “Provers” displays the provers that were detected as installed on your computer. (If not done yet, you must perform prover autodetection using why3 config --detect-provers.) Three provers were detected, in this case, these are Alt-Ergo , Coq  and Simplify .
The middle part is a tree view that allows to browse inside the theories. In this tree view, we have a structured view of the file: this file contains one theory, itself containing three goals.
In Figure 1.2, we clicked on the row corresponding to goal G1. The task associated with this goal is then displayed on the top right, and the corresponding part of the input file is shown on the bottom right part.
You are now ready to call these provers on the goals. Whenever you click on a prover button, this prover is called on the goal selected in the tree view. You can select several goals at a time, either by using multi-selection (typically by clicking while pressing the Shift or Ctrl key) or by selecting the parent theory or the parent file. Let us now select the theory “HelloProof” and click on the Simplify button. After a short time, you should get the display of Figure 1.3.
Goal G1 is now marked with a green “checked” icon in the status column. This means that the goal is proved by the Simplify prover. On the contrary, the two other goals are not proved, they remain marked with an orange question mark.
You can immediately attempt to prove the remaining goals using another prover, e.g. Alt-Ergo, by clicking on the corresponding button. Goal G3 should be proved now, but not G2.
Instead of calling a prover on a goal, you can apply a transformation to it. Since G2 is a conjunction, a possibility is to split it into subgoals. You can do that by clicking on the Split button of section “Transformations” of the left toolbar. Now you have two subgoals, and you can try again a prover on them, for example Simplify. We already have a lot of goals and proof attempts, so it is a good idea to close the sub-trees which are already proved: this can be done by the menu View/Collapse proved goals, or even better by its shortcut “Ctrl-C”. You should see now what is displayed on Figure 1.4.
The first part of goal G2 is still unproved. As a last resort, we can try to call the Coq proof assistant. The first step is to click on the Coq button. A new sub-row appear for Coq, and unsurprisingly the goal is not proved by Coq either. What can be done now is editing the proof: select that row and then click on the Edit button in section “Tools” of the toolbar. This should launch the Coq proof editor, which is coqide by default (see Section 6.3 for details on how to configure this). You get now a regular Coq file to fill in, as shown on Figure 1.5. Please be mindful of the comments of this file. They indicate where Why3 expects you to fill the blanks. Note that the comments themselves should not be removed, as they are needed to properly regenerate the file when the goal is changed. See Section 9.3 for more details.
Of course, in that particular case, the goal cannot be proved since it is not valid. The only thing to do is to fix the input file, as explained below.
Currently, the GUI does not allow to modify the input file. You must edit the file external by some editor of your choice. Let us assume we change the goal G2 by replacing the first occurrence of true by false, e.g.
|goal G2 : (false -> false) /\ (true \/ false)|
We can reload the modified file in the IDE using menu File/Reload, or the shortcut “Ctrl-R”. We get the tree view shown on Figure 1.6.
The important feature to notice first is that all the previous proof attempts and transformations were saved in a database — an XML file created when the Why3 file was opened in the GUI for the first time. Then, for all the goals that remain unchanged, the previous proofs are shown again. For the parts that changed, the previous proofs attempts are shown but marked with “(obsolete)” so that you know the results are not accurate. You can now retry to prove all what remains unproved using any of the provers.
Instead of pushing a prover’s button to rerun its proofs, you can replay the existing but obsolete proof attempts, by clicking on the Replay button. By default, Replay only replays proofs that were successful before. If you want to replay all of them, you must select the context all goals at the top of the left tool bar.
Notice that replaying can be done in batch mode, using the
replay command (see Section 6.5) For
example, running the replayer on the hello_proof example is
as follows (assuming G2 still is
(true -> false) /\ (true \/ false)).
$ why3 replay hello_proof Info: found directory 'hello_proof' for the project Opening session...[Xml warning] prolog ignored [Reload] file '../hello_proof.why' [Reload] theory 'HelloProof' [Reload] transformation split_goal for goal G2 done Progress: 9/9 2/3 +--file ../hello_proof.why: 2/3 +--theory HelloProof: 2/3 +--goal G2 not proved Everything OK.
The last line tells us that no differences were detected between the current run and the run stored in the XML file. The tree above reminds us that G2 is not proved.
You may want to clean some the proof attempts, e.g. removing the unsuccessful ones when a project is finally fully proved.
A proof or a transformation can be removed by selecting it and clicking on button Remove. You must confirm the removal. Beware that there is no way to undo such a removal.
The Clean button performs an automatic removal of all proofs attempts that are unsuccessful, while there exists a successful proof attempt for the same goal.
The prove command makes it possible to check the validity of goals with external provers, in batch mode. This section presents the basic use of this tool. Refer to Section 6.2 for a more complete description of this tool and all its command-line options.
The very first time you want to use Why3, you should proceed with autodetection of external provers. We have already seen how to do it in the Why3 GUI. On the command line, this is done as follows (here “>” is the prompt):
> why3 config --detect
This prints some information messages on what detections are attempted. To know which provers have been successfully detected, you can do as follows.
> why3 --list-provers Known provers: alt-ergo (Alt-Ergo) coq (Coq) simplify (Simplify)
The first word of each line is a unique identifier for the associated prover. We thus have now the three provers Alt-Ergo , Coq  and Simplify .
Let us assume that we want to run Simplify on the HelloProof
example. The command to type and its output are as follows, where the
-P option is followed by the unique prover identifier (as shown
> why3 prove -P simplify hello_proof.why hello_proof.why HelloProof G1 : Valid (0.10s) hello_proof.why HelloProof G2 : Unknown: Unknown (0.01s) hello_proof.why HelloProof G3 : Unknown: Unknown (0.00s)
Unlike the Why3 GUI, the command-line tool does not save the proof attempts or applied transformations in a database.
We can also specify which goal or goals to prove. This is done by giving first a theory identifier, then goal identifier(s). Here is the way to call Alt-Ergo on goals G2 and G3.
> why3 prove -P alt-ergo hello_proof.why -T HelloProof -G G2 -G G3 hello_proof.why HelloProof G2 : Unknown: Unknown (0.01s) hello_proof.why HelloProof G3 : Valid (0.01s)
Finally, a transformation to apply to goals before proving them can be specified. To know the unique identifier associated to a transformation, do as follows.
> why3 --list-transforms Known non-splitting transformations: [...] Known splitting transformations: [...] split_goal split_intro
Here is how you can split the goal G2 before calling Simplify on the resulting subgoals.
> why3 prove -P simplify hello_proof.why -a split_goal -T HelloProof -G G2 hello_proof.why HelloProof G2 : Unknown: Unknown (0.00s) hello_proof.why HelloProof G2 : Valid (0.00s)
Section 10.5 gives the description of the various transformations available.