12. Technical Informations¶
12.1. Structure of Session Files¶
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 format CDATA #IMPLIED>
<!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 (path*, (resultundoneinternalfailureunedited))>
<!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 (validinvalidunknowntimeoutoutofmemorysteplimitexceededfailurehighfailure) #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>
12.2. Prover Detection¶
The data configuration for the automatic detection of installed provers
is stored in the file proversdetectiondata.conf
typically located
in directory /usr/local/share/why3
after installation.
12.3. The why3.conf
Configuration File¶
One can use a custom configuration file. The Why3 tools look for it in the following order:
the file specified by the
why3 config
option,the file specified by the environment variable
WHY3CONFIG
if set,the file
$HOME/.why3.conf
($USERPROFILE/.why3.conf
under Windows) or, in the case of local installation,why3.conf
in the top directory of Why3 sources.
If none of these files exist, a builtin 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 altergo]
.
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.
12.3.1. Extra Configuration Files¶
In addition to the main configuration file, Why3 commands accept the
option why3 extraconfig
to read one or more files
containing additional configuration option. It allows the user to pass
extra declarations in prover drivers, as illustrated in
Section 12.5, including declarations for
realizations, as illustrated in Section 11.2.
12.4. Drivers for External Provers¶
Drivers for external provers are readable files from directory
drivers
. They describe how Why3 should interact
with external provers.
Files with .drv
extension represent drivers that might be
associated to a specific solver in the why3.conf
configuration file (see Section 12.3 for more information);
files with .gen
extension are intended to be imported by
other drivers; finally, files with .aux
extension are
automatically generated from the main Makefile
.
The most important drivers dependencies are shown in the following figures: Fig. 12.1 shows the drivers files for SMT solvers, Fig. 12.2 for TPTP solvers, Fig. 12.3 for Coq, Fig. 12.4 for Isabelle/HOL, and Fig. 12.5 for PVS.
12.5. Adding extra drivers for user theories¶
It is possible for the users to augment the system drivers with extra information for their own declared theories. The processus is described by the following example.
First, we define a new theory in a file bvmisc.mlw
, containing
theory T
use bv.BV8
use bv.BV16
function lsb BV16.t : BV8.t (** least significant bits *)
function msb BV16.t : BV8.t (** most significant bits *)
end
For such a theory, it is a good idea to declare specific translation
rules for provers that have a builtin bitvector support, such as Z3
and CVC4 in this example. To do so, we write a extension driver file,
my.drv
, containing
theory bvmisc.T
syntax function lsb "((_ extract 7 0) %1)"
syntax function msb "((_ extract 15 8) %1)"
end
Now to tell Why3 that we would like this driver extension when calling
Z3 or CVC4, we write an extra configuration file, my.conf
,
containing
[prover_modifiers]
prover = "CVC4"
driver = "my.drv"
[prover_modifiers]
prover = "Z3"
driver = "my.drv"
Finally, to make the whole thing work, we have to call any Why3 command
with the additional option why3 extraconfig
, such as
why3 extraconfig=my.conf prove myfile.mlw
12.6. Transformations¶
This section documents the available transformations. Note that the set
of available transformations in your own installation is given
by why3 listtransforms
.

apply
¶ Apply an hypothesis to the goal of the task using a modus ponens rule. The hypothesis should be an implication whose conclusion can be matched with the goal. The intuitive behavior of
apply
can be translated as follows. Given \(\Gamma, h: f_1 \rightarrow f_2 \vdash G: f_2\),apply h
generates a new task \(\Gamma, h: f_1 \rightarrow f_2 \vdash G: f_1\).In practice, the transformation also manages to instantiate some variables with the appropriate terms.
For example, applying the transformation
apply zero_is_even
on the following goalpredicate is_even int predicate is_zero int axiom zero_is_even: forall x: int. is_zero x > is_even x goal G: is_even 0
produces the following goal:
predicate is_even int predicate is_zero int axiom zero_is_even: forall x:int. is_zero x > is_even x goal G: is_zero 0
The transformation first matched the goal against the hypothesis and instantiated
x
with0
. It then applied the modus ponens rule to generate the new goal.This transformation helps automated provers when they do not know which hypothesis to use in order to prove a goal.

