This chapter describes the input syntax, and informally gives its semantics, illustrated by examples.
A Why3 text contains a list of theories. A theory is a list of declarations. Declarations introduce new types, functions and predicates, state axioms, lemmas and goals. These declarations can be directly written in the theory or taken from existing theories. The base logic of Why3 is first-order logic with polymorphic types.
The code below is an example of Why3 input text, containing three theories.
|theory List type list 'a = Nil | Cons 'a (list 'a) end theory Length use import List use import int.Int function length (l : list 'a) : int = match l with | Nil -> 0 | Cons _ r -> 1 + length r end lemma Length_nonnegative : forall l:list 'a. length l >= 0 end theory Sorted use import List use import int.Int inductive sorted (list int) = | Sorted_Nil : sorted Nil | Sorted_One : forall x:int. sorted (Cons x Nil) | Sorted_Two : forall x y : int, l : list int. x <= y -> sorted (Cons y l) -> sorted (Cons x (Cons y l)) end|
The first theory, List, declares a new algebraic type for polymorphic lists, list ’a. As in ML, ’a stands for a type variable. The type list ’a has two constructors, Nil and Cons. Both constructors can be used as usual function symbols, respectively of type list ’a and ’a × list ’a → list ’a. We deliberately make this theory that short, for reasons which will be discussed later.
The next theory, Length, introduces the notion of list length. The use import List command indicates that this new theory may refer to symbols from theory List. These symbols are accessible in a qualified form, such as List.list or List.Cons. The import qualifier additionally allows us to use them without qualification.
Similarly, the next command use import int.Int adds to our context the theory int.Int from the standard library. The prefix int indicates the file in the standard library containing theory Int. Theories referred to without prefix either appear earlier in the current file, e.g. List, or are predefined.
The next declaration defines a recursive function, length, which computes the length of a list. The function and predicate keywords are used to introduce function and predicate symbols, respectively. Why3 checks every recursive, or mutually recursive, definition for termination. Basically, we require a lexicographic and structural descent for every recursive call for some reordering of arguments. Notice that matching must be exhaustive and that every match expression must be terminated by the end keyword.
Despite using higher-order “curried” syntax, Why3 does not permit partial application: function and predicate arities must be respected.
The last declaration in theory Length is a lemma stating that the length of a list is non-negative.
The third theory, Sorted, demonstrates the definition of an inductive predicate. Every such definition is a list of clauses: universally closed implications where the consequent is an instance of the defined predicate. Moreover, the defined predicate may only occur in positive positions in the antecedent. For example, a clause:
|| Sorted_Bad : forall x y : int, l : list int. (sorted (Cons y l) -> y > x) -> sorted (Cons x (Cons y l))|
would not be allowed. This positivity condition assures the logical soundness of an inductive definition.
Note that the type signature of
sorted predicate does not
include the name of a parameter (see l in the definition
of length): it is unused and therefore optional.
In the previous section we have seen how a theory can reuse the declarations of another theory, coming either from the same input text or from the library. Another way to referring to a theory is by “cloning”. A clone declaration constructs a local copy of the cloned theory, possibly instantiating some of its abstract (i.e. declared but not defined) symbols.
Consider the continued example below. We write an abstract theory of partial orders, declaring an abstract type t and an abstract binary predicate <=. Notice that an infix operation must be enclosed in parentheses when used outside a term. We also specify three axioms of a partial order.
|theory Order type t predicate (<=) t t axiom Le_refl : forall x : t. x <= x axiom Le_asym : forall x y : t. x <= y -> y <= x -> x = y axiom Le_trans: forall x y z : t. x <= y -> y <= z -> x <= z end theory SortedGen use import List clone import Order as O inductive sorted (l : list t) = | Sorted_Nil : sorted Nil | Sorted_One : forall x:t. sorted (Cons x Nil) | Sorted_Two : forall x y : t, l : list t. x <= y -> sorted (Cons y l) -> sorted (Cons x (Cons y l)) end theory SortedIntList use import int.Int clone SortedGen with type O.t = int, predicate O.(<=) = (<=) end|
There is little value in use’ing such a theory: this would constrain us to stay with the type t. However, we can construct an instance of theory Order for any suitable type and predicate. Moreover, we can build some further abstract theories using order, and then instantiate those theories.
Consider theory SortedGen. In the beginning, we use the earlier theory List. Then we make a simple clone theory Order. This is pretty much equivalent to copy-pasting every declaration from Order to SortedGen; the only difference is that Why3 traces the history of cloning and transformations and drivers often make use of it (see Section 10.4).
Notice an important difference between use and clone. If we use a theory, say List, twice (directly or indirectly: e.g. by making use of both Length and Sorted), there is no duplication: there is still only one type of lists and a unique pair of constructors. On the contrary, when we clone a theory, we create a local copy of every cloned declaration, and the newly created symbols, despite having the same names, are different from their originals.
Returning to the example, we finish theory SortedGen with a familiar definition of predicate sorted; this time we use the abstract order on the values of type t.
Now, we can instantiate theory SortedGen to any ordered type, without having to retype the definition of sorted. For example, theory SortedIntList makes clone of SortedGen (i.e. copies its declarations) substituting type int for type O.t of SortedGen and the default order on integers for predicate O.(<=). Why3 will control that the result of cloning is well-typed.
Several remarks ought to be made here. First of all, why should we clone theory Order in SortedGen if we make no instantiation? Couldn’t we write use import Order as O instead? The answer is no, we could not. When cloning a theory, we only can instantiate the symbols declared locally in this theory, not the symbols imported with use. Therefore, we create a local copy of Order in SortedGen to be able to instantiate t and (<=) later.
Secondly, when we instantiate an abstract symbol, its declaration is not copied from the theory being cloned. Thus, we will not create a second declaration of type int in SortedIntList.
The mechanism of cloning bears some resemblance to modules and functors of ML-like languages. Unlike those languages, Why3 makes no distinction between modules and module signatures, modules and functors. Any Why3 theory can be use’d directly or instantiated in any of its abstract symbols.
The command-line tool why3 (described in Section 1.3), allows us to see the effect of cloning. If the input file containing our example is called lists.why, we can launch the following command:
> why3 lists.why -T SortedIntList
to see the resulting theory SortedIntList:
|theory SortedIntList (* use BuiltIn *) (* use Int *) (* use List *) axiom Le_refl : forall x:int. x <= x axiom Le_asym : forall x:int, y:int. x <= y -> y <= x -> x = y axiom Le_trans : forall x:int, y:int, z:int. x <= y -> y <= z -> x <= z (* clone Order with type t = int, predicate (<=) = (<=), prop Le_trans1 = Le_trans, prop Le_asym1 = Le_asym, prop Le_refl1 = Le_refl *) inductive sorted (list int) = | Sorted_Nil : sorted (Nil:list int) | Sorted_One : forall x:int. sorted (Cons x (Nil:list int)) | Sorted_Two : forall x:int, y:int, l:list int. x <= y -> sorted (Cons y l) -> sorted (Cons x (Cons y l)) (* clone SortedGen with type t1 = int, predicate sorted1 = sorted, predicate (<=) = (<=), prop Sorted_Two1 = Sorted_Two, prop Sorted_One1 = Sorted_One, prop Sorted_Nil1 = Sorted_Nil, prop Le_trans2 = Le_trans, prop Le_asym2 = Le_asym, prop Le_refl2 = Le_refl *) end|
In conclusion, let us briefly explain the concept of namespaces in Why3. Both use and clone instructions can be used in three forms (the examples below are given for use, the semantics for clone is the same):
Why3 allows to open new namespaces explicitly in the text. In particular, the instruction “clone import Order as O” can be equivalently written as:
|namespace import O clone export Order end|
However, since Why3 favors short theories over long and complex ones, this feature is rarely used.
We now consider another, slightly more complex example: how to use Why3 to solve a little puzzle known as “Einstein’s logic
problem”. (This Why3 example was contributed by Stéphane Lescuyer.)
The code given below is available in the source distribution in
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 "Einstein's problem"|
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|
It introduces two functions, namely Color.of and Color.to_, from houses to colors and colors to houses, respectively, and the two 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 "Hints" 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 the fourth theory:
|theory Problem "Goal of Einstein's problem" use import Einstein use import EinsteinHints goal G: Pet.to_ Fish = German end|
and we are ready to use Why3 to discharge this goal with any prover of our choice.