The Why3 platform
Version 1.2.1, October 2019
François Bobot1,2 |
Jean-Christophe Filliâtre1,2 |
Claude Marché2,1 |
Guillaume Melquiond2,1 |
Andrei Paskevich1,2 |
1 LRI, CNRS & University Paris-Sud, Orsay, F-91405 |
2 Inria Saclay – Île-de-France, Palaiseau, F-91120 |
©2010–2018 University Paris-Sud, CNRS, Inria
This work has been partly supported by the ‘U3CAT’ national ANR project (ANR-08-SEGI-021-08), the ‘Hi-Lite’ FUI project of the System@tic competitivity cluster, the ‘BWare’ ANR project (ANR-12-INSE-0010), the Joint Laboratory ProofInUse (ANR-13-LAB3-0007); the ‘CoLiS’ ANR project (ANR-15-CE25-0001), and the ‘VOCaL’ ANR project (ANR-15-CE25-008).
Why3 is a platform for deductive program verification. It provides a rich language for specification and programming, called WhyML, and relies on external theorem provers, both automated and interactive, to discharge verification conditions. Why3 comes with a standard library of logical theories (integer and real arithmetic, Boolean operations, sets and maps, etc.) and basic programming data structures (arrays, queues, hash tables, etc.). A user can write WhyML programs directly and get correct-by-construction OCaml programs through an automated extraction mechanism. WhyML is also used as an intermediate language for the verification of C, Java, or Ada programs.
Why3 is a complete reimplementation of the former Why platform [6]. Among the new features are: numerous extensions to the input language, a new architecture for calling external provers, and a well-designed API, allowing to use Why3 as a software library. An important emphasis is put on modularity and genericity, giving the end user a possibility to easily reuse Why3 formalizations or to add support for a new external prover if wanted.
Why3 project page is http://why3.lri.fr/. The last distribution is available there, in source format, together with this documentation and several examples.
Why3 is also distributed under the form of an OPAM package and a Debian package.
Why3 is distributed as open source and freely available under the terms of the GNU LGPL 2.1. See the file LICENSE.
See the file INSTALL for quick installation instructions, and Section 4 of this document for more detailed instructions.
There is a public mailing list for users’ discussions: http://lists.gforge.inria.fr/mailman/listinfo/why3-club.
Report any bug to the Why3 Bug Tracking System: https://gitlab.inria.fr/why3/why3/issues.
We gratefully thank the people who contributed to Why3, directly or indirectly: Stefan Berghofer, Sylvie Boldo, Martin Clochard, Simon Cruanes, Sylvain Dailler, Clément Fumex, Léon Gondelman, David Hauzar, Daisuke Ishii, Johannes Kanig, Mikhail Mandrykin, David Mentré, Benjamin Monate, Kim Nguyen, Thi-Minh-Tuyen Nguyen, Mário Pereira, Raphaël Rieu-Helft, Simāo Melo de Sousa, Asma Tafat, Piotr Trojanek, Makarius Wenzel.
Part I |
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 goal G1: true goal G2: (true -> false) /\ (true \/ false) use 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. 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 5.3 for a more complete description.
The GUI is launched on the file above as follows (here “>” is the prompt):
> 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 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 pane. The corresponding part of the input file is shown when clicking the rightmost tab of that pane.
You are now ready to call provers on the goals (If not done yet, you must perform prover autodetection using why3 config --detect-provers.) A prover is selected using the context menu (right-click). This prover is then 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 run the Alt-Ergo prover. After a short time, you should get the display of Figure 1.3.
Goals G1 and G3 are now marked with a green “checked” icon in the status column. This means that these goals have been proved by Alt-Ergo. On the contrary, goal G2 is not proved; it remains marked with a question mark. You could attempt to prove G2 using another prover, though it is obvious here it will not succeed.
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 selecting Split VC in the context menu. Now you have two subgoals, and you can try again a prover on them, for example Alt-Ergo. 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, by selecting it in the context menu. A new sub-row appear for Coq, and the Coq proof editor is launched. (It is coqide by default; see Section 5.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 8.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.
You can edit the source file, using the corresponding tab in the top-right window of the GUI. 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 refresh the goals using menu File/Save all and Refresh session, 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, using menu Tools/Replay obsolete. By default, Replay only replays proofs that were successful before.
Notice that replaying can be done in batch mode, using the
replay command (see Section 5.4) 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 2/3 (replay OK) +--file ../hello_proof.why: 2/3 +--theory HelloProof: 2/3 +--goal G2 not proved
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 of 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 using menu Tools/Remove or the Delete key. Menu Tools/Clean or shortcut “C” perform an automatic removal of all proofs attempts that are unsuccessful, while there exists a successful proof attempt for the same goal. Beware that there is no way to undo such a removal.
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 5.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. On the command line, this is done as follows:
> 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 1.30 CVC4 1.5 Coq 8.6
The first word of each line is a unique identifier for the associated prover. We thus have now the three provers Alt-Ergo [4], CVC4 [1], and Coq [2].
Let us assume that we want to run Alt-Ergo 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
by --list-provers
option).
> why3 prove -P Alt-Ergo hello_proof.why hello_proof.why HelloProof G1: Valid (0.00s, 1 steps) hello_proof.why HelloProof G2: Unknown (other) (0.01s) hello_proof.why HelloProof G3: Valid (0.00s, 1 steps)
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_right
Here is how you can split the goal G2 before calling Simplify on the resulting subgoals.
> why3 prove -P Alt-Ergo hello_proof.why -a split_goal_right -T HelloProof -G G2 hello_proof.why HelloProof G2: Unknown (other) (0.01s) hello_proof.why HelloProof G2: Valid (0.00s, 1 steps)
Section 9.5 gives the description of the various transformations available.
This chapter describes the WhyML specification and programming language. A WhyML source file has suffix .mlw. It contains a list of modules. Each module contains a list of declarations. These includes
Command-line tools described in the previous chapter also apply to files containing programs. For instance
> why3 prove myfile.mlw
displays the verification conditions for programs contained in file myfile.mlw, and
> why3 prove -P alt-ergo myfile.mlw
runs the SMT solver Alt-Ergo on these verification conditions. All this can be performed within the GUI tool why3 ide as well. See Chapter 5 for more details regarding command lines.
As an introduction to WhyML, we use a small logical puzzle
(Section 2.1) and then the five problems from the VSTTE
2010 verification competition [11].
The source code for all these examples is contained in Why3’s
distribution, in sub-directory examples/. Look for files
logic/einstein.why and vstte10_xxx.mlw.
Let us use Why3 to solve a little puzzle known as “Einstein’s logic problem”. (This Why3 example was contributed by Stéphane Lescuyer.) The problem is stated as follows. Five persons, of five different nationalities, live in five houses in a row, all painted with different colors. These five persons own different pets, drink different beverages, and smoke different brands of cigars. We are given the following information:
The question is: what is the nationality of the fish’s owner?
We start by introducing a general-purpose theory defining the notion of bijection, as two abstract types together with two functions from one to the other and two axioms stating that these functions are inverse of each other.
theory Bijection type t type u function of t : u function to_ u : t axiom To_of : forall x : t. to_ (of x) = x axiom Of_to : forall y : u. of (to_ y) = y end |
We now start a new theory, Einstein, which will contain all the individuals of the problem.
theory Einstein |
First, we introduce enumeration types for houses, colors, persons, drinks, cigars, and pets.
type house = H1 | H2 | H3 | H4 | H5 type color = Blue | Green | Red | White | Yellow type person = Dane | Englishman | German | Norwegian | Swede type drink = Beer | Coffee | Milk | Tea | Water type cigar = Blend | BlueMaster | Dunhill | PallMall | Prince type pet = Birds | Cats | Dogs | Fish | Horse |
We now express that each house is associated bijectively to a color, by cloning the Bijection theory appropriately.
clone Bijection as Color with type t = house, type u = color |
Cloning a theory makes a copy of all its declarations, possibly in combination with a user-provided substitution. Here we substitute type house for type t and type color for type u. As a result, we get two new functions, namely Color.of and Color.to_, from houses to colors and colors to houses, respectively, and two new axioms relating them. Similarly, we express that each house is associated bijectively to a person
clone Bijection as Owner with type t = house, type u = person |
and that drinks, cigars, and pets are all associated bijectively to persons:
clone Bijection as Drink with type t = person, type u = drink clone Bijection as Cigar with type t = person, type u = cigar clone Bijection as Pet with type t = person, type u = pet |
Next, we need a way to state that a person lives next to another. We first define a predicate leftof over two houses.
predicate leftof (h1 h2 : house) = match h1, h2 with | H1, H2 | H2, H3 | H3, H4 | H4, H5 -> true | _ -> false end |
Note how we advantageously used pattern matching, with an or-pattern for the four positive cases and a universal pattern for the remaining 21 cases. It is then immediate to define a neighbour predicate over two houses, which completes theory Einstein.
predicate rightof (h1 h2 : house) = leftof h2 h1 predicate neighbour (h1 h2 : house) = leftof h1 h2 \/ rightof h1 h2 end |
The next theory contains the 15 hypotheses. It starts by importing theory Einstein.
theory EinsteinHints use import Einstein |
Then each hypothesis is stated in terms of to_ and of functions. For instance, the hypothesis “The Englishman lives in a red house” is declared as the following axiom.
axiom Hint1: Color.of (Owner.to_ Englishman) = Red |
And so on for all other hypotheses, up to “The man who smokes Blends has a neighbour who drinks water”, which completes this theory.
... axiom Hint15: neighbour (Owner.to_ (Cigar.to_ Blend)) (Owner.to_ (Drink.to_ Water)) end |
Finally, we declare the goal in a fourth theory:
theory Problem use import Einstein use import EinsteinHints goal G: Pet.to_ Fish = German end |
and we can use Why3 to discharge this goal with any prover of our choice.
> why3 prove -P alt-ergo einstein.why einstein.why Goals G: Valid (1.27s, 989 steps)
The source code for this puzzle is available in the source
distribution of Why3, in file examples/logic/einstein.why
.
Let us now move to the problems of the VSTTE 2010 verification competition [11]. The first problem is stated as follows:
Given an N-element array of natural numbers, write a program to compute the sum and the maximum of the elements in the array.
We assume N ≥ 0 and a[i] ≥ 0 for 0 ≤ i < N, as precondition, and we have to prove the following postcondition:
sum ≤ N × max. |
In a file max_sum.mlw
, we start a new module:
module MaxAndSum |
We are obviously needing arithmetic, so we import the corresponding theory, exactly as we would do within a theory definition:
use import int.Int |
We are also going to use references and arrays from Why3 standard library, so we import the corresponding modules:
use import ref.Ref use import array.Array |
Modules Ref and Array respectively provide a type ref ’a for references and a type array ’a for arrays, together with useful operations and traditional syntax. They are loaded from the WhyML files ref.mlw and array.mlw in the standard library.
We are now in position to define a program function
max_sum
. A function definition is introduced with the keyword
let. In our case, it introduces a function with two arguments,
an array a and its size n:
let max_sum (a: array int) (n: int) : (int, int) = ... |
(There is a function length to get the size of an array but we add this extra parameter n to stay close to the original problem statement.) The function body is a Hoare triple, that is a precondition, a program expression, and a postcondition.
let max_sum (a: array int) (n: int) : (int, int) requires { n = length a } requires { forall i. 0 <= i < n -> a[i] >= 0 } ensures { let (sum, max) = result in sum <= n * max } = ... expression ... |
The first precondition expresses that n is equal to the length of a (this will be needed for verification conditions related to array bound checking). The second precondition expresses that all elements of a are non-negative. The postcondition decomposes the value returned by the function as a pair of integers (sum, max) and states the required property.
returns { sum, max -> sum <= n * max } |
We are now left with the function body itself, that is a code computing the sum and the maximum of all elements in a. With no surprise, it is as simple as introducing two local references
let sum = ref 0 in let max = ref 0 in |
scanning the array with a for loop, updating max and sum
for i = 0 to n - 1 do if !max < a[i] then max := a[i]; sum := !sum + a[i] done; |
and finally returning the pair of the values contained in sum and max:
!sum, !max |
This completes the code for function max_sum.
As such, it cannot be proved correct, since the loop is still lacking
a loop invariant. In this case, the loop invariant is as simple as
!sum <= i * !max
, since the postcondition only requires us to prove
sum <= n * max
. The loop invariant is introduced with the
keyword invariant, immediately after the keyword do:
for i = 0 to n - 1 do invariant { !sum <= i * !max } ... done |
There is no need to introduce a variant, as the termination of a for loop is automatically guaranteed. This completes module MaxAndSum. The whole code is shown below.
module MaxAndSum use import int.Int use import ref.Ref use import array.Array let max_sum (a: array int) (n: int) : (int, int) requires { n = length a } requires { forall i. 0 <= i < n -> a[i] >= 0 } returns { sum, max -> sum <= n * max } = let sum = ref 0 in let max = ref 0 in for i = 0 to n - 1 do invariant { !sum <= i * !max } if !max < a[i] then max := a[i]; sum := !sum + a[i] done; !sum, !max end |
We can now proceed to its verification.
Running why3, or better why3 ide, on file
max_sum.mlw
shows a single verification condition with name
WP max_sum
.
Discharging this verification condition requires a little bit of non-linear
arithmetic. Thus some SMT solvers may fail at proving it, but other
succeed, e.g., CVC4.
The second problem is stated as follows:
Invert an injective array A on N elements in the subrange from 0 to N − 1, i.e. the output array B must be such that B[A[i]] = i for 0 ≤ i < N.
The code is immediate, since it is as simple as
for i = 0 to n - 1 do b[a[i]] <- i done |
so it is more a matter of specification and of getting the proof done with as much automation as possible. In a new file, we start a new module and we import arithmetic and arrays:
module InvertingAnInjection use import int.Int use import array.Array |
It is convenient to introduce predicate definitions for the properties of being injective and surjective. These are purely logical declarations:
predicate injective (a: array int) (n: int) = forall i j. 0 <= i < n -> 0 <= j < n -> i <> j -> a[i] <> a[j] predicate surjective (a: array int) (n: int) = forall i. 0 <= i < n -> exists j: int. (0 <= j < n /\ a[j] = i) |
It is also convenient to introduce the predicate “being in the subrange from 0 to n−1”:
predicate range (a: array int) (n: int) = forall i. 0 <= i < n -> 0 <= a[i] < n |
Using these predicates, we can formulate the assumption that any injective array of size n within the range 0..n−1 is also surjective:
lemma injective_surjective: forall a: array int, n: int. injective a n -> range a n -> surjective a n |
We declare it as a lemma rather than as an axiom, since it is actually provable. It requires induction and can be proved using the Coq proof assistant for instance. Finally we can give the code a specification, with a loop invariant which simply expresses the values assigned to array b so far:
let inverting (a: array int) (b: array int) (n: int) requires { n = length a = length b } requires { injective a n /\ range a n } ensures { injective b n } = for i = 0 to n - 1 do invariant { forall j. 0 <= j < i -> b[a[j]] = j } b[a[i]] <- i done |
Here we chose to have array b as argument; returning a freshly allocated array would be equally simple. The whole module is given below. The verification conditions for function inverting are easily discharged automatically, thanks to the lemma.
module InvertingAnInjection use import int.Int use import array.Array predicate injective (a: array int) (n: int) = forall i j. 0 <= i < n -> 0 <= j < n -> i <> j -> a[i] <> a[j] predicate surjective (a: array int) (n: int) = forall i. 0 <= i < n -> exists j: int. (0 <= j < n /\ a[j] = i) predicate range (a: array int) (n: int) = forall i. 0 <= i < n -> 0 <= a[i] < n lemma injective_surjective: forall a: array int, n: int. injective a n -> range a n -> surjective a n let inverting (a: array int) (b: array int) (n: int) requires { n = length a = length b } requires { injective a n /\ range a n } ensures { injective b n } = for i = 0 to n - 1 do invariant { forall j. 0 <= j < i -> b[a[j]] = j } b[a[i]] <- i done end |
The third problem is stated as follows:
Given a linked list representation of a list of integers, find the index of the first element that is equal to 0.
More precisely, the specification says
You have to show that the program returns an index i equal to the length of the list if there is no such element. Otherwise, the i-th element of the list must be equal to 0, and all the preceding elements must be non-zero.
Since the list is not mutated, we can use the algebraic data type of polymorphic lists from Why3’s standard library, defined in theory list.List. It comes with other handy theories: list.Length, which provides a function length, and list.Nth, which provides a function nth for the n-th element of a list. The latter returns an option type, depending on whether the index is meaningful or not.
module SearchingALinkedList use import int.Int use import option.Option use export list.List use export list.Length use export list.Nth |
It is helpful to introduce two predicates: a first one for a successful search,
predicate zero_at (l: list int) (i: int) = nth i l = Some 0 /\ forall j. 0 <= j < i -> nth j l <> Some 0 |
and a second one for a non-successful search,
predicate no_zero (l: list int) = forall j. 0 <= j < length l -> nth j l <> Some 0 |
We are now in position to give the code for the search function. We write it as a recursive function search that scans a list for the first zero value:
let rec search (i: int) (l: list int) : int = match l with | Nil -> i | Cons x r -> if x = 0 then i else search (i+1) r end |
Passing an index i as first argument allows to perform a tail call. A simpler code (yet less efficient) would return 0 in the first branch and 1 + search ... in the second one, avoiding the extra argument i.
We first prove the termination of this recursive function. It amounts to give it a variant, that is a value that strictly decreases at each recursive call with respect to some well-founded ordering. Here it is as simple as the list l itself:
let rec search (i: int) (l: list int) : int variant { l } = ... |
It is worth pointing out that variants are not limited to values of algebraic types. A non-negative integer term (for example, length l) can be used, or a term of any other type equipped with a well-founded order relation. Several terms can be given, separated with commas, for lexicographic ordering.
There is no precondition for function search. The postcondition expresses that either a zero value is found, and consequently the value returned is bounded accordingly,
i <= result < i + length l /\ zero_at l (result - i) |
or no zero value was found, and thus the returned value is exactly i plus the length of l:
result = i + length l /\ no_zero l |
Solving the problem is simply a matter of calling search with 0 as first argument. The code is given below. The verification conditions are all discharged automatically.
module SearchingALinkedList use import int.Int use export list.List use export list.Length use export list.Nth predicate zero_at (l: list int) (i: int) = nth i l = Some 0 /\ forall j. 0 <= j < i -> nth j l <> Some 0 predicate no_zero (l: list int) = forall j. 0 <= j < length l -> nth j l <> Some 0 let rec search (i: int) (l: list int) : int variant { l } ensures { (i <= result < i + length l /\ zero_at l (result - i)) \/ (result = i + length l /\ no_zero l) } = match l with | Nil -> i | Cons x r -> if x = 0 then i else search (i+1) r end let search_list (l: list int) : int ensures { (0 <= result < length l /\ zero_at l result) \/ (result = length l /\ no_zero l) } = search 0 l end |
Alternatively, we can implement the search with a while loop. To do this, we need to import references from the standard library, together with theory list.HdTl which defines functions hd and tl over lists.
use import ref.Ref use import list.HdTl |
Being partial functions, hd and tl return options. For the purpose of our code, though, it is simpler to have functions which do not return options, but have preconditions instead. Such a function head is defined as follows:
let head (l: list 'a) : 'a requires { l <> Nil } ensures { hd l = Some result } = match l with Nil -> absurd | Cons h _ -> h end |
The program construct absurd denotes an unreachable piece of code. It generates the verification condition false, which is here provable using the precondition (the list cannot be Nil). Function tail is defined similarly:
let tail (l: list 'a) : list 'a requires { l <> Nil } ensures { tl l = Some result } = match l with Nil -> absurd | Cons _ t -> t end |
Using head and tail, it is straightforward to implement the search as a while loop. It uses a local reference i to store the index and another local reference s to store the list being scanned. As long as s is not empty and its head is not zero, it increments i and advances in s using function tail.
let search_loop (l: list int) : int = ensures { ... same postcondition as in search_list ... } = let i = ref 0 in let s = ref l in while !s <> Nil && head !s <> 0 do invariant { ... } variant { !s } i := !i + 1; s := tail !s done; !i |
The postcondition is exactly the same as for function search_list
.
The termination of the while loop is ensured using a variant,
exactly as for a recursive function. Such a variant must strictly decrease at
each execution of the loop body. The reader is invited to figure out
the loop invariant.
The fourth problem is probably the most challenging one. We have to verify the implementation of a program which solves the N-queens puzzle: place N queens on an N × N chess board so that no queen can capture another one with a legal move. The program should return a placement if there is a solution and indicates that there is no solution otherwise. A placement is a N-element array which assigns the queen on row i to its column. Thus we start our module by importing arithmetic and arrays:
module NQueens use import int.Int use import array.Array |
The code is a simple backtracking algorithm, which tries to put a queen on each row of the chess board, one by one (there is basically no better way to solve the N-queens puzzle). A building block is a function which checks whether the queen on a given row may attack another queen on a previous row. To verify this function, we first define a more elementary predicate, which expresses that queens on row pos and q do no attack each other:
predicate consistent_row (board: array int) (pos: int) (q: int) = board[q] <> board[pos] /\ board[q] - board[pos] <> pos - q /\ board[pos] - board[q] <> pos - q |
Then it is possible to define the consistency of row pos with respect to all previous rows:
predicate is_consistent (board: array int) (pos: int) = forall q. 0 <= q < pos -> consistent_row board pos q |
Implementing a function which decides this predicate is another matter. In order for it to be efficient, we want to return False as soon as a queen attacks the queen on row pos. We use an exception for this purpose and it carries the row of the attacking queen:
exception Inconsistent int |
The check is implemented by a function check_is_consistent
,
which takes the board and the row pos as arguments, and scans
rows from 0 to pos-1 looking for an attacking queen. As soon
as one is found, the exception is raised. It is caught immediately
outside the loop and False is returned. Whenever the end of
the loop is reached, True is returned.
let check_is_consistent (board: array int) (pos: int) : bool requires { 0 <= pos < length board } ensures { result <-> is_consistent board pos } = try for q = 0 to pos - 1 do invariant { forall j:int. 0 <= j < q -> consistent_row board pos j } let bq = board[q] in let bpos = board[pos] in if bq = bpos then raise (Inconsistent q); if bq - bpos = pos - q then raise (Inconsistent q); if bpos - bq = pos - q then raise (Inconsistent q) done; True with Inconsistent q -> assert { not (consistent_row board pos q) }; False end |
The assertion in the exception handler is a cut for SMT solvers. This first part of the solution is given below.
module NQueens use import int.Int use import array.Array predicate consistent_row (board: array int) (pos: int) (q: int) = board[q] <> board[pos] /\ board[q] - board[pos] <> pos - q /\ board[pos] - board[q] <> pos - q predicate is_consistent (board: array int) (pos: int) = forall q. 0 <= q < pos -> consistent_row board pos q exception Inconsistent int let check_is_consistent (board: array int) (pos: int) requires { 0 <= pos < length board } ensures { result <-> is_consistent board pos } = try for q = 0 to pos - 1 do invariant { forall j:int. 0 <= j < q -> consistent_row board pos j } let bq = board[q] in let bpos = board[pos] in if bq = bpos then raise (Inconsistent q); if bq - bpos = pos - q then raise (Inconsistent q); if bpos - bq = pos - q then raise (Inconsistent q) done; True with Inconsistent q -> assert { not (consistent_row board pos q) }; False end |
We now proceed with the verification of the backtracking algorithm.
The specification requires us to define the notion of solution, which
is straightforward using the predicate is_consistent
above.
However, since the algorithm will try to complete a given partial
solution, it is more convenient to define the notion of partial
solution, up to a given row. It is even more convenient to split it in
two predicates, one related to legal column values and another to
consistency of rows:
predicate is_board (board: array int) (pos: int) = forall q. 0 <= q < pos -> 0 <= board[q] < length board predicate solution (board: array int) (pos: int) = is_board board pos /\ forall q. 0 <= q < pos -> is_consistent board q |
The algorithm will not mutate the partial solution it is given and, in case of a search failure, will claim that there is no solution extending this prefix. For this reason, we introduce a predicate comparing two chess boards for equality up to a given row:
predicate eq_board (b1 b2: array int) (pos: int) = forall q. 0 <= q < pos -> b1[q] = b2[q] |
The search itself makes use of an exception to signal a successful search:
exception Solution |
The backtracking code is a recursive function bt_queens
which
takes the chess board, its size, and the starting row for the search.
The termination is ensured by the obvious variant n-pos.
let rec bt_queens (board: array int) (n: int) (pos: int) : unit variant { n - pos } |
The precondition relates board, pos, and n and requires board to be a solution up to pos:
requires { 0 <= pos <= n = length board } requires { solution board pos } |
The postcondition is twofold: either the function exits normally and then there is no solution extending the prefix in board, which has not been modified; or the function raises Solution and we have a solution in board.
ensures { eq_board board (old board) pos } ensures { forall b:array int. length b = n -> is_board b n -> eq_board board b pos -> not (solution b n) } raises { Solution -> solution board n } = |
Whenever we reach the end of the chess board, we have found a solution and we signal it using exception Solution:
if pos = n then raise Solution; |
Otherwise we scan all possible positions for the queen on row pos with a for loop:
for i = 0 to n - 1 do |
The loop invariant states that we have not modified the solution prefix so far, and that we have not found any solution that would extend this prefix with a queen on row pos at a column below i:
invariant { eq_board board (old board) pos } invariant { forall b:array int. length b = n -> is_board b n -> eq_board board b pos -> 0 <= b[pos] < i -> not (solution b n) } |
Then we assign column i to the queen on row pos and
we check for a possible attack with check_is_consistent
. If
not, we call bt_queens
recursively on the next row.
board[pos] <- i; if check_is_consistent board pos then bt_queens board n (pos + 1) done |
This completes the loop and function bt_queens
as well.
Solving the puzzle is a simple call to bt_queens
, starting the
search on row 0. The postcondition is also twofold, as for
bt_queens
, yet slightly simpler.
let queens (board: array int) (n: int) : unit requires { length board = n } ensures { forall b:array int. length b = n -> is_board b n -> not (solution b n) } raises { Solution -> solution board n } = bt_queens board n 0 |
This second part of the solution is given below. With the help of a few auxiliary lemmas — not given here but available from Why3’s sources — the verification conditions are all discharged automatically, including the verification of the lemmas themselves.
predicate is_board (board: array int) (pos: int) = forall q. 0 <= q < pos -> 0 <= board[q] < length board predicate solution (board: array int) (pos: int) = is_board board pos /\ forall q. 0 <= q < pos -> is_consistent board q predicate eq_board (b1 b2: array int) (pos: int) = forall q. 0 <= q < pos -> b1[q] = b2[q] exception Solution let rec bt_queens (board: array int) (n: int) (pos: int) : unit variant { n - pos } requires { 0 <= pos <= n = length board } requires { solution board pos } ensures { eq_board board (old board) pos } ensures { forall b:array int. length b = n -> is_board b n -> eq_board board b pos -> not (solution b n) } raises { Solution -> solution board n } = if pos = n then raise Solution; for i = 0 to n - 1 do invariant { eq_board board (old board) pos } invariant { forall b:array int. length b = n -> is_board b n -> eq_board board b pos -> 0 <= b[pos] < i -> not (solution b n) } board[pos] <- i; if check_is_consistent board pos then bt_queens board n (pos + 1) done let queens (board: array int) (n: int) : unit requires { length board = n } ensures { forall b:array int. length b = n -> is_board b n -> not (solution b n) } raises { Solution -> solution board n } = bt_queens board n 0 end |
The last problem consists in verifying the implementation of a well-known purely applicative data structure for queues. A queue is composed of two lists, front and rear. We push elements at the head of list rear and pop them off the head of list front. We maintain that the length of front is always greater or equal to the length of rear. (See for instance Okasaki’s Purely Functional Data Structures [9] for more details.)
We have to implement operations empty, head, tail, and enqueue over this data type, to show that the invariant over lengths is maintained, and finally
to show that a client invoking these operations observes an abstract queue given by a sequence.
In a new module, we import arithmetic and theory list.ListRich, a combo theory that imports all list operations we will require: length, reversal, and concatenation.
module AmortizedQueue use import int.Int use import option.Option use export list.ListRich |
The queue data type is naturally introduced as a polymorphic record type. The two list lengths are explicitly stored, for greater efficiency.
type queue 'a = { front: list 'a; lenf: int; rear : list 'a; lenr: int; } invariant { length front = lenf >= length rear = lenr } by { front = Nil; lenf = 0; rear = Nil; lenr = 0 } |
The type definition is accompanied with an invariant — a logical property imposed on any value of the type. Why3 assumes that any queue passed as an argument to a program function satisfies the invariant and it produces a proof obligation every time a queue is created. The by clause ensures the non-vacuity of this type with invariant. If you omit it, a goal with an existential statement is generated.
For the purpose of the specification, it is convenient to introduce a function sequence which builds the sequence of elements of a queue, that is the front list concatenated to the reversed rear list.
function sequence (q: queue 'a) : list 'a = q.front ++ reverse q.rear |
It is worth pointing out that this function can only be used in specifications. We start with the easiest operation: building the empty queue.
let empty () : queue 'a ensures { sequence result = Nil } = { front = Nil; lenf = 0; rear = Nil; lenr = 0 } |
The postcondition states that the returned queue represents the empty sequence. Another postcondition, saying that the returned queue satisfies the type invariant, is implicit. Note the cast to type queue ’a. It is required, for the type checker not to complain about an undefined type variable.
The next operation is head, which returns the first element from a given queue q. It naturally requires the queue to be non empty, which is conveniently expressed as sequence q not being Nil.
let head (q: queue 'a) : 'a requires { sequence q <> Nil } ensures { hd (sequence q) = Some result } = let Cons x _ = q.front in x |
The fact that the argument q satisfies the type invariant is implicitly assumed. The type invariant is required to prove the absurdity of q.front being Nil (otherwise, sequence q would be Nil as well).
The next operation is tail, which removes the first element from a given queue. This is more subtle than head, since we may have to re-structure the queue to maintain the invariant. Since we will have to perform a similar operation when implementing operation enqueue later, it is a good idea to introduce a smart constructor create that builds a queue from two lists while ensuring the invariant. The list lengths are also passed as arguments, to avoid unnecessary computations.
let create (f: list 'a) (lf: int) (r: list 'a) (lr: int) : queue 'a requires { lf = length f /\ lr = length r } ensures { sequence result = f ++ reverse r } = if lf >= lr then { front = f; lenf = lf; rear = r; lenr = lr } else let f = f ++ reverse r in { front = f; lenf = lf + lr; rear = Nil; lenr = 0 } |
If the invariant already holds, it is simply a matter of building the record. Otherwise, we empty the rear list and build a new front list as the concatenation of list f and the reversal of list r. The principle of this implementation is that the cost of this reversal will be amortized over all queue operations. Implementing function tail is now straightforward and follows the structure of function head.
let tail (q: queue 'a) : queue 'a requires { sequence q <> Nil } ensures { tl (sequence q) = Some (sequence result) } = let Cons _ r = q.front in create r (q.lenf - 1) q.rear q.lenr |
The last operation is enqueue, which pushes a new element in a given queue. Reusing the smart constructor create makes it a one line code.
let enqueue (x: 'a) (q: queue 'a) : queue 'a ensures { sequence result = sequence q ++ Cons x Nil } = create q.front q.lenf (Cons x q.rear) (q.lenr + 1) |
The code is given below. The verification conditions are all discharged automatically.
module AmortizedQueue use import int.Int use import option.Option use import list.ListRich type queue 'a = { front: list 'a; lenf: int; rear : list 'a; lenr: int; } invariant { length front = lenf >= length rear = lenr } by { front = Nil; lenf = 0; rear = Nil; lenr = 0 } function sequence (q: queue 'a) : list 'a = q.front ++ reverse q.rear let empty () : queue 'a ensures { sequence result = Nil } = { front = Nil; lenf = 0; rear = Nil; lenr = 0 } let head (q: queue 'a) : 'a requires { sequence q <> Nil } ensures { hd (sequence q) = Some result } = let Cons x _ = q.front in x let create (f: list 'a) (lf: int) (r: list 'a) (lr: int) : queue 'a requires { lf = length f /\ lr = length r } ensures { sequence result = f ++ reverse r } = if lf >= lr then { front = f; lenf = lf; rear = r; lenr = lr } else let f = f ++ reverse r in { front = f; lenf = lf + lr; rear = Nil; lenr = 0 } let tail (q: queue 'a) : queue 'a requires { sequence q <> Nil } ensures { tl (sequence q) = Some (sequence result) } = let Cons _ r = q.front in create r (q.lenf - 1) q.rear q.lenr let enqueue (x: 'a) (q: queue 'a) : queue 'a ensures { sequence result = sequence q ++ Cons x Nil } = create q.front q.lenf (Cons x q.rear) (q.lenr + 1) end |
This chapter is a tutorial for the users who want to link their own OCaml code with the Why3 library. We progressively introduce the way one can use the library to build terms, formulas, theories, proof tasks, call external provers on tasks, and apply transformations on tasks. The complete documentation for API calls is given at this URL.
We assume the reader has a fair knowledge of the OCaml
language. Notice that the Why3 library must be installed, see
Section 4.1.2. The OCaml code given below is available in
the source distribution in directory examples/use_api/
together
with a few other examples.
The first step is to know how to build propositional formulas. The module Term gives a few functions for building these. Here is a piece of OCaml code for building the formula true ∨ false.
(* opening the Why3 library *) open Why3 (* a ground propositional goal: true or false *) let fmla_true : Term.term = Term.t_true let fmla_false : Term.term = Term.t_false let fmla1 : Term.term = Term.t_or fmla_true fmla_false |
The library uses the common type term both for terms (i.e. expressions that produce a value of some particular type) and formulas (i.e. boolean-valued expressions).
Such a formula can be printed using the module Pretty providing pretty-printers.
(* printing it *) open Format let () = printf "@[formula 1 is:@ %a@]@." Pretty.print_term fmla1 |
Assuming the lines above are written in a file f.ml, it can be compiled using
ocamlfind ocamlc -package why3 -linkpkg f.ml -o f
Running the generated executable f results in the following output.
formula 1 is: true \/ false
Let us now build a formula with propositional variables: A ∧ B → A. Propositional variables must be declared first before using them in formulas. This is done as follows.
let prop_var_A : Term.lsymbol = Term.create_psymbol (Ident.id_fresh "A") [] let prop_var_B : Term.lsymbol = Term.create_psymbol (Ident.id_fresh "B") [] |
The type lsymbol is the type of function and predicate symbols (which we call logic symbols for brevity). Then the atoms A and B must be built by the general function for applying a predicate symbol to a list of terms. Here we just need the empty list of arguments.
let atom_A : Term.term = Term.ps_app prop_var_A [] let atom_B : Term.term = Term.ps_app prop_var_B [] let fmla2 : Term.term = Term.t_implies (Term.t_and atom_A atom_B) atom_A let () = printf "@[formula 2 is:@ %a@]@." Pretty.print_term fmla2 |
As expected, the output is as follows.
formula 2 is: A /\ B -> A
Notice that the concrete syntax of Why3 forbids function and predicate names to start with a capital letter (except for the algebraic type constructors which must start with one). This constraint is not enforced when building those directly using library calls.
Let us see how we can call a prover to prove a formula. As said in previous chapters, a prover must be given a task, so we need to build tasks from our formulas. Task can be build incrementally from an empty task by adding declaration to it, using the functions add_*_decl of module Task. For the formula true ∨ false above, this is done as follows.
(* building the task for formula 1 alone *) let task1 : Task.task = None (* empty task *) let goal_id1 : Decl.prsymbol = Decl.create_prsymbol (Ident.id_fresh "goal1") let task1 : Task.task = Task.add_prop_decl task1 Decl.Pgoal goal_id1 fmla1 |
To make the formula a goal, we must give a name to it, here “goal1”. A goal name has type prsymbol, for identifiers denoting propositions in a theory or a task. Notice again that the concrete syntax of Why3 requires these symbols to be capitalized, but it is not mandatory when using the library. The second argument of add_prop_decl is the kind of the proposition: Paxiom, Plemma or Pgoal. Notice that lemmas are not allowed in tasks and can only be used in theories.
Once a task is built, it can be printed.
(* printing the task *) let () = printf "@[task 1 is:@\n%a@]@." Pretty.print_task task1 |
The task for our second formula is a bit more complex to build, because the variables A and B must be added as abstract (i.e. not defined) propositional symbols in the task.
(* task for formula 2 *) let task2 = None let task2 = Task.add_param_decl task2 prop_var_A let task2 = Task.add_param_decl task2 prop_var_B let goal_id2 = Decl.create_prsymbol (Ident.id_fresh "goal2") let task2 = Task.add_prop_decl task2 Decl.Pgoal goal_id2 fmla2 let () = printf "@[task 2 created:@\n%a@]@." Pretty.print_task task2 |
Execution of our OCaml program now outputs:
task 1 is: theory Task goal Goal1 : true \/ false end task 2 is: theory Task predicate A predicate B goal Goal2 : A /\ B -> A end
To call an external prover, we need to access the Why3 configuration file why3.conf, as it was built using the why3config command line tool or the Detect Provers menu of the graphical IDE. The following API calls allow to access the content of this configuration file.
(* reads the config file *) let config : Whyconf.config = Whyconf.read_config None (* the [main] section of the config file *) let main : Whyconf.main = Whyconf.get_main config (* all the provers detected, from the config file *) let provers : Whyconf.config_prover Whyconf.Mprover.t = Whyconf.get_provers config |
The type ’a Whyconf.Mprover.t is a map indexed by provers. A prover is a record with a name, a version, and an alternative description (to differentiate between various configurations of a given prover). Its definition is in the module Whyconf:
type prover = { prover_name : string; prover_version : string; prover_altern : string; } |
The map provers provides the set of existing provers. In the following, we directly attempt to access a prover named “Alt-Ergo”, any version.
(* One prover named Alt-Ergo in the config file *) let alt_ergo : Whyconf.config_prover = let fp = Whyconf.parse_filter_prover "Alt-Ergo" in (** all provers that have the name "Alt-Ergo" *) let provers = Whyconf.filter_provers config fp in if Whyconf.Mprover.is_empty provers then begin eprintf "Prover Alt-Ergo not installed or not configured@."; exit 0 end else snd (Whyconf.Mprover.max_binding provers) |
We could also get a specific version with :
(* Specific version 2.0.0 of Alt-Ergo in the config file *) let alt_ergo_2_0_0 : Whyconf.config_prover = let fp = Whyconf.parse_filter_prover "Alt-Ergo,2.0.0" in let provers = Whyconf.filter_provers config fp in if Whyconf.Mprover.is_empty provers then begin eprintf "Prover Alt-Ergo 2.0.0 not installed or not configured@."; exit 0 end else snd (Whyconf.Mprover.max_binding provers) |
The next step is to obtain the driver associated to this prover. A driver typically depends on the standard theories so these should be loaded first.
(* builds the environment from the [loadpath] *) let env : Env.env = Env.create_env (Whyconf.loadpath main) (* loading the Alt-Ergo driver *) let alt_ergo_driver : Driver.driver = try Whyconf.load_driver main env alt_ergo.Whyconf.driver [] with e -> eprintf "Failed to load driver for alt-ergo: %a@." Exn_printer.exn_printer e; exit 1 |
We are now ready to call the prover on the tasks. This is done by a function call that launches the external executable and waits for its termination. Here is a simple way to proceed:
(* calls Alt-Ergo *) let result1 : Call_provers.prover_result = Call_provers.wait_on_call (Driver.prove_task ~limit:Call_provers.empty_limit ~command:alt_ergo.Whyconf.command alt_ergo_driver task1) (* prints Alt-Ergo answer *) let () = printf "@[On task 1, Alt-Ergo answers %a@." Call_provers.print_prover_result result1 |
This way to call a prover is in general too naive, since it may never return if the prover runs without time limit. The function prove_task has an optional parameter limit, a record defined in module Call_provers:
type resource_limit = { limit_time : int; limit_mem : int; limit_steps : int; } |
where the field limit_time is the maximum allowed running time in seconds, and limit_mem is the maximum allowed memory in megabytes. The type prover_result is a record defined in module Call_provers:
type prover_result = { pr_answer : prover_answer; pr_status : Unix.process_status; pr_output : string; pr_time : float; pr_steps : int; (* -1 if unknown *) pr_model : model; } |
with in particular the fields:
A pr_answer is the sum type defined in module Call_provers:
type prover_answer = | Valid | Invalid | Timeout | OutOfMemory | StepLimitExceeded | Unknown of string | Failure of string | HighFailure |
corresponding to these kinds of answers:
Here is thus another way of calling the Alt-Ergo prover, on our second task.
let result2 : Call_provers.prover_result = Call_provers.wait_on_call (Driver.prove_task ~command:alt_ergo.Whyconf.command ~limit:{Call_provers.empty_limit with Call_provers.limit_time = 10} alt_ergo_driver task2) let () = printf "@[On task 2, alt-ergo answers %a in %5.2f seconds@." Call_provers.print_prover_answer result1.Call_provers.pr_answer result1.Call_provers.pr_time |
The output of our program is now as follows.
On task 1, alt-ergo answers Valid (0.01s) On task 2, alt-ergo answers Valid in 0.01 seconds
An important feature of the functions for building terms and formulas is that they statically guarantee that only well-typed terms can be constructed.
Here is the way we build the formula 2+2=4. The main difficulty is to access the internal identifier for addition: it must be retrieved from the standard theory Int of the file int.why.
let two : Term.term = Term.t_nat_const 2 let four : Term.term = Term.t_nat_const 4 let int_theory : Theory.theory = Env.read_theory env ["int"] "Int" let plus_symbol : Term.lsymbol = Theory.ns_find_ls int_theory.Theory.th_export ["infix +"] let two_plus_two : Term.term = Term.t_app_infer plus_symbol [two;two] let fmla3 : Term.term = Term.t_equ two_plus_two four |
An important point to notice as that when building the application of + to the arguments, it is checked that the types are correct. Indeed the constructor t_app_infer infers the type of the resulting term. One could also provide the expected type as follows.
let two_plus_two : Term.term = Term.fs_app plus_symbol [two;two] Ty.ty_int |
When building a task with this formula, we need to declare that we use theory Int:
let task3 = None let task3 = Task.use_export task3 int_theory let goal_id3 = Decl.create_prsymbol (Ident.id_fresh "goal3") let task3 = Task.add_prop_decl task3 Decl.Pgoal goal_id3 fmla3 |
To illustrate how to build quantified formulas, let us consider the formula ∀ x:int. x*x ≥ 0. The first step is to obtain the symbols from Int.
let zero : Term.term = Term.t_nat_const 0 let mult_symbol : Term.lsymbol = Theory.ns_find_ls int_theory.Theory.th_export ["infix *"] let ge_symbol : Term.lsymbol = Theory.ns_find_ls int_theory.Theory.th_export ["infix >="] |
The next step is to introduce the variable x with the type int.
let var_x : Term.vsymbol = Term.create_vsymbol (Ident.id_fresh "x") Ty.ty_int |
The formula x*x ≥ 0 is obtained as in the previous example.
let x : Term.term = Term.t_var var_x let x_times_x : Term.term = Term.t_app_infer mult_symbol [x;x] let fmla4_aux : Term.term = Term.ps_app ge_symbol [x_times_x;zero] |
To quantify on x, we use the appropriate smart constructor as follows.
let fmla4 : Term.term = Term.t_forall_close [var_x] [] fmla4_aux |
We illustrate now how one can build theories. Building a theory must be done by a sequence of calls:
Theory.theory_uc
;
Theory.theory
.
Creation of a theory named My_theory
is done by
let my_theory : Theory.theory_uc = Theory.create_theory (Ident.id_fresh "My_theory") |
First let us add formula 1 above as a goal:
let decl_goal1 : Decl.decl = Decl.create_prop_decl Decl.Pgoal goal_id1 fmla1 let my_theory : Theory.theory_uc = Theory.add_decl my_theory decl_goal1 |
Note that we reused the goal identifier goal_id1
that we
already defined to create task 1 above.
Adding formula 2 needs to add the declarations of predicate variables A and B first:
let my_theory : Theory.theory_uc = Theory.add_param_decl my_theory prop_var_A let my_theory : Theory.theory_uc = Theory.add_param_decl my_theory prop_var_B let decl_goal2 : Decl.decl = Decl.create_prop_decl Decl.Pgoal goal_id2 fmla2 let my_theory : Theory.theory_uc = Theory.add_decl my_theory decl_goal2 |
Adding formula 3 is a bit more complex since it uses integers, thus it
requires to “use” the theory int.Int
. Using a theory is
indeed not a primitive operation in the API: it must be done by a
combination of an “export” and the creation of a namespace. We
provide a helper function for that:
(* helper function: [use th1 th2] insert the equivalent of a "use import th2" in theory th1 under construction *) let use th1 th2 = let name = th2.Theory.th_name in Theory.close_scope (Theory.use_export (Theory.open_scope th1 name.Ident.id_string) th2) ~import:true |
Addition of formula 3 is then
let my_theory : Theory.theory_uc = use my_theory int_theory let decl_goal3 : Decl.decl = Decl.create_prop_decl Decl.Pgoal goal_id3 fmla3 let my_theory : Theory.theory_uc = Theory.add_decl my_theory decl_goal3 |
Addition of goal 4 is nothing more complex:
let decl_goal4 : Decl.decl = Decl.create_prop_decl Decl.Pgoal goal_id4 fmla4 let my_theory : Theory.theory_uc = Theory.add_decl my_theory decl_goal4 |
Finally, we close our theory under construction as follows.
let my_theory : Theory.theory = Theory.close_theory my_theory |
We can inspect what we did by printing that theory:
let () = printf "@[my new theory is as follows:@\n@\n%a@]@." Pretty.print_theory my_theory |
which outputs
my new theory is as follows: theory My_theory (* use BuiltIn *) goal goal1 : true \/ false predicate A predicate B goal goal2 : A /\ B -> A (* use int.Int *) goal goal3 : (2 + 2) = 4 goal goal4 : forall x:int. (x * x) >= 0 end
From a theory, one can compute at once all the proof tasks it contains as follows:
let my_tasks : Task.task list = List.rev (Task.split_theory my_theory None None) |
Note that the tasks are returned in reverse order, so we reverse the list above.
We can check our generated tasks by printing them:
let () = printf "Tasks are:@."; let _ = List.fold_left (fun i t -> printf "Task %d: %a@." i Pretty.print_task t; i+1) 1 my_tasks in () |
One can run provers on those tasks exactly as we did above.
The following code illustrates a simple recursive functions of formulas. It explores the formula and when a negation is found, it tries to push it down below a conjunction, a disjunction or a quantifier.
open Term let rec negate (t:term) : term = match t.t_node with | Ttrue -> t_false | Tfalse -> t_true | Tnot t -> t | Tbinop(Tand,t1,t2) -> t_or (negate t1) (negate t2) | Tbinop(Tor,t1,t2) -> t_and (negate t1) (negate t2) | Tquant(Tforall,tq) -> let vars,triggers,t' = t_open_quant tq in let tq' = t_close_quant vars triggers (negate t') in t_exists tq' | Tquant(Texists,tq) -> let vars,triggers,t' = t_open_quant tq in let tq' = t_close_quant vars triggers (negate t') in t_forall tq' | _ -> t_not t let rec traverse (t:term) : term = match t.t_node with | Tnot t -> t_map traverse (negate t) | _ -> t_map traverse t |
The following illustrates how to turn such an OCaml function into a transformation in the sense of the Why3 API. Moreover, it registers that transformation to make it available for example in Why3 IDE.
let negate_goal pr t = [Decl.create_prop_decl Decl.Pgoal pr (traverse t)] let negate_trans = Trans.goal negate_goal let () = Trans.register_transform "push_negations_down" negate_trans ~desc:"In the current goal,@ push negations down,@ \ across logical connectives." |
The directory src/transform
contains the code for the many
transformations that are already available in Why3.
See the example examples/use_api/create_session.ml
of the
distribution for an illustration on how to manipulate proof sessions
from an OCaml program.
The simplest way to build WhyML programs from OCaml is to build untyped syntax trees for such programs, and then call the Why3 typing procedure to build typed declarations.
The examples of this section are available in the file
examples/use_api/mlw_tree.ml
of the distribution.
The first step is to build an environment as already illustrated in
Section 3.3, and open the OCaml module
Ptree
which contains most of the OCaml functions we need in
this section.
open Why3 let config : Whyconf.config = Whyconf.read_config None let main : Whyconf.main = Whyconf.get_main config let env : Env.env = Env.create_env (Whyconf.loadpath main) open Ptree |
To contain all the example programs we are going to build we need a
module. We start the creation of that module using the following
declarations, that first introduces a pseudo “file” to hold the
module, then the module itself called Program
.
let () = Typing.open_file env [] (* empty pathname *) let mk_ident s = { id_str = s; id_ats = []; id_loc = Loc.dummy_position } let () = Typing.open_module (mk_ident "Program") |
Notice the use of a first
simple helper function mk_ident
to build an identifier without
any attributes nor any location.
To write our programs, we need to import some other modules from the
standard library. The following introduces two helper functions for
building qualified identifiers and importing modules, and finally
imports int.Int
.
let mk_qid l = let rec aux l = match l with | [] -> assert false | [x] -> Qident(mk_ident x) | x::r -> Qdot(aux r,mk_ident x) in aux (List.rev l) let use_import (f, m) = let m = mk_ident m in let loc = Loc.dummy_position in Typing.open_scope loc m; Typing.add_decl loc (Ptree.Duse (Qdot (Qident (mk_ident f), m))); Typing.close_scope loc ~import:true let use_int_Int = use_import ("int","Int") |
We want now to build a program equivalent to the following code in concrete Why3 syntax.
let f1 (x:int) : unit requires { x=6 } ensures { result=42 } = x*7 |
The OCaml code that programmatically build this Why3 function is as follows.
let eq_symb = mk_qid [Ident.op_infix "="] let int_type_id = mk_qid ["int"] let int_type = PTtyapp(int_type_id,[]) let mul_int = mk_qid ["Int";Ident.op_infix "*"] let d1 : decl = let id_x = mk_ident "x" in let pre = mk_tapp eq_symb [mk_var id_x; mk_tconst "6"] in let result = mk_ident "result" in let post = mk_tapp eq_symb [mk_var result; mk_tconst "42"] in let spec = { sp_pre = [pre]; sp_post = [Loc.dummy_position,[pat_var result,post]]; sp_xpost = []; sp_reads = []; sp_writes = []; sp_alias = []; sp_variant = []; sp_checkrw = false; sp_diverge = false; sp_partial = false; } in let body = mk_eapp mul_int [mk_evar id_x; mk_econst "7"] in let f1 = Efun(param1 id_x int_type, None, Ity.MaskVisible, spec, body) in Dlet(mk_ident "f1",false,Expr.RKnone, mk_expr f1) let () = try Typing.add_decl Loc.dummy_position d1 with e -> Format.printf "Exception raised during typing of d:@ %a@." Exn_printer.exn_printer e |
This code makes uses of helper functions that are given in Figure 3.1.
let mk_expr e = { expr_desc = e; expr_loc = Loc.dummy_position } let mk_term t = { term_desc = t; term_loc = Loc.dummy_position } let mk_pat p = { pat_desc = p; pat_loc = Loc.dummy_position } let pat_var id = mk_pat (Pvar id) let mk_var id = mk_term (Tident (Qident id)) let param0 = [Loc.dummy_position, None, false, Some (PTtuple [])] let param1 id ty = [Loc.dummy_position, Some id, false, Some ty] let mk_tconst s = mk_term (Tconst Number.(ConstInt { ic_negative = false ; ic_abs = int_literal_dec s })) let mk_econst s = mk_expr (Econst Number.(ConstInt { ic_negative = false ; ic_abs = int_literal_dec s })) let mk_tapp f l = mk_term (Tidapp(f,l)) let mk_eapp f l = mk_expr (Eidapp(f,l)) let mk_evar x = mk_expr(Eident(Qident x))
Figure 3.1: Helper functions for building WhyML programs
We want now to build a program equivalent to the following code in concrete Why3 syntax.
let f2 () : int requires { true } ensures { result >= 0 } = let x = ref 42 in !x |
We need to import the ref.Ref
module first. The rest is similar to the first example, the code is as follows
let ge_int = mk_qid ["Int";Ident.op_infix ">="] let use_ref_Ref = use_import ("ref","Ref") let d2 = let result = mk_ident "result" in let post = mk_term(Tidapp(ge_int,[mk_var result;mk_tconst "0"])) in let spec = { sp_pre = []; sp_post = [Loc.dummy_position,[pat_var result,post]]; sp_xpost = []; sp_reads = []; sp_writes = []; sp_alias = []; sp_variant = []; sp_checkrw = false; sp_diverge = false; sp_partial = false; } in let body = let e1 = mk_eapp (mk_qid ["Ref";"ref"]) [mk_econst "42"] in let id_x = mk_ident "x" in let e2 = mk_eapp (mk_qid ["Ref";Ident.op_prefix "!"]) [mk_evar id_x] in mk_expr(Elet(id_x,false,Expr.RKlocal,e1,e2)) in let f = Efun(param0,None,Ity.MaskVisible,spec,body) in Dlet(mk_ident "f2",false,Expr.RKnone, mk_expr f) let () = try Typing.add_decl Loc.dummy_position d2 with e -> Format.printf "Exception raised during typing of d2:@ %a@." Exn_printer.exn_printer e |
The next example makes use of arrays.
let f (a:array int) : unit requires { a.length >= 1 } ensures { a[0] = 42 } = a[0] <- 42 |
The corresponding OCaml code is as follows
let () = use_import ("array","Array") let array_int_type = PTtyapp(mk_qid ["Array";"array"],[int_type]) let length = mk_qid ["Array";"length"] let array_get = mk_qid ["Array"; Ident.op_get ""] let array_set = mk_qid ["Array"; Ident.op_set ""] let d3 = let id_a = mk_ident "a" in let pre = mk_tapp ge_int [mk_tapp length [mk_var id_a]; mk_tconst "1"] in let post = mk_tapp eq_symb [mk_tapp array_get [mk_var id_a; mk_tconst "0"]; mk_tconst "42"] in let spec = { sp_pre = [pre]; sp_post = [Loc.dummy_position,[mk_pat Pwild,post]]; sp_xpost = []; sp_reads = []; sp_writes = []; sp_alias = []; sp_variant = []; sp_checkrw = false; sp_diverge = false; sp_partial = false; } in let body = mk_eapp array_set [mk_evar id_a; mk_econst "0"; mk_econst "42"] in let f = Efun(param1 id_a array_int_type, None,Ity.MaskVisible,spec,body) in Dlet(mk_ident "f3", false, Expr.RKnone, mk_expr f) let () = try Typing.add_decl Loc.dummy_position d3 with e -> Format.printf "Exception raised during typing of d3:@ %a@." Exn_printer.exn_printer e |
Having declared all the programs we wanted to write, we can now close the module and the file, and get as a result the set of modules of our file, under the form of a map of module names to modules.
let () = Typing.close_module Loc.dummy_position let mods : Pmodule.pmodule Wstdlib.Mstr.t = Typing.close_file () |
We can then construct the proofs tasks for our module, and then try to call the Alt-Ergo prover. The rest of that code is using OCaml functions that were already introduced before.
let my_tasks : Task.task list = let mods = Wstdlib.Mstr.fold (fun _ m acc -> List.rev_append (Task.split_theory m.Pmodule.mod_theory None None) acc) mods [] in List.rev mods open Format let () = printf "Tasks are:@."; let _ = List.fold_left (fun i t -> printf "Task %d: %a@." i Pretty.print_task t; i+1) 1 my_tasks in () let provers : Whyconf.config_prover Whyconf.Mprover.t = Whyconf.get_provers config let alt_ergo : Whyconf.config_prover = let fp = Whyconf.parse_filter_prover "Alt-Ergo" in (** all provers that have the name "Alt-Ergo" *) let provers = Whyconf.filter_provers config fp in if Whyconf.Mprover.is_empty provers then begin eprintf "Prover Alt-Ergo not installed or not configured@."; exit 0 end else snd (Whyconf.Mprover.max_binding provers) let alt_ergo_driver : Driver.driver = try Whyconf.load_driver main env alt_ergo.Whyconf.driver [] with e -> eprintf "Failed to load driver for alt-ergo: %a@." Exn_printer.exn_printer e; exit 1 let () = let _ = List.fold_left (fun i t -> let r = Call_provers.wait_on_call (Driver.prove_task ~limit:Call_provers.empty_limit ~command:alt_ergo.Whyconf.command alt_ergo_driver t) in printf "@[On task %d, alt-ergo answers %a@." i Call_provers.print_prover_result r; i+1 ) 1 my_tasks in () |
That feature is presented in details in Section 5.3.7, that should be read first. The counterexamples can also be generated using the API. The following explains how to change the source code (mainly adding attributes) in order to display counterexamples and how to parse the result given by Why3. To illustrate this, we will adapt the examples from Section 3.1 to display counterexamples.
For variables to be used for counterexamples they need to contain an attribute
called model_trace
and a location. The model_trace
states the
name the user wants the variable to be named in the output of the
counterexamples pass. Usually, people put a reference to their program AST node
in this attribute: this helps them to parse and display the results given by
Why3.
The locations are also necessary as every counterexamples values with no
location won’t be displayed. For example, an assignment of the source language
such as the following will probably trigger the creation of an ident (for the
left value) in a user subsequent tasks:
x := !y + 1 |
This means that the ident generated for x will hold both a model_trace
and a location.
The example becomes the following:
let make_attribute (name: string) : Ident.attribute = Ident.create_attribute ("model_trace:" ^ name) let prop_var_A : Term.lsymbol = (* [user_position file line left_col right_col] *) let loc = Loc.user_position "myfile.my_ext" 28 0 0 in let attrs = Ident.Sattr.singleton (make_attribute "my_A") in Term.create_psymbol (Ident.id_fresh ~attrs ~loc "A") [] |
In the above, we defined a proposition ident with a location and a
model_trace
.
Now that variables are tagged, we can define formulas. To define a goal formula
for counterexamples, we need to tag it with the vc:annotation
attribute. This attribute is automatically added when using the VC generation
of Why3, but on a user-built task, this needs to be added. We also need to add
a location for this goal.
The following is obtained for the simple formula linking A and B:
let atom_A : Term.term = Term.ps_app prop_var_A [] let atom_B : Term.term = Term.ps_app prop_var_B [] (* Voluntarily wrong verification condition *) let fmla2 : Term.term = Term.t_implies atom_A (Term.t_and atom_A atom_B) (* We add a location and attribute to indicate the start of a goal *) let fmla2 : Term.term = let loc = Loc.user_position "myfile.my_ext" 42 28 91 in let attrs = Ident.Sattr.singleton Ity.annot_attr in (* Note that this remove any existing attribute/locations on fmla2 *) Term.t_attr_set ~loc attrs fmla2 |
Note: the transformations used for counterexamples will create new variables
for each variable occuring inside the formula tagged by
vc:annotation
. These variables are duplicates located at the VC
line. They allow giving all counterexample values located at that VC line.
Several output formats are available for counterexamples. For users who want to pretty-print their counterexamples values, we recommend to use the JSON output as follows:
(* prints Cvc4 answer *) let () = printf "@[On task 1, Cvc4 answers %a@." Call_provers.print_prover_result result1 let () = printf "Model is %a@." (Model_parser.print_model_json ?me_name_trans:None ?vc_line_trans:None) result1.Call_provers.pr_model |
Part II |
The simplest way to install Why3 is via OPAM, the OCaml package manager. It is as simple as
> opam install why3
Then jump to Section 4.2 to install external provers.
In short, installation from sources proceeds as follows.
After unpacking the distribution, go to the newly created directory why3-1.2.1. Compilation must start with a configuration phase which is run as
> ./configure
This analyzes your current configuration and checks if requirements hold. Compilation requires:
ocaml ocaml-native-compilersIt is also installable from sources, downloadable from the site http://caml.inria.fr/ocaml/
For some of the Why3 tools, additional OCaml libraries are needed:
liblablgtk2-ocaml-dev liblablgtksourceview2-ocaml-devIt is also installable from sources, available from the site http://wwwfun.kurims.kyoto-u.ac.jp/soft/olabl/lablgtk.html
If you want to use the Coq realizations (Section 8.2), then Coq has to be installed before Why3. Look at the summary printed at the end of the configuration script to check if Coq has been detected properly. Similarly, in order to use PVS (Section 8.5) or Isabelle (Section 8.4) to discharge proofs, PVS and Isabelle must be installed before Why3. You should check that those proof assistants are correctly detected by the configure script.
When configuration is finished, you can compile Why3.
make
Installation is performed (as super-user if needed) using
make install
Installation can be tested as follows:
why3 config --detect
$ cd examples $ why3 replay logic/scottish-private-club 1/1 (replay OK) $ why3 replay same_fringe 18/18 (replay OK)
It is not mandatory to install Why3 into system directories. Why3 can be configured and compiled for local use as follows:
./configure --enable-local make
The Why3 executables are then available in the subdirectory bin/. This directory can be added in your PATH.
By default, the Why3 API is not installed. It can be installed using
Why3 can use a wide range of external theorem provers. These need to be installed separately, and then Why3 needs to be configured to use them. There is no need to install automatic provers, e.g. SMT solvers, before compiling and installing Why3. For installation of external provers, please refer to the specific section about provers from http://why3.lri.fr/. (If you have installed Why3 via OPAM, note that you can install the SMT solver Alt-Ergo via OPAM as well.)
Once you have installed a prover, or a new version of a prover, you have to run the following command:
> why3 config --detect
It scans your PATH for provers and updates your configuration file (see Section 5.1) accordingly.
Why3 is able to use several versions of the same
prover, e.g. it can use both CVC4 1.4 and CVC4 1.5 at the same time.
The automatic detection of provers looks for typical names for their
executable command, e.g. cvc4 for CVC3. However, if you
install several versions of the same prover it is likely that you would
use specialized executable names, such as cvc4-1.4 or
cvc4-1.5. If needed, option --add-prover
can be
added to the config command to specify names of prover executables, e.g.
why3 config --add-prover cvc4 cvc4-dev /usr/local/bin/cvc4-dev
the first argument (here cvc4
) must be one of the family of
provers known. The list of these famillies can be obtain using
why3 config --list-prover-families
as they are in fact listed in the file provers-detection-data.conf
, typically
located in /usr/local/share/why3
after installation. See
Appendix 9.2 for details.
If you happen to upgrade a prover, e.g. installing CVC4 1.5 in place of CVC4 1.4, then the proof sessions formerly recorded will still refer to the old version of the prover. If you open one such a session with the GUI, and replay the proofs, a popup window will show up for asking you to choose between three options:
Notice that if the prover under consideration is an interactive one, then the copy option will duplicate also the edited proof scripts, whereas the upgrade-without-copy option will just reuse the former proof scripts.
Your choice between the three options above will be recorded, one for each prover, in the Why3 configuration file. Within the GUI, you can discard these choices via the Preferences dialog: just click on one choice to remove it.
Outside the GUI, the prover upgrades are handled as follows. The replay command will take into account any prover upgrade policy stored in the configuration. The session command performs move or copy operations on proof attempts in a fine-grained way, using filters, as detailed in Section 5.5.
This chapter details the usage of each of the command-line tools provided by the Why3 environment. The main command is why3; it acts as an entry-point to all the features of Why3. It is invoked as such
why3 [general options...] <command> [specific options...]
The following commands are available:
All these commands are also available as standalone executable files, if needed.
The commands accept a common subset of command-line options. In
particular, option --help
displays the usage and options.
-L
.
-C
.
Why3 must be configured to access external provers. Typically, this is done by running the config command. This must be done each time a new prover is installed.
The provers that Why3 attempts to detect are described in the readable configuration file provers-detection-data.conf of the Why3 data directory (e.g. /usr/local/share/why3). Advanced users may try to modify this file to add support for detection of other provers. (In that case, please consider submitting a new prover configuration on the bug tracking system.)
The result of provers detection is stored in the user’s
configuration file (~/.why3.conf
or, in the case of local
installation, why3.conf
in Why3 sources top directory). This file
is also human-readable, and advanced users may modify it in order to
experiment with different ways of calling provers, e.g. different
versions of the same prover, or with different options.
The config command also detects the plugins installed in the Why3 plugins directory (e.g. /usr/local/lib/why3/plugins). A plugin must register itself as a parser, a transformation or a printer, as explained in the corresponding section.
If the user’s configuration file is already present,
config will only reset unset variables to default value,
but will not try to detect provers.
The option --detect-provers
should be used to force
Why3 to detect again the available
provers and to replace them in the configuration file. The option
--detect-plugins
will do the same for plugins.
If a supported prover is installed under a name
that is not automatically recognized by why3config,
the option --add-prover
will add a specified binary
to the configuration. For example, an Alt-Ergo executable
/home/me/bin/alt-ergo-trunk
can be added as follows:
why3 config --add-prover alt-ergo alt-ergo-trunk /home/me/bin/alt-ergo-trunk
As the first argument, one should put a prover family
identification string. The list of known prover families
can be obtained by the option --list-prover-families
.
Why3 is primarily used to call provers on goals contained in an input file. By default, such a file must be written in WhyML language (extension .mlw). However, a dynamically loaded plugin can register a parser for some other format of logical problems, e.g. TPTP or SMT-LIB.
The prove command executes the following steps:
--format
option to choose
among the available parsers. why3 --list-formats
lists
the registered parsers.
WhyML modules are turned into
theories containing verification conditions as goals.
-G/--goal
and -T/--theory
. Option
-T/--theory
applies to the previous file appearing on the
command line. Option -G/--goal
applies to the previous theory
appearing on the command line. If no theories are selected in a file,
then every theory is considered as selected. If no goals are selected
in a theory, then every goal is considered as selected.
-a/--apply-transform
in their order of appearance on the
command line. why3 --list-transforms
lists the known
transformations; plugins can add more of them.
-D/--driver
option,
or the driver of the prover selected with the -P/--prover
option. why3 --list-provers
lists the known provers, i.e. the ones
that appear in the configuration file.
-P/--prover
is given, call the selected prover
on each generated task and print the results. If option
-D/--driver
is given, print each generated task using
the format specified in the selected driver.
The provers can give the following output:
That feature is presented in details in Section 5.3.7, that should be read first.
Counterexamples are also displayed by the why3 prove command when one selects a prover with the counterexamples alternative. The output is currently done in a JSON syntax (this may change in the future).
The basic usage of the GUI is described by the tutorial of Section 1.2. The command-line options are the common options detailed in introduction to this chapter, plus the specific option already described for the command prove in Section 5.2.2.
At least one anonymous argument must be specified on the command line. More precisely, the first anonymous argument must be the directory of the session. If the directory does not exist, it is created. The other arguments should be existing files that are going to be added to the session. For convenience, if there is only one anonymous argument, it can be an existing file and in this case the session directory is obtained by removing the extension from the file name.
We describe the actions of the various menus and buttons of the interface.
Why3 stores in a session the way you achieve to prove goals that come from a file (.why), from weakest-precondition (.mlw) or by other means. A session stores which file you prove, by applying which transformations, by using which prover. A proof attempt records the complete name of a prover (name, version, optional attribute), the time limit and memory limit given, and the result of the prover. The result of the prover is the same as when you run the prove command. It contains the time taken and the state of the proof:
Additionally, a proof attempt can have the following attributes:
Generally, proof attempts are marked obsolete just after the start of the user interface. Indeed, when you load a session in order to modify it (not with why3session info for instance), Why3 rebuilds the goals to prove by using the information provided in the session. If you modify the original file (.mlw) or if the transformations have changed (new version of Why3), Why3 will detect that. Since the provers might answer differently on these new proof obligations, the corresponding proof attempts are marked obsolete.
The left toolbar that was present in former versions of Why3 is now replaced by a context menu activited by clicking the right mouse button, while cursor is on a given row of the proof session tree.
For automatic provers, this allows to see the file sent to the prover.
For interactive provers, this also allows to add or modify the corresponding proof script. The modifications are saved, and can be retrieved later even if the goal was modified.
Between the top-right zone containing source files and task, and the bottom-right zone containing various messages, a text input field allows the user to invoke commands using a textual interface (see Figure 1.1). The ’help’ command displays a basic list of available commands. All commands available in the menus are also available as a textual command. However the textual interface allows for much more possibilities, including the ability to invoke transformations with arguments.
The preferences dialog allows you to customize various settings. They are grouped together under several tabs.
Note that there are to different buttons to close that dialog. The “Close” button will make modifications of any of these settings effective only for the current run of the GUI. The “Save&Close” button will save the modified settings in Why3 configuration file, to make them permanent.
Why3 provides some support for extracting a potential counterexample from failing proof attempts, for provers that are able to produce a counter-model of the proof task. Why3 attempts to turn this counter-model into values for the free variables of the original Why3 input. Currently, this is supported for CVC4 prover version at least 1.5, and Z3 prover version at least 4.4.0.
The generation of counterexamples is fully integrated in Why3 IDE. The recommended usage is to first start a prover normally, as shown in Figure 5.1) and then click on the status icon for the corresponding proof attempt in the tree. Alternatively, one can use the key shortcut “G” or type get-ce in the command entry. The result can be seen on Figure 5.2: the same prover but with the alternative counterexamples is run. The resulting counterexample is displayed in two different ways. First, it is displayed in the Task tab of the top-right window, at the end of the text of the task, under the form of a list of pairs “variable = value”, ordered by the line number of the source code in which that variable takes that value. Second, it is displayed in the Counterexample tab of the bottom right window, this time interleaved with the code, as shown in Figure 5.2.
![]()
Figure 5.1: Failing execution of CVC4
![]()
Figure 5.2: Counterexamples display for CVC4
The counterexamples can contain values of various types.
To detail the display of map values, consider the following code with a trivially false postcondition:
use int.Int use ref.Ref use map.Map let ghost test_map (ghost x : ref (map int int)) : unit ensures { !x[0] <> !x[1] } = x := Map.set !x 0 3 |
Executing CVC4 with the “counterexamples” alternative on goal will trigger counterexamples:
use int.Int use ref.Ref use map.Map let ghost test_map (ghost x : ref (map int int)) : unit (* x = (1 => 3,others => 0) *) ensures { !x[0] <> !x[1] } (* x = (0 => 3,1 => 3,others => 0) *) = x := Map.set !x 0 3 (* x = (0 => 3,1 => 3,others => 0) *) |
The notation for map is to be understood with indices on left of the arrows and values on the right “(index => value)”. The meaning of the keyword others is the value for all indices that were not mentioned yet. This shows that setting the parameter x to a map that has value 3 for index 1 and zero for all other indices is a counterexample. We can check that this negates the Why3ensures clause.
The counterexamples are known not to work on the following non-exhaustive list (which is undergoing active development):
More information on the implementation of counterexamples in Why3 can be found in [7] and in [5]. For the producing counterexamples using the Why3 API, see Section 3.10.
The replay command is meant to execute the proofs stored in a Why3 session file, as produced by the IDE. Its main purpose is to play non-regression tests. For instance, examples/regtests.sh is a script that runs regression tests on all the examples.
The tool is invoked in a terminal or a script using
The session file why3session.xml stored in the given directory is loaded and all the proofs it contains are rerun. Then, all the differences between the information stored in the session file and the new run are shown.
Nothing is shown when there is no change in the results, whether the considered goal is proved or not. When all the proof are done, a summary of what is proved or not is displayed using a tree-shape pretty print, similar to the IDE tree view after doing “Collapse proved goals”. In other words, when a goal, a theory, or a file is fully proved, the subtree is not shown.
When some proof attempts stored in the session file are obsolete, the replay is run anyway, as with the replay button in the IDE. Then, the session file will be updated if both
In other cases, you can use the IDE to update the session, or use the
option --force
described below.
The exit code is 0 if no difference was detected, 1 if there was. Other exit codes mean some failure in running the replay.
Options are:
The smoke detector tries to detect if the context is self-contradicting and, thus, that anything can be proved in this context. The smoke detector can’t be run on an outdated session and does not modify the session. It has three possible configurations:
Goal G : forall x:int. q x -> (p1 x \/ p2 x)becomes
Goal G : ~ (forall x:int. q x -> (p1 x \/ p2 x))In other words, if the smoke detector is triggered, it means that the context of the goal G is self-contradicting.
Goal G : forall x:int. q x /\ ~ (p1 x \/ p2 x)In other words, the premises of goal G are pushed in the context, so that if the smoke detector is triggered, it means that the context of the goal G and its premises are self-contradicting. It should be clear that detecting smoke in that case does not necessarily means that there is a mistake: for example, this could occur in the WP of a program with an unfeasible path.
At the end of the replay, the name of the goals that triggered the smoke detector are printed:
goal 'G', prover 'Alt-Ergo 0.93.1': Smoke detected!!!
Moreover Smoke detected (exit code 1) is printed at the end if the smoke detector has been triggered, or No smoke detected (exit code 0) otherwise.
The session command makes it possible to extract information from proof sessions on the command line, or even modify them to some extent. The invocation of this program is done under the form
why3 session <subcommand> [options] <session directories>
The available subcommands are as follows:
The first three commands do not modify the sessions, whereas the last modify them.
The command why3 session info reports various informations about the session, depending on the following specific options.
provers
and --edited-files
by the character number 0
instead of end of line \n
. That allows you to safely use
(even if the filename contains space or carriage return) the result
with other commands. For example you can count the number of proof
line in all the coq edited files in a session with:
why3 session info --edited-files vstte12_bfs --print0 | xargs -0 coqwcor you can add all the edited files in your favorite repository with:
why3 session info --edited-files --print0 vstte12_bfs.mlw | \ xargs -0 git add
The proof statistics given by option --stats
are as follows:
For example, here are the session statistics produced on the “hello proof” example of Section 1.
== Number of root goals ==
total: 3 proved: 2
== Number of sub goals ==
total: 2 proved: 1
== Goals not proved ==
+-- file ../hello_proof.why
+-- theory HelloProof
+-- goal G2
+-- transformation split_goal_right
+-- goal G2.0
== Goals proved by only one prover ==
+-- file ../hello_proof.why
+-- theory HelloProof
+-- goal G1: Alt-Ergo 0.99.1
+-- goal G2
+-- transformation split_goal_right
+-- goal G2.1: Alt-Ergo 0.99.1
+-- goal G3: Alt-Ergo 0.99.1
== Statistics per prover: number of proofs, time (minimum/maximum/average) in seconds ==
Alt-Ergo 0.99.1 : 3 0.00 0.00 0.00
Command latex produces a summary of the replay under the form of a tabular environment in LaTeX, one tabular for each theory, one per file.
The specific options are
file.theory.goal
. The
file produced is named accordingly,
e.g. file.theory.goal.tex
. This option can be given several
times to produce several tables in one run. When this option is
given at least once, the default behavior that is to produce one
table per theory is disabled.
The generated LaTeX files contain some macros that must be defined externally. Various definitions can be given to them to customize the output.
\usepackage{xcolor} \usepackage{colortbl} \usepackage{rotating} \newcommand{\provername}[1]{\cellcolor{yellow!25} \begin{sideways}\textbf{#1}~~\end{sideways}} \newcommand{\explanation}[1]{\cellcolor{yellow!13}lemma \texttt{#1}} \newcommand{\transformation}[1]{\cellcolor{yellow!13}transformation \texttt{#1}} \newcommand{\subgoal}[2]{\cellcolor{yellow!13}subgoal #2} \newcommand{\valid}[1]{\cellcolor{green!13}#1} \newcommand{\unknown}[1]{\cellcolor{red!20}#1} \newcommand{\invalid}[1]{\cellcolor{red!50}#1} \newcommand{\timeout}[1]{\cellcolor{red!20}(#1)} \newcommand{\outofmemory}[1]{\cellcolor{red!20}(#1)} \newcommand{\noresult}{\multicolumn{1}{>{\columncolor[gray]{0.8}}c|}{~}} \newcommand{\failure}{\cellcolor{red!20}failure} \newcommand{\highfailure}{\cellcolor{red!50}FAILURE}
Figure 5.3: Sample macros for the LaTeX command
Figure 5.4: LaTeX table produced for the HelloProof example (style 1)
Figure 5.5: LaTeX table produced for the HelloProof example (style 2)
Figure 5.3 suggests some definitions for these macros, while Figures 5.4 and 5.5 show the tables obtained from the HelloProof example of Section 1, respectively with style 1 and 2.
This command produces a summary of the proof session in HTML syntax. There are two styles of output: ‘table’ and ‘simpletree’. The default is ‘table’.
The file generated is named why3session.html and is written in the session directory by default (see option -o to override this default).
Why3 Proof Results for Project "hello_proof"
Theory "hello_proof.HelloProof": not fully verified
Obligations Alt-Ergo 0.99.1 Coq 8.7.1 G1 0.00 --- G2 0.00 --- split_goal_right G2.0 0.00 0.29 G2.1 0.00 --- G3 0.00 ---
Figure 5.6: HTML table produced for the HelloProof example
The style ‘table’ outputs the contents of the session as a table, similar to the LaTeX output above. Figure 5.6 is the HTML table produced for the ‘HelloProof’ example, as typically shown in a Web browser. The gray cells filled with --- just mean that the prover was not run on the corresponding goal. Green background means the result was “Valid”, other cases are in orange background. The red background for a goal means that the goal was not proved.
The style ‘simpletree’ displays the contents of the session under the
form of tree, similar to the tree view in the IDE. It uses only basic
HTML tags such as <ul>
and <li>
.
Specific options for this command are as follows.
coqdoc
command to display Coq proof
scripts. This is equivalent to --add_pp .v "coqdoc
--no-index --html -o %o %i" .htmlThe command why3 session update permits to modify the session contents, depending on the following specific options.
This tool can produce HTML pages from Why3 source code. Why3 code for theories or modules is output in preformatted HTML code. Comments are interpreted in three different ways.
Additionally, all the Why3 identifiers are typeset with links so that one can navigate through the HTML documentation, going from some identifier use to its definition.
-o
.
Some constructs are interpreted:
A CSS file style.css
suitable for rendering is generated in the
same directory as output files. This CSS style can be modified manually,
since regenerating the HTML documentation will not overwrite an existing
style.css
file.
Why3 can symbolically execute programs written using the WhyML language (extension .mlw). See also Section 7.1.
Why3 can extract programs written using the WhyML language (extension .mlw) to OCaml. See also Section 7.2.
Why3 can produce skeleton files for proof assistants that, once filled, realize the given theories. See also Section 8.2.
Why3 can give some token statistics about WhyML source files.
In this chapter, we describe the syntax and semantics of WhyML.
Blank characters are space, horizontal tab, carriage return, and line feed. Blanks separate lexemes but are otherwise ignored. Comments are enclosed by (* and *) and can be nested. Note that (*) does not start a comment.
Strings are enclosed in double quotes ("
). Double quotes can be
escaped inside strings using the backslash character (\
).
The other special sequences are \n
for line feed and \t
for horizontal tab.
In the following, strings are referred to with the non-terminal
string.
The syntax for numerical constants is given by the following rules:
Integer and real constants have arbitrary precision. Integer constants can be given in base 10, 16, 8 or 2. Real constants can be given in base 10 or 16. Notice that the exponent in hexadecimal real constants is written in base 10.
Identifiers are composed of letters, digits, underscores, and primes. The syntax distinguishes identifiers that start with a lowercase letter or an underscore (lident), identifiers that start with an uppercase letter (uident), and identifiers that start with a prime (qident, used exclusively for type variables):
alpha | ::= | a – z ∣ A – Z |
suffix | ::= | alpha ∣ digit ∣ ' ∣ _ |
lident | ::= | (a – z) suffix* ∣ _ suffix+ |
uident | ::= | (A – Z) suffix* |
qident | ::= | ' (a – z) suffix* |
Identifiers that contain a prime followed by a letter, such as int32’max, are reserved for symbols introduced by Why3 and cannot be used for user-defined symbols.
In order to refer to symbols introduced in different namespaces (scopes), we can put a dot-separated “qualifier prefix” in front of an identifier (e.g. Map.S.get). This allows us to use the symbol get from the scope Map.S without importing it in the current namespace:
All parenthesised expressions in WhyML (types, patterns, logical terms, program expressions) admit a qualifier before the opening parenthesis, e.g. Map.S.(get m i). This imports the indicated scope into the current namespace during the parsing of the expression under the qualifier. For the sake of convenience, the parentheses can be omitted when the expression itself is enclosed in parentheses, square brackets or curly braces.
Prefix and infix operators are built from characters organized in four precedence groups (op-char-1 to op-char-4), with optional primes at the end:
Infix operators from a high-numbered group bind stronger than the infix operators from a low-numbered group. For example, infix operator .*. from group 3 would have a higher precedence than infix operator ->- from group 1. Prefix operators always bind stronger than infix operators. The so-called “tight operators” are prefix operators that have even higher precedence than the juxtaposition (application) operator, allowing us to write expressions like inv !x without parentheses.
Finally, any identifier, term, formula, or expression in a WhyML source can be tagged either with a string attribute or a location:
An attribute cannot contain newlines or closing square brackets; leading and trailing spaces are ignored. A location consists of a file name in double quotes, a line number, and starting and ending character positions.
WhyML features an ML-style type system with polymorphic types, variants (sum types), and records that can have mutable fields. The syntax for type expressions is the following:
Built-in types are int (arbitrary precision integers), real (real numbers), bool, the arrow type (also called the mapping type), and the tuple types. The empty tuple type is also called the unit type and can be written as unit.
Note that the syntax for type expressions notably differs from the usual ML syntax. In particular, the type of polymorphic lists is written list ’a, and not ’a list.
Snapshot types are specific to WhyML, they denote the types of ghost values produced by pure logical functions in WhyML programs. A snapshot of an immutable type is the type itself: thus, {int} is the same as int and {list ’a} is the same as list ’a. A snapshot of a mutable type, however, represents a snapshot value which cannot be modified anymore. Thus, a snapshot array a of type {array int} can be read from (a[42] is accepted) but not written into (a[42] <- 0 is rejected). Generally speaking, a program function that expects an argument of a mutable type will accept an argument of the corresponding snapshot type as long as it is not modified by the function.
term ::= integer integer constant ∣ real real constant ∣ true ∣ false Boolean constant ∣ () empty tuple ∣ qualid qualified identifier ∣ qualifier? ( term ) term in a scope ∣ qualifier? begin term end idem ∣ tight-op term tight operator ∣ { term-field+ } record ∣ { term with term-field+ } record update ∣ term . lqualid record field access ∣ term [ term ] '* collection access ∣ term [ term <- term ] '* collection update ∣ term [ term .. term ] '* collection slice ∣ term [ term .. ] '* right-open slice ∣ term [ .. term ] '* left-open slice ∣ term term+ application ∣ prefix-op term prefix operator ∣ term infix-op-4 term infix operator 4 ∣ term infix-op-3 term infix operator 3 ∣ term infix-op-2 term infix operator 2 ∣ term at uident past value ∣ old term initial value ∣ term infix-op-1 term infix operator 1 ∣ ... continued in Fig. 6.2 term-field ::= lqualid = term ; field = value qualid ::= qualifier? (lident-ext ∣ uident) qualified identifier lident-ext ::= lident lowercase identifier ∣ ( ident-op ) operator identifier ∣ ( ident-op ) (_ ∣ ') alpha suffix* associated identifier ident-op ::= infix-op-1 infix operator 1 ∣ infix-op-2 infix operator 2 ∣ infix-op-3 infix operator 3 ∣ infix-op-4 infix operator 4 ∣ prefix-op _ prefix operator ∣ tight-op _? tight operator ∣ [ ] '* collection access ∣ [ <- ] '* collection update ∣ [ ] '* <- in-place update ∣ [ .. ] '* collection slice ∣ [ _ .. ] '* right-open slice ∣ [ .. _ ] '* left-open slice
Figure 6.1: WhyML terms (part I).
term ::= ... see Fig. 6.1 ∣ not term negation ∣ term /\ term conjunction ∣ term && term asymmetric conjunction ∣ term \/ term disjunction ∣ term || term asymmetric disjunction ∣ term by term proof indication ∣ term so term consequence indication ∣ term -> term implication ∣ term <-> term equivalence ∣ term : type type cast ∣ attribute+ term attributes ∣ term (, term)+ tuple ∣ quantifier quant-vars triggers? . term quantifier ∣ ... continued in Fig. 6.3 quantifier ::= forall ∣ exists quant-vars ::= quant-cast (, quant-cast)* quant-cast ::= binder+ (: type)? binder ::= _ ∣ bound-var bound-var ::= lident attribute* triggers ::= [ trigger (| trigger)* ] trigger ::= term (, term)*
Figure 6.2: WhyML terms (part II).
A significant part of a typical WhyML source file is occupied by non-executable logical content intended for specification and proof: function contracts, assertions, definitions of logical functions and predicates, axioms, lemmas, etc.
Logical expressions are called terms. Boolean terms are called formulas. Internally, Why3 distinguishes the proper formulas (produced by predicate symbols, propositional connectives and quantifiers) and the terms of type bool (produced by Boolean variables and logical functions that return bool). However, this distinction is not enforced on the syntactical level, and Why3 will perform the necessary conversions behind the scenes.
The syntax of WhyML terms is given in Figures 6.1-6.3. The constructions are listed in the order of decreasing precedence. For example, as was mentioned above, tight operators have the highest precedence of all operators, so that -p.x denotes the negation of the record field p.x, whereas !p.x denotes the field x of a record stored in the reference p.
An operator in parentheses acts as an identifier referring to that operator, for example, in a definition. To distinguish between prefix and infix operators, an underscore symbol is appended at the end: for example, (-) refers to the binary subtraction and (-_) to the unary negation. Tight operators cannot be used as infix operators, and thus do not require disambiguation.
In addition to prefix and infix operators, WhyML supports several mixfix bracket operators to manipulate various collection types: dictionaries, arrays, sequences, etc. Bracket operators do not have any predefined meaning and may be used to denote access and update operations for various user-defined collection types. We can introduce multiple bracket operations in the same scope by disambiguating them with primes after the closing bracket: for example, a[i] may denote array access and s[i]’ sequence access. Notice that the in-place update operator a[i] <- v cannot be used inside logical terms: all effectful operations are restricted to program expressions. To represent the result of a collection update, we should use a pure logical update operator a[i <- v] instead.
WhyML supports “associated” names for operators, obtained by adding a suffix after the parenthesised operator name. For example, an axiom that represents the specification of the infix operator (+) may be called (+)’spec or (+)_spec. As with normal identifiers, names with a letter after a prime, such as (+)’spec, can only be introduced by Why3, and not by the user in a WhyML source.
The at and old operators are used inside postconditions and assertions to refer to the value of a mutable program variable at some past moment of execution (see the next section for details). These operators have higher precedence than the infix operators from group 1 (infix-op-1): old i > j is parsed as (old i) > j and not as old (i > j).
Infix operators from groups 2-4 are left-associative. Infix operators from group 1 are non-associative and can be chained. For example, the term 0 <= i < j < length a is parsed as the conjunction of three inequalities 0 <= i, i < j, and j < length a.
As with normal identifiers, we can put a qualifier over a parenthesised operator, e.g. Map.S.([]) m i. Also, as noted above, a qualifier can be put over a parenthesised term, and the parentheses can be omitted if the term is a record or a record update.
The propositional connectives in WhyML formulas are listed in Figure 6.2. The non-standard connectives — asymmetric conjunction (&&), asymmetric disjunction (||), proof indication (by), and consequence indication (so) — are used to control the goal-splitting transformations of Why3 and provide integrated proofs for WhyML assertions, postconditions, lemmas, etc. The semantics of these connectives follows the rules below:
For example, full splitting of the goal (A by (exists x. B so C)) && D produces four subgoals: exists x. B (the premise is verified), forall x. B -> C (the premise justifies the conclusion), (exists x. B /\ C) -> A (the proof justifies the affirmation), and finally, A -> D (the proof of A is discarded and A is used to prove D).
The behaviour of the splitting transformations is further controlled by attributes [@stop_split] and [@case_split]. Consult Section 9.5.5 for details.
Among the propositional connectives, not has the highest precedence, && has the same precedence as /\ (weaker than negation), || has the same precedence as \/ (weaker than conjunction), by, so, ->, and <-> all have the same precedence (weaker than disjunction). All binary connectives except equivalence are right-associative. Equivalence is non-associative and is chained instead: A <-> B <-> C is transformed into a conjunction of A <-> B and B <-> C. To reduce ambiguity, WhyML forbids to place a non-parenthesised implication at the right-hand side of an equivalence: A <-> B -> C is rejected.
term ::= ... see Fig. 6.1 and 6.2 ∣ if term then term else term conditional ∣ match term with term-case+ end pattern matching ∣ let pattern = term in term let-binding ∣ let symbol param+ = term in term mapping definition ∣ fun param+ -> term unnamed mapping term-case ::= | pattern -> term pattern ::= binder variable or ‘_’ ∣ () empty tuple ∣ { (lqualid = pattern ;)+ } record pattern ∣ uqualid pattern* constructor ∣ ghost pattern ghost sub-pattern ∣ pattern as ghost? bound-var named sub-pattern ∣ pattern , pattern tuple pattern ∣ pattern | pattern “or” pattern ∣ qualifier? ( pattern ) pattern in a scope symbol ::= lident-ext attribute* user-defined symbol param ::= type-arg unnamed typed ∣ binder (un)named untyped ∣ ( ghost? type ) unnamed typed ∣ ( ghost? binder ) (un)named untyped ∣ ( ghost? binder+ : type ) multi-variable typed
Figure 6.3: WhyML terms (part III).
In Figure 6.3, we find the more advanced term constructions: conditionals, let-bindings, pattern matching, and local function definitions, either via the let-in construction or the fun keyword. The pure logical functions defined in this way are called mappings; they are first-class values of “arrow” type τ1 -> τ2.
The patterns are similar to those of OCaml, though the when clauses and numerical constants are not supported. Unlike in OCaml, as binds stronger than the comma: in the pattern (p1,p2 as x), variable x is bound to the value matched by pattern p2. Also notice the closing end after the match-with term. A let-in construction with a non-trivial pattern is translated as a match-with term with a single branch.
Inside logical terms, pattern matching must be exhaustive: WhyML rejects a term like let Some x = o in …, where o is a variable of an option type. In program expressions, non-exhaustive pattern matching is accepted and a proof obligation is generated to show that the values not covered cannot occur in execution.
The syntax of parameters in user-defined operations—first-class mappings, top-level logical functions and predicates, and program functions—is rather flexible in WhyML. Like in OCaml, the user can specify the name of a parameter without its type and let the type be inferred from the definition. Unlike in OCaml, the user can also specify the type of the parameter without giving its name. This is convenient when the symbol declaration does not provide the actual definition or specification of the symbol, and thus only the type signature is of relevance. For example, one can declare an abstract binary function that adds an element to a set simply by writing function add ’a (set ’a) : set ’a. A standalone non-qualified lowercase identifier without attributes is treated as a type name when the definition is not provided, and as a parameter name otherwise.
Ghost patterns, ghost variables after as, and ghost parameters in function definitions are only used in program code, and not allowed in logical terms.
The syntax of program expressions is given in Figures 6.4-6.5. As before, the constructions are listed in the order of decreasing precedence. The rules for tight, prefix, infix, and bracket operators are the same as for logical terms. In particular, the infix operators from group 1 can be chained. Notice that binary operators && and || denote here the usual lazy conjunction and disjunction, respectively.
expr ::= integer integer constant ∣ real real constant ∣ true ∣ false Boolean constant ∣ () empty tuple ∣ qualid identifier in a scope ∣ qualifier? ( expr ) expression in a scope ∣ qualifier? begin expr end idem ∣ tight-op expr tight operator ∣ { (lqualid = expr ;)+ } record ∣ { expr with (lqualid = expr ;)+ } record update ∣ expr . lqualid record field access ∣ expr [ expr ] '* collection access ∣ expr [ expr <- expr ] '* collection update ∣ expr [ expr .. expr ] '* collection slice ∣ expr [ expr .. ] '* right-open slice ∣ expr [ .. expr ] '* left-open slice ∣ expr expr+ application ∣ prefix-op expr prefix operator ∣ expr infix-op-4 expr infix operator 4 ∣ expr infix-op-3 expr infix operator 3 ∣ expr infix-op-2 expr infix operator 2 ∣ expr infix-op-1 expr infix operator 1 ∣ not expr negation ∣ expr && expr lazy conjunction ∣ expr || expr lazy disjunction ∣ expr : type type cast ∣ attribute+ expr attributes ∣ ghost expr ghost expression ∣ expr (, expr)+ tuple ∣ expr <- expr assignment ∣ ... continued in Fig. 6.5
Figure 6.4: WhyML program expressions (part I).
Keyword ghost marks the expression as ghost code added for verification purposes. Ghost code is removed from the final code intended for execution, and thus cannot affect the computation of the program results nor the content of the observable memory.
Assignment updates in place a mutable record field or an element of a collection. The former can be done simultaneously on a tuple of values: x.f, y.g <- a, b. The latter form, a[i] <- v, amounts to a call of the ternary bracket operator ([]<-) and cannot be used in a multiple assignment.
expr ::= ... see Fig. 6.4 ∣ expr spec+ added specification ∣ if expr then expr (else expr)? conditional ∣ match expr with (| pattern -> expr)+ end pattern matching ∣ qualifier? begin spec+ expr end abstract block ∣ expr ; expr sequence ∣ let pattern = expr in expr let-binding ∣ let fun-defn in expr local function ∣ let rec fun-defn (with fun-defn)* in expr recursive function ∣ fun param+ spec* -> spec* expr unnamed function ∣ any result spec* arbitrary value fun-defn ::= fun-head spec* = spec* expr function definition fun-head ::= ghost? kind? symbol param+ (: result)? function header kind ::= function ∣ predicate ∣ lemma function kind result ::= ret-type ∣ ( ret-type (, ret-type)* ) ∣ ( ret-name (, ret-name)* ) ret-type ::= ghost? type unnamed result ret-name ::= ghost? binder : type named result spec ::= requires { term } pre-condition ∣ ensures { term } post-condition ∣ returns { (| pattern -> term)+ } post-condition ∣ raises { (| pattern -> term)+ } exceptional post-c. ∣ raises { uqualid (, uqualid)* } raised exceptions ∣ reads { lqualid (, lqualid)* } external reads ∣ writes { path (, path)* } memory writes ∣ alias { alias (, alias)* } memory aliases ∣ variant { variant (, variant)* } termination variant ∣ diverges may not terminate ∣ (reads ∣ writes ∣ alias) { } empty effect path ::= lqualid (. lqualid)* v.field1.field2 alias ::= path with path arg1 with result variant ::= term (with lqualid)? variant + WF-order
Figure 6.5: WhyML program expressions (part II).
The syntax for terms is given in Figure 6.1. The various constructs have the following priorities and associativities, from lowest to greatest priority:
construct | associativity |
if then else / let in | – |
label | – |
cast | – |
infix-op level 1 | left |
infix-op level 2 | left |
infix-op level 3 | left |
infix-op level 4 | left |
prefix-op | – |
function application | left |
brackets / ternary brackets | – |
bang-op | – |
Note the curryfied syntax for function application, though partial application is not allowed (rejected at typing).
The syntax for formulas is given Figure 6.6. The various constructs have the following priorities and associativities, from lowest to greatest priority:
construct | associativity |
if then else / let in | – |
label | – |
-> / <-> | right |
by / so | right |
\/ / || | right |
/\ / && | right |
not | – |
infix level 1 | left |
infix level 2 | left |
infix level 3 | left |
infix level 4 | left |
prefix | – |
Note that infix symbols of level 1 include equality (=) and disequality (<>).
Figure 6.6: Syntax for formulas.
Notice that there are two symbols for the conjunction: /\
and &&
, and similarly for disjunction. They are logically
equivalent, but may be treated slightly differently by some
transformations. For instance, split transforms the goal
A /\ B
into subgoals A
and B
, whereas it transforms
A && B
into subgoals A
and A -> B
. Similarly, it
transforms not (A || B)
into subgoals not A
and
not ((not A) /\ B)
.
The by/so connectives are proof indications. They are
logically equivalent to their first argument, but may affect the result
of some transformations. For instance, the split_goal
transformations interpret those connectives as introduction of logical cuts
(see 9.5.5 for details).
The syntax for theories is given on Figure 6.7 and 6.8.
Figure 6.7: Syntax for theories (part 1).
Figure 6.8: Syntax for theories (part 2).
TO BE COMPLETED
TO BE COMPLETED
A declaration of the form type r = < range a b > defines a type that projects into the integer range [a,b]. Note that in order to make such a declaration the theory int.Int must be imported.
Why3 let you cast an integer literal in a range type (e.g. (42:r)) and will check at typing that the literal is in range. Defining such a range type r automatically introduces the following:
function r'int r : int constant r'maxInt : int constant r'minInt : int |
The function r’int projects a term of type r to its integer value. The two constants represent the high bound and low bound of the range respectively.
Unless specified otherwise with the meta "keep:literal" on r, the transformation eliminate_literal introduces an axiom
axiom r'axiom : forall i:r. r'minInt <= r'int i <= r'maxInt |
and replaces all casts of the form (42:r) with a constant and an axiom as in:
constant rliteral7 : r axiom rliteral7_axiom : r'int rliteral7 = 42 |
This type is used in the standard library in the theories bv.BV8, bv.BV16, bv.BV32, bv.BV64.
A declaration of the form type f = < float eb sb > defines a type of floating-point numbers as specified by the IEEE-754 standard [8]. Here the literal eb represents the number of bits in the exponent and the literal sb the number of bits in the significand (including the hidden bit). Note that in order to make such a declaration the theory real.Real must be imported.
Why3 let you cast a real literal in a float type (e.g. (0.5:f)) and will check at typing that the literal is representable in the format. Note that Why3 do not implicitly round a real literal when casting to a float type, it refuses the cast if the literal is not representable.
Defining such a type f automatically introduces the following:
predicate f'isFinite f function f'real f : real constant f'eb : int constant f'sb : int |
As specified by the IEEE standard, float formats includes infinite values and also a special NaN value (Not-a-Number) to represent results of undefined operations such as 0/0. The predicate f’isFinite indicates whether its argument is neither infinite nor NaN. The function f’real projects a finite term of type f to its real value, its result is not specified for non finite terms.
Unless specified otherwise with the meta "keep:literal" on f, the transformation eliminate_literal will introduce an axiom
axiom f'axiom : forall x:f. f'isFinite x -> -. max_real <=. f'real x <=. max_real |
where max_real is the value of the biggest finite float in the specified format. The transformation also replaces all casts of the form (0.5:f) with a constant and an axiom as in:
constant fliteral42 : f axiom fliteral42_axiom : f'real fliteral42 = 0.5 /\ f'isFinite fliteral42 |
This type is used in the standard library in the theories ieee_float.Float32 and ieee_float.Float64.
A Why3 input file is a (possibly empty) list of theories.
The syntax for specification clauses in programs is given in Figure 6.9.
Figure 6.9: Specification clauses in programs.
Within specifications, terms are extended with new constructs
old
and at
:
Within a postcondition, old
t refers to the value of term t
in the prestate. Within the scope of a code mark L,
the term at
t '
L refers to the value of term t at the program
point corresponding to L.
The syntax for program expressions is given in Figure 6.10 and Figure 6.11.
Figure 6.10: Syntax for program expressions (part 1).
expr ::= ... see Fig. 6.4 ∣ expr spec+ added specification ∣ if expr then expr (else expr)? conditional ∣ match expr with (| pattern -> expr)+ end pattern matching ∣ qualifier? begin spec+ expr end abstract block ∣ expr ; expr sequence ∣ let pattern = expr in expr let-binding ∣ let fun-defn in expr local function ∣ let rec fun-defn (with fun-defn)* in expr recursive function ∣ fun param+ spec* -> spec* expr unnamed function ∣ any result spec* arbitrary value fun-defn ::= fun-head spec* = spec* expr function definition fun-head ::= ghost? kind? symbol param+ (: result)? function header kind ::= function ∣ predicate ∣ lemma function kind result ::= ret-type ∣ ( ret-type (, ret-type)* ) ∣ ( ret-name (, ret-name)* ) ret-type ::= ghost? type unnamed result ret-name ::= ghost? binder : type named result spec ::= requires { term } pre-condition ∣ ensures { term } post-condition ∣ returns { (| pattern -> term)+ } post-condition ∣ raises { (| pattern -> term)+ } exceptional post-c. ∣ raises { uqualid (, uqualid)* } raised exceptions ∣ reads { lqualid (, lqualid)* } external reads ∣ writes { path (, path)* } memory writes ∣ alias { alias (, alias)* } memory aliases ∣ variant { variant (, variant)* } termination variant ∣ diverges may not terminate ∣ (reads ∣ writes ∣ alias) { } empty effect path ::= lqualid (. lqualid)* v.field1.field2 alias ::= path with path arg1 with result variant ::= term (with lqualid)? variant + WF-order
Figure 6.11: Syntax for program expressions (part 2).
In applications, arguments are evaluated from right to left.
This includes applications of infix operators, with the only exception of
lazy operators &&
and ||
that evaluate from left to
right, lazily.
The syntax for modules is given in Figure 6.12.
Figure 6.12: Syntax for modules.
Any declaration which is accepted in a theory is also accepted in a module. Additionally, modules can introduce record types with mutable fields and declarations which are specific to programs (global variables, functions, exceptions).
A WhyML input file is a (possibly empty) list of theories and modules.
A theory defined in a WhyML file can only be used within that file. If a theory is supposed to be reused from other files, be they Why3 or WhyML files, it should be defined in a Why3 file.
The Why3 standard library provides general-purpose modules, to be used in logic and/or programs. It can be browsed on-line at http://why3.lri.fr/stdlib/. Each file contains one or several modules. To use or clone a module M from file file, use the syntax file.M, since file is available in Why3’s default load path. For instance, the module of integers and the module of references are imported as follows:
use import int.Int use import ref.Ref |
A sub-directory mach/ provides various modules to model machine arithmetic. For instance, the module of 63-bit integers and the module of arrays indexed by 63-bit integers are imported as follows:
use import mach.int.Int63 use import mach.array.Array63 |
In particular, the types and operations from these modules are mapped to native OCaml’s types and operations when Why3 code is extracted to OCaml (see Section 7.2).
This chapter shows how WhyML code can be executed, either by being interpreted or compiled to some existing programming language.
Let us consider the program of Section 2.2 that computes the maximum and the sum of an array of integers. Let us assume it is contained in a file maxsum.mlw.
To test function max_sum, we can introduce a WhyML test function in module MaxAndSum
let test () = let n = 10 in let a = make n 0 in a[0] <- 9; a[1] <- 5; a[2] <- 0; a[3] <- 2; a[4] <- 7; a[5] <- 3; a[6] <- 2; a[7] <- 1; a[8] <- 10; a[9] <- 6; max_sum a n |
and then we use the execute command to interpret this function, as follows:
> why3 execute maxsum.mlw MaxAndSum.test Execution of MaxAndSum.test (): type: (int, int) result: (45, 10) globals:
We get the expected output, namely the pair (45, 10).
An alternative to interpretation is to compile WhyML to OCaml. We do so using the extract command, as follows:
> why3 extract -D ocaml64 maxsum.mlw -o max_sum.ml
The extract command requires the name of a driver, which indicates
how theories/modules from the Why3 standard library are translated to
OCaml. Here we assume a 64-bit architecture and thus we pass
ocaml64. We also specify an output file using option
-o
, namely max_sum.ml.
After this command, the file max_sum.ml contains an OCaml
code for function max_sum.
To compile it, we create a file main.ml
containing a call to max_sum, e.g.,
let a = Array.map Z.of_int [| 9; 5; 0; 2; 7; 3; 2; 1; 10; 6 |] let s, m = Max_sum.max_sum a (Z.of_int 10) let () = Format.printf "sum=%s, max=%s@." (Z.to_string s) (Z.to_string m) |
It is convenient to use ocamlbuild to compile and link both files max_sum.ml and main.ml:
> ocamlbuild -pkg zarith main.native
Since Why3’s type int is translated to OCaml arbitrary precision integers using the ZArith library, we have to pass option -pkg zarith to ocamlbuild. In order to get extracted code that uses OCaml’s native integers instead, one has to use Why3’s types for 63-bit integers from libraries mach.int.Int63 and mach.array.Array63.
The extract command accepts three different targets for extraction: a WhyML file, a module, or a symbol (function, type, exception). To extract all the symbols from every module of a file named f.mlw, one should write
> why3 extract -D <driver> f.mlw
To extract only the symbols from module M of file f.mlw, one should write
> why3 extract -D <driver> -L <dir> f.M
To extract only the symbol s (a function, a type, or an exception) from module M of file f.mlw, one should write
> why3 extract -D <driver> -L <dir> f.M.s
Note the use of -L <dir>, for both extraction of a module and a symbol, in order to state the location of file f.mlw.
The following options can be added to the extraction command line:
We illustrate different ways of using the extract command through some examples. Consider the program of Section 2.6. If we are only interested in extracting function enqueue, we can proceed as follows:
> why3 extract -D ocaml64 -L . aqueue.AmortizedQueue.enqueue -o aqueue.ml
Here we assume that file aqueue.mlw contains this program, and that we invoke extract from the directory where this file is stored. File aqueue.ml now contains the following OCaml code:
let enqueue (x: 'a) (q: 'a queue) : 'a queue = create (q.front) (q.lenf) (x :: (q.rear)) (Z.add (q.lenr) (Z.of_string "1")) |
Choosing a function symbol as the entry point of extraction allows us to focus only on specific parts of the program. However, the generated code cannot be type-checked by the OCaml compiler, as it depends on function create and on type ’a queue, whose definitions are not given. In order to obtain a complete OCaml implementation, we can perform a recursive extraction:
> why3 extract --recursive -D ocaml64 -L . \ aqueue.AmortizedQueue.enqueue -o aqueue.ml
This updates the contents of file aqueue.ml as follows:
type 'a queue = { front: 'a list; lenf: Z.t; rear: 'a list; lenr: Z.t; } let create (f: 'a list) (lf: Z.t) (r: 'a list) (lr: Z.t) : 'a queue = if Z.geq lf lr then { front = f; lenf = lf; rear = r; lenr = lr } else let f1 = List.append f (List.rev r) in { front = f1; lenf = Z.add lf lr; rear = []; lenr = (Z.of_string "0") } let enqueue (x: 'a) (q: 'a queue) : 'a queue = create (q.front) (q.lenf) (x :: (q.rear)) (Z.add (q.lenr) (Z.of_string "1")) |
This new version of the code is now accepted by the OCaml compiler (provided the ZArith library is available, as above).
Several OCaml drivers can be specified on the command line, using option -D several times. In particular, one can provide a custom driver to map some symbols of a Why3 development to existing OCaml code. Suppose for instance we have a file file.mlw containing a proof parameterized with some type elt and some binary function f:
module M type elt val f (x y: elt) : elt let double (x: elt) : elt = f x x ... |
When it comes to extract this module to OCaml, we may want to instantiate type elt with OCaml’s type int and function f with OCaml’s addition. For this purpose, we provide the following in a file mydriver.drv:
module file.M syntax type elt "int" syntax val f "%1 + %2" end |
OCaml fragments to be substituted for Why3 symbols are given as
arbitrary strings, where %1
, %2
, etc., will be replaced
with actual arguments.
Here is the extraction command line and its output:
> why3 extract -D ocaml64 -D mydriver.drv -L . file.M let double (x: int) : int = x + x ...
When using such custom drivers, it is not possible to pass Why3 file names on the command line; one has to specify module names to be extracted, as done above.
Instead of calling an automated theorem prover to discharge a goal, Why3 offers the possibility to call an interactive theorem prover instead. In that case, the interaction is decomposed into two distinct phases:
An example of such an interaction is given in the tutorial section 1.2.
Some proof assistants offer more than one possible editor, e.g. a choice between the use of a dedicated editor and the use of the Emacs editor and the ProofGeneral mode. Selection of the preferred mode can be made in why3ide preferences, under the “Editors” tab.
Given a Why3 theory, one can use a proof assistant to make a realization of this theory, that is to provide definitions for some of its uninterpreted symbols and proofs for some of its axioms. This way, one can show the consistency of an axiomatized theory and/or make a connection to an existing library (of the proof assistant) to ease some proofs.
Generating the skeleton for a theory is done by passing to the realize command a driver suitable for realizations, the names of the theories to realize, and a target directory.
why3 realize -D path/to/drivers/prover-realize.drv -T env_path.theory_name -o path/to/target/dir/
The theory is looked into the files from the environment, e.g. the standard library. If the theory is stored in a different location, option -L should be used.
The name of the generated file is inferred from the theory name. If the target directory already contains a file with the same name, Why3 extracts all the parts that it assumes to be user-edited and merges them in the generated file.
Note that Why3 does not track dependencies between realizations and theories, so a realization will become outdated if the corresponding theory is modified. It is up to the user to handle such dependencies, for instance using a Makefile.
If a theory has been realized, the Why3 printer for the corresponding prover will no longer output declarations for that theory but instead simply put a directive to load the realization. In order to tell the printer that a given theory is realized, one has to add a meta declaration in the corresponding theory section of the driver.
theory env_path.theory_name meta "realized_theory" "env_path.theory_name", "optional_naming" end
The first parameter is the theory name for Why3. The second parameter, if not empty, provides a name to be used inside generated scripts to point to the realization, in case the default name is not suitable for the interactive prover.
While modifying an existing driver file might be sufficient for local
use, it does not scale well when the realizations are to be shipped to
other users. Instead, one should create two additional files: a
configuration file that indicates how to modify paths, provers, and
editors, and a driver file that contains only the needed
meta "realized_theory"
declarations. The configuration file should be as
follows.
[main] loadpath="path/to/theories" [prover_modifiers] name="Coq" option="-R path/to/vo/files Logical_directory" driver="path/to/file/with/meta.drv" [editor_modifiers coqide] option="-R path/to/vo/files Logical_directory" [editor_modifiers proofgeneral-coq] option="--eval \"(setq coq-load-path (cons '(\\\"path/to/vo/files\\\" \ \\\"Logical_directory\\\") coq-load-path))\""
This configuration file can be passed to Why3 thanks to the
--extra-config
option.
This section describes the content of the Coq files generated by Why3 for both proof obligations and theory realizations. When reading a Coq script, Why3 is guided by the presence of empty lines to split the script, so the user should refrain from removing empty lines around generated blocks or adding empty lines inside them.
(* This file is generated by ... *)
.
Parameter
. Axioms are assumed with the Axiom
directive. When regenerating a script, Why3 assumes that all such
symbols have been generated by a previous run. As a consequence,
the user should not introduce new symbols with these two
directives, as they would be lost.
(* Why3 assumption *)
.
This comment should not be removed; otherwise Why3 will assume
that the definition is a user-defined block.
(* Why3 goal *)
. The user is supposed to
fill the script after the statement. Why3 assumes that the
user-made part extends up to Qed
, Admitted
,
Save
, or Defined
, whichever comes first. In the
case of definitions, the original statement can be replaced by
a Notation
directive, in order to ease the usage of
predefined symbols. Why3 also recognizes Variable
and Hypothesis
and preserves them; they should be used in
conjunction with Coq’s Section
mechanism to realize
theories that still need some abstract symbols and axioms.
Why3 preserves any block from the script that does not fall into one of the previous categories. Such blocks can be used to import other libraries than the ones from the prelude. They can also be used to state and prove auxiliary lemmas. Why3 tries to preserve the position of these user-defined blocks relatively to the generated ones.
Currently, the parser for Coq scripts is rather naive and does not know
much about comments. For instance, Why3 can easily be confused by
some terminating directive like Qed
that would be present in a
comment.
When using Isabelle from Why3, files generated from Why3 theories and goals are stored in a dedicated XML format. Those files should not be edited. Instead, the proofs must be completed in a file with the same name and extension .thy. This is the file that is opened when using “Edit” action in why3 ide.
You need version Isabelle2017 or Isabelle2018. Former versions are not supported. We assume below that your version is 2018, please replace 2018 by 2017 otherwise.
Isabelle must be installed before compiling Why3. After compilation and installation of Why3, you must manually add the path
<Why3 lib dir>/isabelle
into either the user file
.isabelle/Isabelle2018/etc/components
or the system-wide file
<Isabelle install dir>/etc/components
The most convenient way to call Isabelle for discharging a Why3 goal is to start the Isabelle/jedit interface in server mode. In this mode, one must start the server once, before launching why3 ide, using
isabelle why3_jedit
Then, inside a why3 ide session, any use of “Edit” will transfer the file to the already opened instance of jEdit. When the proof is completed, the user must send back the edited proof to why3 ide by closing the opened buffer, typically by hitting Ctrl-w.
Starting from Isabelle version 2018, Why3 is able to exploit the
server features of Isabelle to speed up the processing of proofs in
batch mode, e.g. when replaying them from within Why3 IDE. Currently,
when replaying proofs using the isabelle why3
tool, an Isabelle
process including a rather heavyweight Java/Scala and PolyML runtime
environment has to be started, and a suitable heap image has to be
loaded for each proof obligation, which can take several seconds. To
avoid this overhead, an Isabelle server and a suitable session can be
started once, and then isabelle why3
can just connect to it and
request the server to process theories. In order to allow a tool such
as Why3 IDE to use the Isabelle server, it has to be started via the
wrapper tool isabelle use_server
. For example, to process the proofs
in examples/logic/genealogy using Why3 IDE and the Isabelle server, do
the following:
isabelle server &
isabelle use_server why3 ide genealogy
Realizations must be designed in some .thy as follows. The realization file corresponding to some Why3 file f.why should have the following form.
theory Why3_f imports Why3_Setup begin section {* realization of theory T *} why3_open "f/T.xml" why3_vc <some lemma> <proof> why3_vc <some other lemma> by proof [...] why3_end
See directory lib/isabelle for examples.
You need version 6.0.
When a PVS file is regenerated, the old version is split into chunks,
according to blank lines. Chunks corresponding to Why3 declarations
are identified with a comment starting with % Why3
, e.g.
% Why3 f f(x: int) : int
Other chunks are considered to be user PVS declarations.
Thus a comment such as % Why3 f
must not be removed;
otherwise, there will be two
declarations for f in the next version of the file (one being
regenerated and another one considered to be a user-edited chunk).
The user is allowed to perform the following actions on a PVS realization:
Why3 makes some effort to merge new declarations with old ones and with user chunks. If it happens that some chunks could not be merged, they are appended at the end of the file, in comments.
The proof session state is stored in an XML file named <dir>/why3session.xml, where <dir> is the directory of the project. The XML file follows the DTD given in share/why3session.dtd and reproduced below.
<!ELEMENT why3session (prover*, file*)> <!ATTLIST why3session shape_version CDATA #IMPLIED> <!ELEMENT prover EMPTY> <!ATTLIST prover id CDATA #REQUIRED> <!ATTLIST prover name CDATA #REQUIRED> <!ATTLIST prover version CDATA #REQUIRED> <!ATTLIST prover alternative CDATA #IMPLIED> <!ATTLIST prover timelimit CDATA #IMPLIED> <!ATTLIST prover memlimit CDATA #IMPLIED> <!ATTLIST prover steplimit CDATA #IMPLIED> <!ELEMENT file (path*, theory*)> <!ATTLIST file name CDATA #IMPLIED> <!ATTLIST file verified CDATA #IMPLIED> <!ATTLIST file proved CDATA #IMPLIED> <!ELEMENT path EMPTY> <!ATTLIST path name CDATA #REQUIRED> <!ELEMENT theory (label*,goal*)> <!ATTLIST theory name CDATA #REQUIRED> <!ATTLIST theory verified CDATA #IMPLIED> <!ATTLIST theory proved CDATA #IMPLIED> <!ELEMENT goal (label*, proof*, transf*)> <!ATTLIST goal name CDATA #REQUIRED> <!ATTLIST goal expl CDATA #IMPLIED> <!ATTLIST goal sum CDATA #IMPLIED> <!ATTLIST goal shape CDATA #IMPLIED> <!ATTLIST goal proved CDATA #IMPLIED> <!ELEMENT proof (result|undone|internalfailure|unedited)> <!ATTLIST proof prover CDATA #REQUIRED> <!ATTLIST proof timelimit CDATA #IMPLIED> <!ATTLIST proof memlimit CDATA #IMPLIED> <!ATTLIST proof steplimit CDATA #IMPLIED> <!ATTLIST proof edited CDATA #IMPLIED> <!ATTLIST proof obsolete CDATA #IMPLIED> <!ELEMENT result EMPTY> <!ATTLIST result status (valid|invalid|unknown|timeout|outofmemory|steplimitexceeded|failure|highfailure) #REQUIRED> <!ATTLIST result time CDATA #IMPLIED> <!ATTLIST result steps CDATA #IMPLIED> <!ELEMENT undone EMPTY> <!ELEMENT unedited EMPTY> <!ELEMENT internalfailure EMPTY> <!ATTLIST internalfailure reason CDATA #REQUIRED> <!ELEMENT transf (goal*)> <!ATTLIST transf name CDATA #REQUIRED> <!ATTLIST transf proved CDATA #IMPLIED> <!ATTLIST transf arg1 CDATA #IMPLIED> <!ATTLIST transf arg2 CDATA #IMPLIED> <!ATTLIST transf arg3 CDATA #IMPLIED> <!ATTLIST transf arg4 CDATA #IMPLIED> <!ELEMENT label EMPTY> <!ATTLIST label name CDATA #REQUIRED> |
The data configuration for the automatic detection of
installed provers is stored in the file
provers-detection-data.conf typically located in directory
/usr/local/share/why3
after installation. The content of this
file is reproduced below.
[ATP alt-ergo] name = "Alt-Ergo" exec = "alt-ergo" exec = "alt-ergo-2.3.0" exec = "alt-ergo-2.2.0" exec = "alt-ergo-2.1.0" exec = "alt-ergo-2.0.0" version_switch = "-version" version_regexp = "^\\([0-9.]+\\)$" version_ok = "2.3.0" version_ok = "2.2.0" version_ok = "2.1.0" version_ok = "2.0.0" version_bad = "1.30" version_bad = "1.01" version_bad = "0.99.1" version_bad = "0.95.2" command = "%e -timelimit %t %f" command_steps = "%e -steps-bound %S %f" driver = "alt_ergo" editor = "altgr-ergo" use_at_auto_level = 1 # CVC4 version >= 1.6, with counterexamples [ATP cvc4-ce] name = "CVC4" alternative = "counterexamples" exec = "cvc4" exec = "cvc4-1.6" exec = "cvc4-1.7" version_switch = "--version" version_regexp = "This is CVC4 version \\([^ \n\r]+\\)" version_ok = "1.6" version_ok = "1.7" driver = "cvc4_16_counterexample" --random-seed=42 is not needed as soon as --random-freq=0.0 by default # to try: --inst-when=full-last-call command = "%e --tlimit-per=%t000 --lang=smt2 %f" command_steps = "%e --stats --rlimit=%S --lang=smt2 %f" # CVC4 version >= 1.6 [ATP cvc4] name = "CVC4" exec = "cvc4" exec = "cvc4-1.6" exec = "cvc4-1.7" version_switch = "--version" version_regexp = "This is CVC4 version \\([^ \n\r]+\\)" version_ok = "1.6" version_ok = "1.7" driver = "cvc4_16" --random-seed=42 is not needed as soon as --random-freq=0.0 by default # to try: --inst-when=full-last-call command = "%e --tlimit=%t000 --lang=smt2 %f" command_steps = "%e --stats --rlimit=%S --lang=smt2 %f" use_at_auto_level = 1 # CVC4 version = 1.5, with counterexamples [ATP cvc4-ce] name = "CVC4" alternative = "counterexamples" exec = "cvc4" exec = "cvc4-1.5" version_switch = "--version" version_regexp = "This is CVC4 version \\([^ \n\r]+\\)" version_ok = "1.5" driver = "cvc4_15_counterexample" --random-seed=42 is not needed as soon as --random-freq=0.0 by default # to try: --inst-when=full-last-call command = "%e --tlimit-per=%t000 --lang=smt2 %f" command_steps = "%e --stats --rlimit=%S --lang=smt2 %f" # CVC4 version 1.5 [ATP cvc4] name = "CVC4" exec = "cvc4" exec = "cvc4-1.5" version_switch = "--version" version_regexp = "This is CVC4 version \\([^ \n\r]+\\)" version_ok = "1.5" driver = "cvc4_15" --random-seed=42 is not needed as soon as --random-freq=0.0 by default # to try: --inst-when=full-last-call command = "%e --tlimit=%t000 --lang=smt2 %f" command_steps = "%e --stats --rlimit=%S --lang=smt2 %f" use_at_auto_level = 1 # CVC4 version 1.4, using SMTLIB fixed-size bitvectors [ATP cvc4] name = "CVC4" exec = "cvc4" exec = "cvc4-1.4" version_switch = "--version" version_regexp = "This is CVC4 version \\([^ \n\r]+\\)" version_old = "1.4" driver = "cvc4_14" --random-seed=42 is not needed as soon as --random-freq=0.0 by default # to try: --inst-when=full-last-call --rlimit=%S : cvc4 1.4 DOES NOT accept -1 as argument # cvc4 1.4 does not print steps used in --stats anyway command = "%e --tlimit=%t000 --lang=smt2 %f" use_at_auto_level = 1 # CVC4 version 1.4, not using SMTLIB bitvectors [ATP cvc4] name = "CVC4" alternative = "noBV" exec = "cvc4" exec = "cvc4-1.4" version_switch = "--version" version_regexp = "This is CVC4 version \\([^ \n\r]+\\)" version_old = "1.4" driver = "cvc4" --random-seed=42 is not needed as soon as --random-freq=0.0 by default # to try: --inst-when=full-last-call --rlimit=%S : cvc4 1.4 DOES NOT accept -1 as argument # cvc4 1.4 does not print steps used in --stats anyway command = "%e --tlimit=%t000 --lang=smt2 %f" # CVC4 version 1.0 to 1.3 [ATP cvc4] name = "CVC4" exec = "cvc4" exec = "cvc4-1.3" exec = "cvc4-1.2" exec = "cvc4-1.1" exec = "cvc4-1.0" version_switch = "--version" version_regexp = "This is CVC4 version \\([^ \n\r]+\\)" version_old = "1.3" version_old = "1.2" version_old = "1.1" version_old = "1.0" driver = "cvc4" command = "%e --lang=smt2 %f" # Psyche version 2.x [ATP psyche] name = "Psyche" exec = "psyche" exec = "psyche-2.02" version_switch = "-version" version_regexp = "\\([^ \n\r]+\\)" version_ok = "2.0" driver = "psyche" command = "%e -gplugin dpll_wl %f" # CVC3 versions 2.4.x [ATP cvc3] name = "CVC3" exec = "cvc3" exec = "cvc3-2.4.1" exec = "cvc3-2.4" version_switch = "-version" version_regexp = "This is CVC3 version \\([^ \n]+\\)" version_ok = "2.4.1" version_old = "2.4" # the -timeout option is unreliable in CVC3 2.4.1 command = "%e -seed 42 %f" driver = "cvc3" # CVC3 versions 2.x [ATP cvc3] name = "CVC3" exec = "cvc3" exec = "cvc3-2.2" exec = "cvc3-2.1" version_switch = "-version" version_regexp = "This is CVC3 version \\([^ \n]+\\)" version_old = "2.2" version_old = "2.1" command = "%e -seed 42 -timeout %t %f" driver = "cvc3" [ATP yices] name = "Yices" exec = "yices" exec = "yices-1.0.38" version_switch = "--version" version_regexp = "\\([^ \n]+\\)" version_ok = "1.0.38" version_old = "^1\.0\.3[0-7]$" version_old = "^1\.0\.2[5-9]$" version_old = "^1\.0\.2[0-4]$" version_old = "^1\.0\.1\.*$" command = "%e" driver = "yices" [ATP yices-smt2] name = "Yices" exec = "yices-smt2" exec = "yices-smt2-2.3.0" version_switch = "--version" version_regexp = "^Yices \\([^ \n]+\\)$" version_ok = "2.3.0" command = "%e" driver = "yices-smt2" [ATP eprover] name = "Eprover" exec = "eprover" exec = "eprover-2.0" exec = "eprover-1.9.1" exec = "eprover-1.9" exec = "eprover-1.8" exec = "eprover-1.7" exec = "eprover-1.6" exec = "eprover-1.5" exec = "eprover-1.4" version_switch = "--version" version_regexp = "E \\([-0-9.]+\\) [^\n]+" version_ok = "2.0" version_old = "1.9.1-001" version_old = "1.9" version_old = "1.8-001" version_old = "1.7" version_old = "1.6" version_old = "1.5" version_old = "1.4" command = "%e -s -R -xAuto -tAuto --cpu-limit=%t --tstp-in %f" driver = "eprover" use_at_auto_level = 2 [ATP gappa] name = "Gappa" exec = "gappa" exec = "gappa-1.3.2" exec = "gappa-1.3.0" exec = "gappa-1.2.2" exec = "gappa-1.2.0" exec = "gappa-1.1.1" exec = "gappa-1.1.0" exec = "gappa-1.0.0" exec = "gappa-0.16.1" exec = "gappa-0.14.1" version_switch = "--version" version_regexp = "Gappa \\([^ \n]*\\)" version_ok = "^1\.[0-3]\..+$" version_old = "^0\.1[1-8]\..+$" command = "%e -Eprecision=70" driver = "gappa" [ATP mathsat] name = "MathSAT5" exec = "mathsat" exec = "mathsat-5.2.2" version_switch = "-version" version_regexp = "MathSAT5 version \\([^ \n]+\\)" version_ok = "5.2.2" command = "%e -input=smt2 -model -random_seed=80" driver = "mathsat" [ATP simplify] name = "Simplify" exec = "Simplify" exec = "simplify" exec = "Simplify-1.5.4" exec = "Simplify-1.5.5" version_switch = "-version" version_regexp = "Simplify version \\([^ \n,]+\\)" version_old = "1.5.5" version_old = "1.5.4" command = "%e %f" driver = "simplify" [ATP metis] name = "Metis" exec = "metis" version_switch = "-v" version_regexp = "metis \\([^ \n,]+\\)" version_ok = "2.3" command = "%e --time-limit %t %f" driver = "metis" [ATP metitarski] name = "MetiTarski" exec = "metit" exec = "metit-2.4" exec = "metit-2.2" version_switch = "-v" version_regexp = "MetiTarski \\([^ \n,]+\\)" version_ok = "2.4" version_old = "2.2" command = "%e --time %t %f" driver = "metitarski" [ATP polypaver] name = "PolyPaver" exec = "polypaver" exec = "polypaver-0.3" version_switch = "--version" version_regexp = "PolyPaver \\([0-9.]+\\) (c)" version_ok = "0.3" command = "%e -d 2 -m 10 --time=%t %f" driver = "polypaver" [ATP spass] name = "Spass" exec = "SPASS" exec = "SPASS-3.7" version_switch = " | grep 'SPASS V'" version_regexp = "SPASS V \\([^ \n\t]+\\)" version_ok = "3.7" command = "%e -TPTP -PGiven=0 -PProblem=0 -TimeLimit=%t %f" driver = "spass" use_at_auto_level = 2 [ATP spass] name = "Spass" exec = "SPASS" exec = "SPASS-3.8ds" version_switch = " | grep 'SPASS[^ \\n\\t]* V'" version_regexp = "SPASS[^ \n\t]* V \\([^ \n\t]+\\)" version_ok = "3.8ds" command = "%e -Isabelle=1 -PGiven=0 -TimeLimit=%t %f" driver = "spass_types" use_at_auto_level = 2 [ATP vampire] name = "Vampire" exec = "vampire" exec = "vampire-0.6" version_switch = "--version" version_regexp = "Vampire \\([0-9.]+\\)" command = "%e -t %t" driver = "vampire" version_ok = "0.6" [ATP princess] name = "Princess" exec = "princess" exec = "princess-2015-12-07" # version_switch = "-h" # version_regexp = "(CASC version \\([0-9-]+\\))" version_regexp = "(release \\([0-9-]+\\))" command = "%e -timeout=%t %f" driver = "princess" # version_ok = "2013-05-13" version_ok = "2015-12-07" [ATP beagle] name = "Beagle" exec = "beagle" exec = "beagle-0.4.1" # version_switch = "-h" version_regexp = "version \\([0-9.]+\\)" command = "%e %f" driver = "beagle" version_ok = "0.4.1" [ATP verit] name = "veriT" exec = "veriT" exec = "veriT-201410" version_switch = "--version" version_regexp = "version \\([^ \n\r]+\\)" command = "%e --disable-print-success %f" driver = "verit" version_ok = "201410" [ATP verit] name = "veriT" exec = "veriT" exec = "veriT-201310" version_switch = "--version" version_regexp = "version \\([^ \n\r]+\\)" command = "%e --disable-print-success --enable-simp \ --enable-unit-simp --enable-simp-sym --enable-unit-subst-simp --enable-bclause %f" driver = "verit" version_old = "201310" # Z3 >= 4.6.0, with counterexamples and incremental usage [ATP z3-ce] name = "Z3" alternative = "counterexamples" exec = "z3" exec = "z3-4.8.6" exec = "z3-4.8.5" exec = "z3-4.8.4" exec = "z3-4.8.3" exec = "z3-4.8.1" exec = "z3-4.7.1" exec = "z3-4.6.0" exec = "z3-4.5.0" exec = "z3-4.4.1" exec = "z3-4.4.0" version_switch = "-version" version_regexp = "Z3 version \\([^ \n\r]+\\)" version_ok = "4.8.6" version_ok = "4.8.5" version_ok = "4.8.4" version_ok = "4.8.3" version_ok = "4.8.1" version_ok = "4.7.1" version_ok = "4.6.0" version_ok = "4.5.0" version_old = "4.4.1" version_old = "4.4.0" driver = "z3_440_counterexample" -t sets the time limit per query command = "%e -smt2 -t:%t000 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 %f" command_steps = "%e -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 memory_max_alloc_count=%S %f" # Z3 >= 4.4.0, with BV support [ATP z3] name = "Z3" exec = "z3" exec = "z3-4.8.6" exec = "z3-4.8.5" exec = "z3-4.8.4" exec = "z3-4.8.3" exec = "z3-4.8.1" exec = "z3-4.7.1" exec = "z3-4.6.0" exec = "z3-4.5.0" exec = "z3-4.4.1" exec = "z3-4.4.0" version_switch = "-version" version_regexp = "Z3 version \\([^ \n\r]+\\)" version_ok = "4.8.6" version_ok = "4.8.5" version_ok = "4.8.4" version_ok = "4.8.3" version_ok = "4.8.1" version_ok = "4.7.1" version_ok = "4.6.0" version_ok = "4.5.0" version_old = "4.4.1" version_old = "4.4.0" driver = "z3_440" command = "%e -smt2 -T:%t sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 %f" command_steps = "%e -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 memory_max_alloc_count=%S %f" use_at_auto_level = 1 # Z3 >= 4.4.0, without BV support [ATP z3-nobv] name = "Z3" alternative = "noBV" exec = "z3" exec = "z3-4.8.6" exec = "z3-4.8.5" exec = "z3-4.8.4" exec = "z3-4.8.3" exec = "z3-4.8.1" exec = "z3-4.7.1" exec = "z3-4.6.0" exec = "z3-4.5.0" exec = "z3-4.4.1" exec = "z3-4.4.0" version_switch = "-version" version_regexp = "Z3 version \\([^ \n\r]+\\)" version_ok = "4.8.6" version_ok = "4.8.5" version_ok = "4.8.4" version_ok = "4.8.3" version_ok = "4.8.1" version_ok = "4.7.1" version_ok = "4.6.0" version_ok = "4.5.0" version_old = "4.4.1" version_old = "4.4.0" driver = "z3_432" command = "%e -smt2 -T:%t sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 %f" command_steps = "%e -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 memory_max_alloc_count=%S %f" # Z3 4.3.2 does not support option global option -rs anymore. # use settings given by "z3 -p" instead # Z3 4.3.2 supports Datatypes [ATP z3] name = "Z3" exec = "z3-4.3.2" version_switch = "-version" version_regexp = "Z3 version \\([^ \n\r]+\\)" version_old = "4.3.2" driver = "z3_432" command = "%e -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 %f" command_steps = "%e -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 memory_max_alloc_count=%S %f" [ATP z3] name = "Z3" exec = "z3" exec = "z3-4.3.1" exec = "z3-4.3.0" exec = "z3-4.2" exec = "z3-4.1.2" exec = "z3-4.1.1" exec = "z3-4.0" version_switch = "-version" version_regexp = "Z3 version \\([^ \n\r]+\\)" version_old = "4.3.1" version_old = "4.3.0" version_old = "4.2" version_old = "4.1.2" version_old = "4.1.1" version_old = "4.0" driver = "z3" command = "%e -smt2 -rs:42 %f" [ATP z3] name = "Z3" exec = "z3" exec = "z3-3.2" exec = "z3-3.1" exec = "z3-3.0" version_switch = "-version" version_regexp = "Z3 version \\([^ \n\r]+\\)" version_old = "3.2" version_old = "3.1" version_old = "3.0" driver = "z3" # the -T is unreliable in Z3 3.2 command = "%e -smt2 -rs:42 %f" [ATP z3] name = "Z3" exec = "z3" exec = "z3-2.19" exec = "z3-2.18" exec = "z3-2.17" exec = "z3-2.16" version_switch = "-version" version_regexp = "Z3 version \\([^ \n\r]+\\)" version_old = "^2\.2.+$" version_old = "^2\.1[6-9]$" driver = "z3" command = "%e -smt2 -rs:42 \ PHASE_SELECTION=0 \ RESTART_STRATEGY=0 \ RESTART_FACTOR=1.5 \ QI_EAGER_THRESHOLD=100 \ ARITH_RANDOM_INITIAL_VALUE=true \ SORT_AND_OR=false \ CASE_SPLIT=3 \ DELAY_UNITS=true \ DELAY_UNITS_THRESHOLD=16 \ %f" #Other Parameters given by Nikolaj Bjorner #BV_REFLECT=true #arith? #MODEL_PARTIAL=true #MODEL_VALUE_COMPLETION=false #MODEL_HIDE_UNUSED_PARTITIONS=false #MODEL_V1=true #ASYNC_COMMANDS=false #NNF_SK_HACK=true [ATP z3] name = "Z3" exec = "z3" exec = "z3-2.2" exec = "z3-2.1" exec = "z3-1.3" version_switch = "-version" version_regexp = "Z3 version \\([^ \n\r]+\\)" version_old = "^2\.1[0-5]$" version_old = "^2\.[0-9]$" version_old = "1.3" command = "%e -smt %f" driver = "z3_smtv1" [ATP zenon] name = "Zenon" exec = "zenon" exec = "zenon-0.8.0" exec = "zenon-0.7.1" version_switch = "-v" version_regexp = "zenon version \\([^ \n\t]+\\)" version_ok = "0.8.0" version_ok = "0.7.1" command = "%e -p0 -itptp -max-size %mM -max-time %ts %f" driver = "zenon" [ATP zenon_modulo] name = "Zenon Modulo" exec = "zenon_modulo" version_switch = "-v" version_regexp = "zenon_modulo version \\([0-9.]+\\)" version_ok = "0.4.1" command = "%e -p0 -itptp -max-size %mM -max-time %ts %f" driver = "zenon_modulo" [ATP iprover] name = "iProver" exec = "iprover" exec = "iprover-0.8.1" version_switch = " | grep iProver" version_regexp = "iProver v\\([^ \n\t]+\\)" version_ok = "0.8.1" command = "%e --fof true --out_options none \ --time_out_virtual %t --clausifier /usr/bin/env --clausifier_options \ \"eprover --cnf --tstp-format \" %f" driver = "iprover" [ATP mathematica] name = "Mathematica" exec = "math" version_switch = "-run \"Exit[]\"" version_regexp = "Mathematica \\([0-9.]+\\)" version_ok = "9.0" version_ok = "8.0" version_ok = "7.0" command = "%e -noprompt" driver = "mathematica" [ITP coq] name = "Coq" support_library = "%l/coq/version" exec = "coqtop" version_switch = "-v" version_regexp = "The Coq Proof Assistant, version \\([^ \n]+\\)" version_ok = "^8\.9\.[0-1]$" version_ok = "^8\.8\.[0-2]$" version_ok = "^8\.7\.[0-2]$" version_ok = "8.6.1" version_ok = "8.6" version_old = "^8\.5pl[1-3]$" version_old = "8.5" command = "%e -batch -R %l/coq Why3 -l %f" driver = "coq" editor = "coqide" [ITP pvs] name = "PVS" support_library = "%l/pvs/version" exec = "pvs" version_switch = "-version" version_regexp = "PVS Version \\([^ \n]+\\)" version_ok = "6.0" version_bad = "^[0-5]\..+$" command = "%l/why3-call-pvs %l/pvs proveit -f %f" driver = "pvs" in_place = true editor = "pvs" [ITP isabelle] name = "Isabelle" exec = "isabelle" version_switch = "version" version_regexp = "Isabelle\\([0-9]+\\(-[0-9]+\\)?\\)" version_ok = "2018" version_bad = "2017" version_bad = "2016-1" command = "%e why3 -b %f" driver = "isabelle2018" in_place = true editor = "isabelle-jedit" [ITP isabelle] name = "Isabelle" exec = "isabelle" version_switch = "version" version_regexp = "Isabelle\\([0-9]+\\(-[0-9]+\\)?\\)" version_ok = "2017" version_bad = "2018" version_bad = "2016-1" command = "%e why3 -b %f" driver = "isabelle2017" in_place = true editor = "isabelle-jedit" [editor pvs] name = "PVS" command = "%l/why3-call-pvs %l pvs %f" [editor coqide] name = "CoqIDE" command = "coqide -R %l/coq Why3 %f" [editor proofgeneral-coq] name = "Emacs/ProofGeneral/Coq" command = "emacs --eval \"(setq coq-load-path '((\\\"%l/coq\\\" \\\"Why3\\\")))\" %f" [editor isabelle-jedit] name = "Isabelle/jEdit" command = "isabelle why3 -i %f" [editor altgr-ergo] name = "AltGr-Ergo" command = "altgr-ergo %f" [shortcut shortcut1] name="Alt-Ergo" shortcut="altergo" |
One can use a custom configuration file. The Why3 tools look for it in the following order:
If none of these files exist, a built-in default configuration is used.
A section begins with a header inside square brackets and ends at the beginning of the next section. The header of a section can be a single identifier, e.g. [main], or it can be composed by a family name and a single family argument, e.g. [prover alt-ergo].
Sections contain associations key=value. A value is either an integer (e.g. -555), a boolean (true, false), or a string (e.g. "emacs"). Some specific keys can be attributed multiple values and are thus allowed to occur several times inside a given section. In that case, the relative order of these associations matters.
Drivers for external provers are readable files from directory drivers. Experimented users can modify them to change the way the external provers are called, in particular which transformations are applied to goals.
[TO BE COMPLETED LATER]
This section documents the available transformations. We first describe the most important ones, and then we provide a quick documentation of the others, first the non-splitting ones, e.g. those which produce exactly one goal as result, and the others which produce any number of goals.
Notice that the set of available transformations in your own installation is given by
why3 --list-transforms
Those transformations generally amount to replace some applications of function or predicate symbols with its definition.
function f x_1 ... x_n = (g e_1 ... e_k) predicate p x_1 ... x_n = (q e_1 ... e_k) |
goal G: forall l: list 'a. length l >= 0 |
goal G : forall l:list 'a. match l with | Nil -> length l >= 0 | Cons a l1 -> length l1 >= 0 -> length l >= 0 end |
[@induction]
attribute can be used to
force induction over one particular variable, e.g. with
goal G: forall l1 [@induction] l2 l3: list 'a. l1 ++ (l2 ++ l3) = (l1 ++ l2) ++ l3 |
l1
. If this attribute is attached to
several variables, a lexicographic induction is performed on these
variables, from left to right.These transformations simplify the goal by applying several kinds of simplification, described below. The transformations differ only by the kind of rules they apply:
The kinds of simplification are as follows.
true
and the transformations thus does not produce any sub-goal.
For example, a goal
like 6*7=42
is solved by those transformations.
inline_goal
. Transformation
compute_in_goal
unfolds all definitions, including recursive ones.
For compute_specified
, the user can enable unfolding of a specific
logic symbol by attaching the meta rewrite_def
to the symbol.
function sqr (x:int) : int = x * x meta "rewrite_def" function sqr |
axiom a: forall ... t1 = t2 |
axiom a: forall ... f1 <-> f2 |
meta "rewrite" prop a |
Instead of using a meta, it is possible to declare an axiom as a
rewrite rule by adding the [@rewrite]
attribute on the axiom name or
on the axiom itself, e.g.:
axiom a [@rewrite]: forall ... t1 = t2 lemma b: [@rewrite] forall ... f1 <-> f2 |
The second form allows some form of local rewriting, e.g.
lemma l: forall x y. ([@rewrite] x = y) -> f x = f y |
can be proved by introduce_premises
followed by compute_specified
.
The computations performed by these transformations can take an arbitrarily large number of steps, or even not terminate. For this reason, the number of steps is bounded by a maximal value, which is set by default to 1000. This value can be increased by another meta, e.g.
meta "compute_max_steps" 1_000_000 |
When this upper limit is reached, a warning is issued, and the partly-reduced goal is returned as the result of the transformation.
Select_eq
of theory map.Map
.
function f : ... = ... g ... with g : ... = e |
function g : ... = e function f : ... = ... g ... |
forall x, x = t -> P(x) |
P(t) |
The transformation treats specially asymmetric and
by/so connectives. Asymmetric conjunction
A && B
in goal position is handled as syntactic sugar for
A /\ (A -> B)
. The conclusion of the first subgoal can then
be used to prove the second one.
Asymmetric disjunction A || B
in hypothesis position is handled as
syntactic sugar for A \/ ((not A) /\ B)
.
In particular, a case analysis on such hypothesis would give the negation of
the first hypothesis in the second case.
The by connective is treated as a proof indication. In
hypothesis position, A by B
is treated as if it were
syntactic sugar for its regular interpretation A
. In goal
position, it is treated as if B
was an intermediate step for
proving A
. A by B
is then replaced by B
and the
transformation also generates a side-condition subgoal B -> A
representing the logical cut.
Although splitting stops at disjunctive points like symmetric disjunction and left-hand sides of implications, the occurrences of the by connective are not restricted. For instance:
goal G : (A by B) && C |
goal G1 : B goal G2 : A -> C goal G3 : B -> A (* side-condition *) |
goal G : (A by B) \/ (C by D) |
goal G1 : B \/ D goal G2 : B -> A (* side-condition *) goal G3 : D -> C (* side-condition *) |
goal G : (A by B) || (C by D) |
goal G1 : B || D goal G2 : B -> A (* side-condition *) goal G3 : B || (D -> C) (* side-condition *) |
goal G : exists x. P x by x = 42 |
goal G1 : exists x. x = 42 goal G2 : forall x. x = 42 -> P x (* side-condition *) |
The so connective plays a similar role in hypothesis position, as it serves as a consequence indication. In goal position, A so B
is treated as if it were syntactic sugar for its regular interpretation A
. In hypothesis position, it is treated as if both A
and B
were true because B
is a consequence of A
. A so B
is replaced by A /\ B
and the transformation also generates a side-condition subgoal A -> B
corresponding to the consequence relation between formula.
As with the by connective, occurrences of so are unrestricted. For instance:
goal G : (((A so B) \/ C) -> D) && E |
goal G1 : ((A /\ B) \/ C) -> D goal G2 : (A \/ C -> D) -> E goal G3 : A -> B (* side-condition *) |
goal G : A by exists x. P x so Q x so R x by T x (* reads: A by (exists x. P x so (Q x so (R x by T x))) *) |
goal G1 : exists x. P x goal G2 : forall x. P x -> Q x (* side-condition *) goal G3 : forall x. P x -> Q x -> T x (* side-condition *) goal G4 : forall x. P x -> Q x -> T x -> R x (* side-condition *) goal G5 : (exists x. P x /\ Q x /\ R x) -> A (* side-condition *) |
A
: There exists a x
for which P
holds. Then,
for that witness Q
and R
also holds. The last one holds
because T
holds as well. And from those three conditions on
x
, we can deduce A
.
The transformations in the split family can be controlled by using attributes on formulas.
The [@stop_split]
attribute can be used to block the splitting of a
formula. The attribute is removed after blocking, so applying the
transformation a second time will split the formula. This is can be
used to decompose the splitting process in several steps. Also, if a
formula with this attribute is found in non-goal position, its
by/so proof indication will be erased by the
transformation. In a sense, formulas tagged by [@stop_split]
are
handled as if they were local lemmas.
The [@case_split]
attribute can be used to force case analysis on hypotheses.
For instance, applying split_goal on
goal G : ([@case_split] A \/ B) -> C |
generates the subgoals
goal G1 : A -> C goal G2 : B -> C |
Without the attribute, the transformation does nothing because undesired case analysis may easily lead to an exponential blow-up.
Note that the precise behavior of splitting transformations in presence of
the [@case_split]
attribute is not yet specified
and is likely to change in future versions.
As seen in Section 5.3, the IDE provides a few buttons that trigger the run of simple proof strategies on the selected goals. Proof strategies can be defined using a basic assembly-style language, and put into the Why3 configuration file. The commands of this basic language are:
To examplify this basic programming language, we give below the
default strategies that are attached to the default buttons of the
IDE, assuming that the provers Alt-Ergo 1.30, CVC4 1.5 and Z3 4.5.0
were detected by the why3 config --detect
command
t split_goal_wp exit
c Z3,4.5.0, 1 1000 c Alt-Ergo,1.30, 1 1000 c CVC4,1.5, 1 1000The three provers are tried for a time limit of 1 second and memory limit of 1 Gb, each in turn. This is a perfect strategy for a first attempt to discharge a new goal.
start: c Z3,4.5.0, 1 1000 c Alt-Ergo,1.30, 1 1000 c CVC4,1.5, 1 1000 t split_goal_wp start c Z3,4.5.0, 10 4000 c Alt-Ergo,1.30, 10 4000 c CVC4,1.5, 10 4000The three provers are first tried for a time limit of 1 second and memory limit of 1 Gb, each in turn. If none of them succeed, a split is attempted. If the split works then the same strategy is retried on each sub-goals. If the split does not succeed, the provers are tried again with a larger limits.
start: c Z3,4.5.0, 1 1000 c Eprover,2.0, 1 1000 c Spass,3.7, 1 1000 c Alt-Ergo,1.30, 1 1000 c CVC4,1.5, 1 1000 t split_goal_wp start c Z3,4.5.0, 5 2000 c Eprover,2.0, 5 2000 c Spass,3.7, 5 2000 c Alt-Ergo,1.30, 5 2000 c CVC4,1.5, 5 2000 t introduce_premises afterintro afterintro: t inline_goal afterinline g trylongertime afterinline: t split_goal_wp start trylongertime: c Z3,4.5.0, 30 4000 c Eprover,2.0, 30 4000 c Spass,3.7, 30 4000 c Alt-Ergo,1.30, 30 4000 c CVC4,1.5, 30 4000Notice that now 5 provers are used. The provers are first tried for a time limit of 1 second and memory limit of 1 Gb, each in turn. If none of them succeed, a split is attempted. If the split works then the same strategy is retried on each sub-goals. If the split does not succeed, the prover are tried again with limits of 5 s and 2 Gb. If all fail, we attempt the transformation of introduction of premises in the context, followed by an inlining of the definitions in the goals. We then attempt a split again, if the split succeeds, we restart from the beginning, if it fails then provers are tried again with 30s and 4 Gb.
Part III |
Version 1.2 introduces a simplified syntax for reference variables, to avoid the somehow heavy OCaml syntax using bang character. In short, this is syntactic sugar summarized in the following table. An example using this new syntax is in examples/isqrt.mlw
auto-dereference syntax | desugared to |
let &x = ... in | let (x: ref ...) = ... in |
f x; | f x.contents; |
x <- ... | x.contents <- ... |
let ref x = ... | let &x = ref ... |
Notice that:
&
marker adds the typing constraint (x: ref ...)
let/val ref
and let/val &
are allowed
That syntactic sugar is further extended to pattern matching, function parameters and reference passing as follows.
auto-dereference syntax | desugared to | ||||||||||||||
match e with (x,&y) -> y end | match e with (x,(y: ref ...)) -> y.contents end | ||||||||||||||
|
| ||||||||||||||
let incr (ref x: int) ... | let incr (&x: ref int) ... |
The type annotation is not required. Let-functions with such formal parameters also prevent the actual argument from auto-dereferencing when used in logic. Pure logical symbols cannot be declared with such parameters.
Auto-dereference suppression does not work in the middle of a relation
chain: in 0 < x :< 17
, x
will be dereferenced even if (:<)
expects a
ref-parameter on the left.
Finally, that syntactic sugar applies to the caller side:
auto-dereference syntax | desugared to | ||||||
|
|
The &
marker can only be attached to a variable. Works in logic.
Ref-binders and &
-binders in variable declarations, patterns,
and function parameters do not require importing ref.Ref
.
Any example that does not use references inside data structures
can be rewritten by using ref-binders, without importing ref.Ref
.
Explicit use of type symbol "ref", program function "ref",
or field "contents" require importing ref.Ref
or why3.Ref.Ref
.
Operations (:=)
and (!)
require importing ref.Ref
.
Operation (:=)
is fully subsumed by direct assignment (<-)
.
The syntax of WhyML programs changed in release 1.0. The table in Figure A.1 summarizes the changes.
Note also that logical symbols can no longer be used in non-ghost code; in particular, there is no polymorphic equality in programs anymore, so equality functions must be declared/defined on a per-type basis (already done for type int in the standard library). The CHANGES.md file describes other potential sources of incompatibility.
version 0.88 version 1.0 function f ... let function f ... if called in programs ’L: label L in at x ’L x at L \x. e fun x -> e use HighOrd nothing, not needed anymore HighOrd.pred ty ty -> bool type t model ... type t = abstract ... abstract e ensures { Q } begin ensures { Q } e end namespace N scope N use import M use M "attribute" [@attribute] meta M prop P meta M lemma P or meta M axiom P or meta M goal P loop ... end while true do ... done type ... invariant { ... self.foo ... } type ... invariant { ... foo ... }
Figure A.1: Syntax changes from version 0.88 to version 1.0
Here are a few more semantic changes
diverges
clause to that
function’s contract. It was also possible to disable that warning by
adding the label "W:diverges:N"
to the function’s
name. Version 1.00 of Why3 is more aggressively requiring the user
to prove the termination of functions which are not given the
diverges
clause, and the previous warning is now an
error. The possibility of proving only partial correctness is now
given on a more fine-grain basis: any expression for which one wants
to prove partial correctness only, must by annotated with the
attribute [@vc:divergent]
.In other words, if one was using the following structure in Why3 0.xx:
let f "W:diverges:N" <parameters> <contract> = <body> |
then in 1.00 it should be written as
let f <parameters> <contract> = [@vc:divergent] <body> |
any
construct
in Why3 0.xx was introducing an arbitrary value satisfying the
associated post-condition. In some sense, this construct was
introducing some form of an axiom stating that such a value
exists. In Why3 1.00, it is now mandatory to prove the existence of
such a value, and a VC is generated for that purpose.To obtain the effect of the former semantics of the any
construct, one should use instead a local val
function. In other words, if one was using the following structure in Why3 0.xx:
any t ensures { P } |
then in 1.00 it should be written as
val x:t ensures { P } in x |
The syntax of WhyML programs changed in release 0.80. The table in Figure A.2 summarizes the changes.
version 0.73 version 0.80 type t = {| field : int |} type t = { field : int } {| field = 5 |} { field = 5 } use import module M use import M let rec f (x:int) (y:int) : t
variant { t } with rel =
{ P }
e
{ Q }
| Exc1 -> { R1 }
| Exc2 n -> { R2 }let rec f (x:int) (y:int) : t
variant { t with rel }
requires { P }
ensures { Q }
raises { Exc1 -> R1
| Exc2 n -> R2 }
= eval f (x:int) (y:int) :
{ P }
t
writes a b
{ Q }
| Exc1 -> { R1 }
| Exc2 n -> { R2 }val f (x:int) (y:int) : t
requires { P }
writes { a, b }
ensures { Q }
raises { Exc1 -> R1
| Exc2 n -> R2 }val f : x:int -> y:int ->
{ P }
t
writes a b
{ Q }
| Exc1 -> { R1 }
| Exc2 n -> { R2 }val f (x y:int) : t
requires { P }
writes { a, b }
ensures { Q }
raises { Exc1 -> R1
| Exc2 n -> R2 }abstract e { Q } abstract e ensures { Q }
Figure A.2: Syntax changes from version 0.73 to version 0.80
The main new features with respect to Why 2.xx are the following.
|
|
This document was translated from LATEX by HEVEA.