apply with
¶ Variant of
apply
intended to be used in contexts where the latter cannot infer what terms to use for variables given in the applied hypothesis.For example, applying the transformation
apply transitivity
on the following goalaxiom ac: a = c axiom cb: c = b axiom transitivity : forall x y z:int. x = y > y = z > x = z goal G1 : a = b
raises the following error:
apply: Unable to infer arguments (try using "with") for: y
It means that the tool is not able to infer the right term to instantiate symbol
y
. In our case, the user knows that the termc
should work. So, it can be specified as follows:apply transitivity with c
This generates two goals which are easily provable with hypotheses
ac
andcb
.When multiple variables are needed, they should be provided as a list in the transformation. For the sake of the example, we complicate the
transitivity
hypothesis:axiom t : forall x y z k:int. k = k > x = y > y = z > x = z
A value can be provided for
k
as follows:apply t with c,0
.

assert
¶ Create an intermediate subgoal. This is comparable to
assert
written in WhyML code. Here, the intent is only to help provers by specifying one key argument of the reasoning they should use.Example: From a goal of the form \(\Gamma \vdash G\), the transformation
assert (n = 0)
produces the following two tasks: \(\Gamma \vdash h: n = 0\) and \(\Gamma, h: n = 0 \vdash G\). This effectively addsh
as an intermediate goal to prove.

assert as
¶ Same as
assert
, except that a name can be given to the new hypothesis. Example:assert (x = 0) as x0
.

case
¶ Split a goal into two subgoal, using the excluded middle on a given formula. On the task \(\Gamma \vdash G\), the transformation
case f
produces two tasks: \(\Gamma, h: f \vdash G\) and \(\Gamma, h: \neg f \vdash G\).For example, applying
case (x = 0)
on the following goalsconstant x : int constant y : int goal G: if x = 0 then y = 2 else y = 3
produces the following goals:
constant x : int constant y : int axiom h : x = 0 goal G : if x = 0 then y = 2 else y = 3
constant x : int constant y : int axiom h : not x = 0 goal G : if x = 0 then y = 2 else y = 3
The intent is again to simplify the job of automated provers by giving them a key argument of the reasoning behind the proof of a subgoal.

case as
¶ Same as
case
, except that a name can be given to the new hypothesis. Example:case (x = 0) as x0
.

clear_but
¶ Remove all the hypotheses except those specified in the arguments. This is useful when a prover fails to find relevant hypotheses in a very large context. Example:
clear_but h23,h25
.

compute_hyp
¶ Apply the transformation
compute_in_goal
on the given hypothesis.

compute_hyp_specified
¶ Apply the transformation
compute_specified
on the given hypothesis.

compute_in_goal
¶ Aggressively apply all known computation/simplification rules.
The kinds of simplification are as follows.
Computations with builtin symbols, e.g., operations on integers, when applied to explicit constants, are evaluated. This includes evaluation of equality when a decision can be made (on integer constants, on constructors of algebraic data types), Boolean evaluation, simplification of patternmatching/conditional expression, extraction of record fields, and betareduction. At best, these computations reduce the goal to
true
and the transformations thus does not produce any subgoal. For example, a goal like6*7=42
is solved by those transformations.Unfolding of definitions, as done by
inline_goal
. Transformationcompute_in_goal
unfolds all definitions, including recursive ones. Forcompute_specified
, the user can enable unfolding of a specific logic symbol by attaching the metarewrite_def
to the symbol.function sqr (x:int) : int = x * x meta "rewrite_def" function sqr
Rewriting using axioms or lemmas declared as rewrite rules. When an axiom (or a lemma) has one of the forms
axiom a: forall ... t1 = t2
or
axiom a: forall ... f1 <> f2
then the user can declare
meta "rewrite" prop a
to turn this axiom into a rewrite rule. Rewriting is always done from left to right. Beware that there is no check for termination nor for confluence of the set of rewrite rules declared.
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 bycompute_specified
.The computations performed by this transformation 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 partlyreduced goal is returned as the result of the transformation.

compute_specified
¶ Same as
compute_in_goal
, but perform rewriting using only builtin operators and userprovided rules.

destruct
¶ Eliminate the head symbol of a hypothesis.
For example, applying
destruct h
on the following goalconstant p1 : bool predicate p2 int axiom h : p1 = True /\ (forall x:int. p2 x) goal G : p2 0
removes the logical connective
/\
and producesconstant p1 : bool predicate p2 int axiom h1 : p1 = True axiom h : forall x:int. p2 x goal G : p2 0
destruct
can be applied on the following constructions:false
,true
,/\
,\/
,>
,not
,exists
,if ... then ... else ...
,match ... with ... end
,(in)equality on constructors of the same type.

destruct_rec
¶ Recursively call
destruct
on the generated hypotheses. The recursion on implication andmatch
stops after the first occurence of a different symbol.For example, applying
destruct_rec H
on the following goalpredicate a predicate b predicate c axiom H : (a > b) /\ (b /\ c) goal G : false
does not destruct the implication symbol because it occurs as a subterm of an already destructed symbol. This restriction applies only to implication and
match
Other symbols are destructed recursively. Thus, in the generated task, the second/\
is simplified:predicate a predicate b predicate c axiom H2 : a > b axiom H1 : b axiom H: c goal G : false

destruct_term
¶ Destruct an expression according to the type of the expression. The transformation produces all possible outcomes of a destruction of the algebraic type.
For example, applying
destruct_term a
on the following goaltype t = A  B int constant a : t goal G : a = A
produces the following two goals:
type t = A  B int constant a : t constant x : int axiom h : a = B x goal G : a = A
type t = A  B int constant a : t axiom h : a = A goal G : a = A
The term was destructed according to all the possible outcomes in the type. Note that, during destruction, a new constant
x
has been introduced for the argument of constructorB
.

destruct_term using
¶ Same as
destruct_term
, except that names can be given to the constants that were generated.

destruct_term_subst
¶ Same as
destruct_term
, except that it also substitutes the created term.

eliminate_builtin
¶ Remove definitions of symbols that are declared as builtin in the driver, with a “syntax” rule.

eliminate_definition_func
¶ Replace all function definitions with axioms.

eliminate_definition_pred
¶ Replace all predicate definitions with axioms.

eliminate_definition
¶ Apply both
eliminate_definition_func
andeliminate_definition_pred
.

eliminate_if
¶ Apply both
eliminate_if_term
andeliminate_if_fmla
.

eliminate_if_fmla
¶ Replace formulas of the form
if f1 then f2 else f3
by an equivalent formula using implications and other connectives.

eliminate_if_term
¶ Replace terms of the form
if formula then t2 else t3
by lifting them at the level of formulas. This may introduceif then else
in formulas.

eliminate_inductive
¶ Replace inductive predicates by (incomplete) axiomatic definitions, construction axioms and an inversion axiom.

eliminate_let
¶ Apply both
eliminate_let_fmla
andeliminate_let_term
.

eliminate_let_fmla
¶ Eliminate
let
by substitution, at the predicate level.

eliminate_let_term
¶ Eliminate
let
by substitution, at the term level.

eliminate_literal
¶

eliminate_mutual_recursion
¶ Replace mutually recursive definitions with axioms.

eliminate_recursion
¶ Replace all recursive definitions with axioms.

encoding_tptp
¶ Encode theories into unsorted logic.

exists
¶ Instantiate an existential quantification with a witness.
For example, applying
exists 0
on the following goalgoal G : exists x:int. x = 0
instantiates the symbol
x
with0
. Thus, the goal becomesgoal G : 0 = 0

hide
¶ Hide a given term, by creating a new constant equal to the term and then replacing all occurences of the term in the context by this constant.
For example, applying
hide t (1 + 1)
on the goalconstant y : int axiom h : forall x:int. x = (1 + 1) goal G : (y  (1 + 1)) = ((1 + 1)  (1 + 1))
replaces all the occurrences of
(1 + 1)
witht
, which gives the following goal:constant y : int constant t : int axiom H : t = (1 + 1) axiom h : forall x:int. x = t goal G : (y  t) = (t  t)

hide_and_clear
¶ First apply
hide
and then remove the equality between the hidden term and the introduced constant. This means that the hidden term completely disappears and cannot be recovered.

induction
¶ Perform a reasoning by induction for the current goal.
For example, applying
induction n
on the following goalconstant n : int predicate p int predicate p1 int axiom h : p1 n goal G : p n
performs an induction on
n
starting at0
. The goal for the base case isconstant n : int predicate p int predicate p1 int axiom h : p1 n axiom Init : n <= 0 goal G : p n
while the recursive case is
constant n : int predicate p int predicate p1 int axiom h : p1 n axiom Init : 0 < n axiom Hrec : forall n1:int. n1 < n > p1 n1 > p n1 goal G : p n

induction_arg_pr
¶ Apply
induction_pr
on the given hypothesis/goal symbol.

induction_arg_ty_lex
¶ Apply
induction_ty_lex
on the given symbol.

induction_pr
¶

induction_ty_lex
¶ Perform structural, lexicographic induction on goals involving universally quantified variables of algebraic data types, such as lists, trees, etc. For instance, it transforms the following goal
goal G: forall l: list 'a. length l >= 0
into this one:
goal G : forall l:list 'a. match l with  Nil > length l >= 0  Cons a l1 > length l1 >= 0 > length l >= 0 end
When induction can be applied to several variables, the transformation picks one heuristically. The
[@induction]
attribute can be used to force induction over one particular variable, withgoal G: forall l1 [@induction] l2 l3: list 'a. l1 ++ (l2 ++ l3) = (l1 ++ l2) ++ l3
induction will be applied on
l1
. If this attribute is attached to several variables, a lexicographic induction is performed on these variables, from left to right.

inline_trivial
¶ Expand and remove definitions of the form
function f x1 ... xn = g e1 ... ek predicate p x1 ... xn = q e1 ... ek
when each
ei
is either a ground term or one of thexj
, and eachx1 ... xn
occurs at most once in all theei
.The attribute
[@inline:trivial]
can be used to tag functions, so that the transformation forcefully expands them (not using the conditions above). This can be used to ensure that some specific functions are inlined for automatic provers (inline_trivial
is used in many drivers).

inline_goal
¶ Expand all outermost symbols of the goal that have a nonrecursive definition.

inline_all
¶ Expand all nonrecursive definitions.

instantiate
¶ Generate a new hypothesis with quantified variables replaced by the given terms.
For example, applying
instantiate h 0, 1
on the following goalpredicate p int axiom h : forall x:int, y:int. x <= y > p x /\ p y goal G : p 0
generates a new hypothesis:
predicate p int axiom h : forall x:int, y:int. x <= y > p x /\ p y axiom Hinst : 0 <= 1 > p 0 /\ p 1 goal G : p 0
This is used to help automatic provers that are generally better at working on instantiated hypothesis.

inst_rem
¶ Apply
instantiate
then remove the original instantiated hypothesis.

introduce_premises
¶ Move antecedents of implications and universal quantifications of the goal into the premises of the task.

intros
¶ Introduce universal quantifiers in the context.
For example, applying
intros n, m
on the following goalpredicate p int int int goal G : forall x:int, y:int, z:int. p x y z
produces the following goal:
predicate p int int int constant n : int constant m : int goal G : forall z:int. p n m z

intros_n
¶ Same as
intros
, but stops after the nth quantified variable or premise.For example, applying
intros_n 2
on the following goalpredicate p int int int goal G : forall x:int, y:int, z:int. p x y z
produces the following goal:
predicate p int int int constant x : int constant y : int goal G : forall z:int. p x y z

inversion_arg_pr
¶ Apply
inversion_pr
on the given hypothesis/goal symbol.

inversion_pr
¶

left
¶ Remove the right part of the head disjunction of the goal.
For example, applying
left
on the following goalconstant x : int goal G : x = 0 \/ x = 1
produces the following goal:
constant x : int goal G : x = 0

pose
¶ Add a new constant equal to the given term.
For example, applying
pose t (x + 2)
to the following goalconstant x : int goal G : true
produces the following goal:
constant x : int constant t : int axiom H : t = (x + 2) goal G : true

remove
¶ Remove a hypothesis from the context.
For example, applying
remove h
on the following goalaxiom h : true goal G : true
produces the following goal:
goal G : true

replace
¶ Replace a term with another one in a hypothesis or in the goal. This generates a new goal which asks for the proof of the equality.
For example, applying
replace (y + 1) (x + 2) in h
on the following goalconstant x : int constant y : int axiom h : x >= (y + 1) goal G : true
produces the following two goals:
constant x : int constant y : int axiom h : x >= (x + 2) goal G : true
constant x : int constant y : int axiom h : x >= (y + 1) goal G : (y + 1) = (x + 2)

revert
¶ Opposite of
intros
. It takes hypotheses/constants and quantifies them in the goal.For example, applying
revert x
on the following goalconstant x : int constant y : int axiom h : x = y goal G : true
produces the following goal:
constant y : int goal G : forall x:int. x = y > true

rewrite
¶ Rewrite using the given equality hypothesis.
For example, applying
rewrite eq
on the following goalfunction a int : bool function b int : bool constant y : int axiom eq : forall x:int. not x = 0 > a x = b x goal G : a y = True
produces the following goal:
function a int : bool function b int : bool constant y : int axiom eq : forall x:int. not x = 0 > a x = b x goal G : b y = True
It also produces a goal for the premise of the equality hypothesis (as would
apply
):function a int : bool function b int : bool constant y : int axiom eq : forall x:int. not x = 0 > a x = b x goal G : not y = 0

rewrite with
¶ Variant of
rewrite
intended to be used in contexts where the latter cannot infer what terms to use for the variables of the given hypotheses (see alsoapply with
).For example, the transformation
rewrite eq with 0
can be applied to the following goal:function a int : bool function b int : bool constant y : int axiom eq : forall x:int, z:int. z = 0 > not x = 0 > a x = b x goal G : a y = True
Here, a value is provided for the symbol
z
. This leads to the following three goals. One is the rewritten one, while the other two are for the premises of the equality hypothesis.function a int : bool function b int : bool constant y : int axiom eq : forall x:int, z:int. z = 0 > not x = 0 > a x = b x goal G : b y = True
function a int : bool function b int : bool constant y : int axiom eq : forall x:int, z:int. z = 0 > not x = 0 > a x = b x goal G : 0 = 0
function a int : bool function b int : bool constant y : int axiom eq : forall x:int, z:int. z = 0 > not x = 0 > a x = b x goal G : not y = 0

right
¶ Remove the left part of the head disjunction of the goal.
For example, applying
right
on the following goalconstant x : int goal G : x = 0 \/ x = 1
produces the following goal:
constant x : int goal G : x = 1

simplify_array
¶ Automatically rewrite the task using the lemma
Select_eq
of theorymap.Map
.

simplify_formula
¶ Reduce trivial equalities
t=t
to true and then simplify propositional structure: removestrue
,false
, simplifiesf /\ f
tof
, etc.

simplify_formula_and_task
¶ Apply
simplify_formula
and remove the goal if it is equivalent to true.

simplify_recursive_definition
¶ Reduce mutually recursive definitions if they are not really mutually recursive, e.g.,
function f : ... = ... g ... with g : ... = e
becomes
function g : ... = e function f : ... = ... g ...
if
f
does not occur ine
.

simplify_trivial_quantification
¶ Simplify quantifications of the form
forall x, x = t > P(x)
into
P(t)
when
x
does not occur int
. More generally, this simplification is applied wheneverx=t
ort=x
appears in negative position.

simplify_trivial_quantification_in_goal
¶ Apply
simplify_trivial_quantification
, but only in the goal.

split_all
¶ Perform both
split_premise
andsplit_goal
.

split_all_full
¶ Perform both
split_premise
andsplit_goal_full
.

split_goal
¶ Change conjunctive goals into the corresponding set of subgoals. In absence of case analysis attributes, the number of subgoals generated is linear in the size of the initial goal.
The transformation treats specially asymmetric and
by
/so
connectives. Asymmetric conjunctionA && B
in goal position is handled as syntactic sugar forA /\ (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 forA \/ ((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 interpretationA
. In goal position, it is treated as ifB
was an intermediate step for provingA
.A by B
is then replaced byB
and the transformation also generates a sidecondition subgoalB > A
representing the logical cut.Although splitting stops at disjunctive points like symmetric disjunction and lefthand sides of implications, the occurrences of the
by
connective are not restricted. For instance:Splitting
goal G : (A by B) && C
generates the subgoals
goal G1 : B goal G2 : A > C goal G3 : B > A (* sidecondition *)
Splitting
goal G : (A by B) \/ (C by D)
generates
goal G1 : B \/ D goal G2 : B > A (* sidecondition *) goal G3 : D > C (* sidecondition *)
Splitting
goal G : (A by B)  (C by D)
generates
goal G1 : B  D goal G2 : B > A (* sidecondition *) goal G3 : B  (D > C) (* sidecondition *)
Note that due to the asymmetric disjunction, the disjunction is kept in the second sidecondition subgoal.
Splitting
goal G : exists x. P x by x = 42
generates
goal G1 : exists x. x = 42 goal G2 : forall x. x = 42 > P x (* sidecondition *)
Note that in the sidecondition subgoal, the context is universally closed.
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 interpretationA
. In hypothesis position, it is treated as if bothA
andB
were true becauseB
is a consequence ofA
.A so B
is replaced byA /\ B
and the transformation also generates a sidecondition subgoalA > B
corresponding to the consequence relation between formula.As with the
by
connective, occurrences ofso
are unrestricted. Examples:Splitting
goal G : (((A so B) \/ C) > D) && E
generates
goal G1 : ((A /\ B) \/ C) > D goal G2 : (A \/ C > D) > E goal G3 : A > B (* sidecondition *)
Splitting
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))) *)
generates
goal G1 : exists x. P x goal G2 : forall x. P x > Q x (* sidecondition *) goal G3 : forall x. P x > Q x > T x (* sidecondition *) goal G4 : forall x. P x > Q x > T x > R x (* sidecondition *) goal G5 : (exists x. P x /\ Q x /\ R x) > A (* sidecondition *)
In natural language, this corresponds to the following proof scheme for
A
: There exists ax
for whichP
holds. Then, for that witnessQ
andR
also holds. The last one holds becauseT
holds as well. And from those three conditions onx
, we can deduceA
.
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 nongoal position, itsby
/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, applyingsplit_goal
ongoal 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 blowup.
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.

split_goal_full
¶ Behave similarly to
split_goal
, but also convert the goal to conjunctive normal form. The number of subgoals generated may be exponential in the size of the initial goal.

split_intro
¶ Perform both
split_goal
andintroduce_premises
.

split_premise
¶ Replace axioms in conjunctive form by an equivalent collection of axioms. In absence of case analysis attributes (see
split_goal
for details), the number of axiom generated per initial axiom is linear in the size of that initial axiom.

split_premise_full
¶ Behave similarly to
split_premise
, but also convert the axioms to conjunctive normal form. The number of axioms generated per initial axiom may be exponential in the size of the initial axiom.

subst
¶ Substitute a given constant using an equality found in the context. The constant is removed.
For example, when applying
subst x
on the following goalconstant x : int constant y : int constant z : int axiom h : x = y + 1 axiom h1 : z = (x + y) goal G : x = z
the transformation first finds the hypothesis
h
that can be used to rewritex
. Then, it replaces every occurrences ofx
withy + 1
. Finally, it removesh
andx
. The resulting goal is as follows:constant y : int constant z : int axiom h1 : z = ((y + 1) + y) goal G : (y + 1) = z
This transformation is used to make the task more easily readable by a human during debugging. This transformation should not help automatic provers at all as they generally implement substitution rules in their logic.

unfold
¶ Unfold the definition of a logical symbol in the given hypothesis.
For example, applying
unfold p
on the following goalpredicate p (x:int) = x <= 22 axiom h : forall x:int. p x > p (x  1) goal G : p 21
produces the following goal:
predicate p (x:int) = x <= 22 axiom h : forall x:int. p x > p (x  1) goal G : 21 <= 22
One can also unfold in the hypothesis, using
unfold p in h
, which gives the following goal:predicate p (x:int) = x <= 22 axiom h : forall x:int. x <= 22 > (x  1) <= 22 goal G : 21 <= 22

use_th
¶ Import a theory inside the current context. This is used, in some rare case, to reduced the size of the context in other goals, since importing a theory in the WhyML code would the theory available in all goals whereas the theory is only needed in one specific goal.
For example, applying
use_th int.Int
on the following goalpredicate p int goal G : p 5
imports the
Int
theory. So, one is able to use the addition over integers, e.g.,replace 5 (2 + 3)
.Any lemma appearing in the imported theory can also be used.
Note that axioms are also imported. So, this transformation should be used with care. We recommend to use only theories that do not contain any axiom because this transformation could easily make the context inconsistent.
12.7. Proof Strategies¶
As seen in Section 6.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 assemblystyle language, and put into the Why3 configuration file. The commands of this basic language are:
c p t m
calls the prover p with a time limit t and memory limit m. On success, the strategy ends, it continues to next line otherwise.t n lab
applies the transformation n. On success, the strategy continues to label lab, and is applied to each generated subgoals. It continues to next line otherwise.g lab
unconditionally jumps to label lab.lab:
declares the label lab. The default labelexit
stops the program.
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 AltErgo 2.3.0, CVC4 1.7 and Z3 4.8.4 were detected by
the why3 config
command.
 Split_VC
is bound to the 1line strategy
t split_vc exit
 Auto_level_0
is bound to
c Z3,4.8.4, 1 1000 c AltErgo,2.3.0, 1 1000 c CVC4,1.7, 1 1000
The 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.
 Auto_level_1
is bound to
c Z3,4.8.4, 5 1000 c AltErgo,2.3.0, 5 1000 c CVC4,1.7, 5 1000
Same as Auto_level_0 but with 5 seconds instead of 1.
 Auto_level_2
is bound to
start: c Z3,4.8.4, 1 1000 c AltErgo,2.3.0, 1 1000 c CVC4,1.7, 1 1000 t split_vc start c Z3,4.8.4, 10 4000 c AltErgo,2.3.0, 10 4000 c CVC4,1.7, 10 4000
The 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 subgoals. If the split does not succeed, the provers are tried again with larger limits.
 Auto level 3
is bound to
start: c Z3,4.8.4, 1 1000 c Eprover,2.0, 1 1000 c Spass,3.7, 1 1000 c AltErgo,2.3.0, 1 1000 c CVC4,1.7, 1 1000 t split_vc start c Z3,4.8.4, 5 2000 c Eprover,2.0, 5 2000 c Spass,3.7, 5 2000 c AltErgo,2.3.0, 5 2000 c CVC4,1.7, 5 2000 t introduce_premises afterintro afterintro: t inline_goal afterinline g trylongertime afterinline: t split_all_full start trylongertime: c Z3,4.8.4, 30 4000 c Eprover,2.0, 30 4000 c Spass,3.7, 30 4000 c AltErgo,2.3.0, 30 4000 c CVC4,1.7, 30 4000
Notice 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 subgoals. 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.
12.8. WhyML Attributes¶

case_split
¶

induction
¶

infer
¶

inline:trivial
¶

model_trace
¶

rewrite
¶

stop_split
¶

vc:annotation
¶

vc:divergent
¶

vc:keep_precondition
¶

vc:sp
¶

vc:wp
¶

vc:white_box
¶
12.9. Why3 Metas¶
12.10. Debug Flags¶

inferloop
¶

inferprintairesult
¶

inferprintcfg
¶

printinferredinvs
¶

printdomainsloop
¶

stack_trace
¶
12.11. Updating Syntax Error Messages¶
Here is the developer’s recipe to update a syntax error message. We do it on the following illustrative example.
function let int : int
If such a file is passed to Why3, one obtains:
File "bench/parsing/bad/498_function.mlw", line 1, characters 912:
syntax error
The recipe given here provides a way to produce a more informative message. It is based on handcrafted error messages provided by the Menhir parser generator.
The first step is to call menhir with option interpreterror
while giving as input the erroneous input, under the form of a sequence
of tokens as generated by src/parser/lexer.mll
.
$ echo "decl_eof: FUNCTION LET"  menhir base src/parser/parser interpreterror src/parser/parser_common.mly src/parser/parser.mly
decl_eof: FUNCTION LET
##
## Ends in an error in state: 1113.
##
## pure_decl > FUNCTION . function_decl list(with_logic_decl) [ VAL USE TYPE THEORY SCOPE PREDICATE MODULE META LET LEMMA INDUCTIVE IMPORT GOAL FUNCTION EXCEPTION EOF END CONSTANT COINDUCTIVE CLONE AXIOM ]
##
## The known suffix of the stack is as follows:
## FUNCTION
##
<YOUR SYNTAX ERROR MESSAGE HERE>
The text returned by that command should be appended to
src/parser/handcrafted.messages
, with of course an appropriate error
message, such as this one:
expected function name must be a nonreserved uncapitalized identifier (token LIDENT_NQ), found "$0"