12. Technical Informations

12.1. Prover Detection

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.

12.2. The why3.conf Configuration File

One can use a custom configuration file. The Why3 tools look for it in the following order:

1. the file specified by the why3 --config option,

2. the file specified by the environment variable WHY3CONFIG if set,

3. 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 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.

12.2.1. Extra configuration files

In addition to the main configuration file, Why3 commands accept the option why3 --extra-config 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.4, including declarations for realizations, as illustrated in Section 10.2.

12.3. 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.2 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.

Fig. 12.1 Driver dependencies for SMT solvers

Fig. 12.2 Driver dependencies for TPTP solvers

Fig. 12.3 Driver dependencies for Coq

Fig. 12.4 Driver dependencies for Isabelle/HOL

Fig. 12.5 Driver dependencies for PVS

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.4. Drivers for User Theories

It is possible for the users to augment the system drivers with extra information for their own declared theories. The process 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 built-in bit-vector 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 --extra-config, such as

why3 --extra-config=my.conf prove myfile.mlw

12.5. Transformations

This section documents the available transformations. Note that the set of available transformations in your own installation is given by why3 show transformations.

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 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_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 with 0. 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 goal

axiom 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 term c should work. So, it can be specified as follows: apply transitivity with c

This generates two goals which are easily provable with hypotheses ac and cb.

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 adds h 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 subgoals, 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 goals

constant 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 built-in 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 pattern-matching/conditional expression, extraction of record fields, and beta-reduction. At best, these computations reduce the goal to true and the transformations thus does not produce any sub-goal. For example, a goal like 6*7=42 is solved by those transformations.

• Unfolding of definitions, as done by 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
  

• 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 by compute_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 partly-reduced goal is returned as the result of the transformation.

compute_specified

Same as compute_in_goal, but perform rewriting using only built-in operators and user-provided rules.

cut

Same as assert, but the order of the generated subgoals is reversed.

destruct

Eliminate the head symbol of a hypothesis.

For example, applying destruct h on the following goal

constant p1 : bool
predicate p2 int
axiom h : p1 = True /\ (forall x:int. p2 x)
goal G : p2 0

removes the logical connective /\ and produces

constant 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 and match stops after the first occurrence of a different symbol.

For example, applying destruct_rec H on the following goal

predicate 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 goal

type 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 constructor B.

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_algebraic

Replace algebraic data types by first-order definitions [Pas09].

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 and eliminate_definition_pred.

eliminate_if

Apply both eliminate_if_term and eliminate_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 introduce if 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 and eliminate_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_smt

Encode polymorphic types into monomorphic types [BCCL08].

encoding_tptp

Encode theories into unsorted logic.

exists

Instantiate an existential quantification with a witness.

For example, applying exists 0 on the following goal

goal G : exists x:int. x = 0

instantiates the symbol x with 0. Thus, the goal becomes

goal G : 0 = 0

hide

Hide a given term, by creating a new constant equal to the term and then replacing all occurrences of the term in the context by this constant.

For example, applying hide t (1 + 1) on the goal

constant 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) with t, 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 goal

constant n : int
predicate p int
predicate p1 int
axiom h : p1 n
goal G : p n

performs an induction on n starting at 0. The goal for the base case is

constant 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 from

Same as induction, but it starts the induction from a given integer instead of 0.

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, with

goal 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 the xj, and each x1 ... xn occurs at most once in all the ei.

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 non-recursive definition.

inline_all

Expand all non-recursive definitions.

instantiate

Generate a new hypothesis with quantified variables replaced by the given terms.

For example, applying instantiate h 0, 1 on the following goal

predicate 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 goal

predicate 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 goal

predicate 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 goal

constant 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 goal

constant 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 goal

axiom h : true
goal G : true

produces the following goal:

goal G : true

remove_unused

Remove from the context all the logic symbols that are not used by the goal or the hypothesis.

The effect of that transformation can be expanded by adding dependency metas. Namely, with a declaration of the form

meta "remove_unused:dependency" axiom a, function f

then occurrences of f in axiom a are not counted as occurrences for f. The intended meaning is that a is a definitional axiom for f, so when f is not needed in the remainder, both the axiom and the declaration of f can be removed.

When there are several such definitional axioms for f, a meta must be declared for each axiom. When an axiom is definitional for several symbols at the same time, several meta must be declared as well. The rule of thumb is that an axiom is kept as soon as at least one of the symbols it defines is needed in the remainder, otherwise it is discarded.

remove_unused_keep_constant

A variant of remove_unused above, where the constant, i.e. the nullary function symbols, are always kept.

The effect of that transformation is controllable with an additional meta of the form

meta "remove_unused:remove_constant" constant f

when in that case f is also tried to be removed, as if it was with the full remove_unused transformation.

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 goal

constant 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)

It can be seen as the combination of assert and rewrite.

revert

Opposite of intros. It takes hypotheses/constants and quantifies them in the goal.

For example, applying revert x on the following goal

constant 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 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 : 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 also apply 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

rewrite_list

Variant of rewrite that allows simultaneous rewriting in a list of hypothesis/goals.

right

Remove the left part of the head disjunction of the goal.

For example, applying right on the following goal

constant 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 theory map.Map.

simplify_formula

Reduce trivial equalities t=t to true and then simplify propositional structure: removes true, false, simplifies f /\ f to f, 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 in e.

simplify_trivial_quantification

Simplify quantifications of the form

forall x, x = t -> P(x)

into

P(t)

when x does not occur in t. More generally, this simplification is applied whenever x=t or t=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 and split_goal.

split_all_full

Perform both split_premise and split_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 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:

• Splitting

  goal G : (A by B) && C
  

  generates the subgoals

  goal G1 : B
  goal G2 : A -> C
  goal G3 : B -> A (* side-condition *)
  

• Splitting

  goal G : (A by B) \/ (C by D)
  

  generates

  goal G1 : B \/ D
  goal G2 : B -> A (* side-condition *)
  goal G3 : D -> C (* side-condition *)
  

• Splitting

  goal G : (A by B) || (C by D)
  

  generates

  goal G1 : B || D
  goal G2 : B -> A        (* side-condition *)
  goal G3 : B || (D -> C) (* side-condition *)
  

  Note that due to the asymmetric disjunction, the disjunction is kept in the second side-condition 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 (* side-condition *)
  

  Note that in the side-condition 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 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. 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               (* side-condition *)
  

• 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               (* 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 *)
  

  In natural language, this corresponds to the following proof scheme for 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.

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 and introduce_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 goal

constant 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 rewrite x. Then, it replaces every occurrences of x with y + 1. Finally, it removes h and x. 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.

subst_all

Substitute all the variables that can be substituted.

For example, applying subst_all on the following goal

constant x : int
constant x1 : int
constant y : int
constant z : int
axiom h : x = (y + 1)
axiom hx1 : x = x1
axiom h1 : z = (x + y)
goal G : x = z

produces the following goal, where x, x1, and z have been removed:

constant y : int
goal G : (y + 1) = ((y + 1) + y)

The order in which constants are substituted is not specified.

unfold

Unfold the definition of a logical symbol in the given hypothesis.

For example, applying unfold p on the following goal

predicate 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 goal

predicate 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.6. Proof Strategies

In the context of Why3, proof strategies are mechanisms that automate the application of transformations and provers on proof tasks. These strategies are mainly meant to be invoked in the IDE.

Strategies come into two flavours: first the so-called basic strategies, and second a more complex mechanism allowing one to program strategies in OCaml. Such strategies are supposed to be programmed on top of the module Strategy of the Why3 API. Such strategies can also by called goal-oriented, since programming them in OCaml provides a way to inspect the formulas in the goal or hypothesis of the task, and apply transformations depending on their shapes.

Below we document one of such strategy: a strategy for error propagation in floating-point computations.

12.6.1. Basic Strategies

As seen in Section 5.3, the IDE provides a few buttons that trigger the run of basic proof strategies on the selected goals. Such 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:

• 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.

• c p1 t1 m1 | ... | pk tk mk calls the provers p1 to pk in parallel. On success on one prover, the other provers are interrupted, and the strategy ends. It continues to next line if none of the provers succeed.

• t n lab applies the transformation n. On success, the strategy continues to label lab, and is applied to each generated sub-goals. It continues to next line otherwise.

• g lab unconditionally jumps to label lab.

• lab: declares the label lab. The default label exit stops the program.

To exemplify 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 2.3.0, CVC4 1.7, and Z3 4.8.4 have been detected by the why3 config command.

Split_VC

is bound to the 1-line strategy

t split_vc exit

Auto_level_0

is bound to

c Z3,4.8.4, 1 1000
c Alt-Ergo,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 | Alt-Ergo,2.3.0, 5 1000 | CVC4,1.7, 5 1000

Same as Auto_level_0 but with 5 seconds instead of 1, and in parallel.

Auto_level_2

is bound to

start:
c Z3,4.8.4, 1 1000
c Alt-Ergo,2.3.0, 1 1000
c CVC4,1.7, 1 1000
t split_vc start
c Z3,4.8.4, 10 4000 | Alt-Ergo,2.3.0, 10 4000 | 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 sub-goals. If the split does not succeed, the provers are tried again with larger limits, and in parallel.

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 Alt-Ergo,2.3.0, 1 1000
c CVC4,1.7, 1 1000
t split_vc start
c Z3,4.8.4, 5 2000 | Eprover,2.0, 5 2000 | Spass,3.7, 5 2000 | Alt-Ergo,2.3.0, 5 2000 | 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 | Eprover,2.0, 30 4000 | Spass,3.7, 30 4000 | Alt-Ergo,2.3.0, 30 4000 | 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 sub-goals. If the split does not succeed, the prover are tried again with limits of 5 s and 2 Gb, and in parallel. 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. Otherwise, provers are tried again, in parallel, with 30s and 4 Gb.

12.6.2. Forward propagation in floating-point computations

The specialized strategy forward_propagation can be used for automatically computing and proving a rounding error on a term of type ufloat which is the type of unbounded floats as defined in the theory ufloat of the standard library. More background on forward error propagation will be available soon in an incoming research report.

The only transformations used are :

• assert, to assert the existence of a forward error.

• apply, to apply one of the forward propagation lemmas.

The strategy uses the following process:

1. Look at the form of the goal. If the goal has the form abs (to_real x -. exact_x) <=. C, it goes to step 2, else it does nothing.

2. Look at term x. There are 2 cases :

• 2.1. : x is either the result of a supported ufloat operation (e.g. addition, multiplication) on some arguments or the result of the application of an approximation of a supported function (e.g. exponential) to some arguments. Then the strategy applies recursively step 2 for each argument of the ufloat operation/function approximation to compute their forward error. For each forward error computed, the strategy also generates a proof tree containing the steps to prove it. If at least one forward error is computed, then the propagation lemma corresponding to the ufloat operation/approximated function is used to compute the forward error for x and exact_x, and a corresponding proof tree is generated. The root of the proof tree consists of an assertion of the forward error computed for x, and the child node will generally be the application of the transformation apply with the propagation lemma as an argument. The propagation lemma contains hypotheses about forward errors for the arguments, therefore the proof trees computed for them recursively are attached as nodes to the corresponding nodes of the tree.

• 2.2. : x is something else. Then no forward error is computed and no proof tree is generated.

Currently, propagation lemmas exist for the following functions :

• ufloat addition, subtraction, multiplication and negation.

• ufloat approximations of log and exp functions.

• ufloat approximations of the iterated sum function (defined in stdlib module real.Sum).

The following excerpt is an example of a program that can be proved using the strategy :

use real.RealInfix
use real.Abs
use ufloat.USingle

let ghost addition_errors_basic (a b c : usingle)
  ensures {
    let exact = to_real a +. to_real b +. to_real c in
    let exact_abs = abs (to_real a) +. abs (to_real b) +. abs (to_real c) in
    abs (to_real result -. exact) <=. 2. *. eps *. exact_abs
  }
= a ++. b ++. c

To use the strategy within Why3 IDE in order to prove the program, one must perform the following steps :

1. Apply the split_vc transformation to generate the subgoals.

2. Select the proof node of the postcondition and apply the forward_propagation strategy, either by typing the name of the strategy in the command line or by right clicking on the proof node and selecting the strategy.

3. The strategy will generate a proof tree. The nodes of the tree should be easily proved using one of the auto strategies.

Note that the forward_propagation strategy can also be used when the user has no specific forward error in mind as a way to propose a provable bound. For instance in the example above, one could have replaced the term 2. *. eps *. exact_abs by anything in the postcondition. The strategy would still have worked and it would have generated an assertion about a forward error that it can prove. One could then use this forward error in the postcondition.

For more examples of the use of the strategy, see the directory examples/numeric of the examples repository.

12.7. WhyML Attributes

case_split

cfg:stackify

cfg:subregion_analysis

extraction:inline

If the name of a function is labeled with this attribute, its body will be inlined at every call site during extraction (see Section 9.2). This is especially useful for trivial wrapper functions whose only purpose is to provide a slightly different specification from the original function.

extraction:likely

This attribute can be applied to a Boolean expression to indicate whether it is likely to be true. This is used at extraction time (see Section 9.2), assuming the target language supports it. For example, when extracting to C, the extracted expression will be tagged with __builtin_expect.

extraction:unlikely

This attribute can be applied to a Boolean expression to indicate whether it is likely to be false. This is the opposite of extraction:likely.

extraction:preserve_single_field

This attribute is applied to the declaration of a record type. It is used to disable an optimization made by the preprocessing step that precedes the invocation of extraction drivers. During this step, record types with a single field like:

type t = { a : int }

are rewritten as:

type t = int

If this attribute is applied to t, then this optimization is disabled.

induction

infer

inline:trivial

java:class_kind:

This attribute annotates a module. Three suffixes are allowed: abstract, interface and class. This three attributes specify what kind of class the Java driver has to generate for the module, either a regular or an abstract class or an interface.

java:constructor

This attribute is used to mark functions

java:exception:

If a module is annotated with the attribute java:exception: exn-class, the Java driver translates it into a Java exception class. The exn-class part of the attribute indicates the parent class from which the generated class inherits. Actually exn-class is printed out as-is after the extends specifier of the generated class.

java:implements:

This attribute is applied to a module. Its suffix is a coma-separated list of identifiers of Java interfaces. From the driver point of view, the specified interfaces are just strings of characters and are printed out as-is in the generated Java code. The driver does not check if theses interfaces are actually implemented by the module; this verification is left to the Java compiler.

java:package:

If the attribute java:package: some.package annotates a module, the Java driver creates the expected class in the package some.package. In addition to the Java instruction package, the driver follows the usual convention by creating the .java file in the directory some/package/. The directory of the package is created relatively to the output directory specified with the option -o (see The extract Command).

java:visibility:public

java:visibility:package

java:visibility:private

By default, in the code generated by the Java driver, classes, instance variables and methods are declared public. The driver allows three attributes to change this default visibility: public, private and package. Note that visibility attributes are not checked by the driver.

If java:visibility:private is used to annotate a module, the generated class is declared private. Even if it is syntactically allowed, the specification of Java language does not allow private specifier for top-level classes.

By default, functions and types inherit the visibility attribute of the module. For instance if a module is declared with java:visibility:package then all functions, instance variables and Enum-types will be declared with package visibility. Each element of the module can be annotated with a different visibility attribute that replaces the default one.

Instance variables actually inherits the visibility attribute of the type that defines them. Yet, each instance variable may have its own visibility attribute.

model_trace

rewrite

stop_split

vc:annotation

This attribute is added by the VC generator, on the user input formulas which become goals to prove in the resulting VC. It should not be added manually.

vc:divergent

This attribute indicates whether VCs for termination should be generated. See Section 8.2.2 for details.

vc:keep_precondition

This attribute indicates whether preconditions of calls should be kept as assumptions for the program after the call. See Section 8.2.4 for details.

vc:sp

This attribute, put on a WhyML expression, locally switches the VC generator to the SP mode, for that expression. See Section 8.2.1 for details.

vc:white_box

This attribute is added by the Why3 parser for contract attached to an expression in WhyML code. Such a contract is indeed encoded by a local function with this attribute. It is for internal use only and should never be added manually.

vc:wp

This attribute, put on a WhyML expression, locally switches the VC generator to the WP mode, for that expression. See Section 8.2.1 for details.

12.8. Why3 Metas

compute_max_steps

keep:literal

realized_theory

rewrite

rewrite_def

vc:proved_wf

Declare a hypothesis as a proof of well-foundedness of a binary relation. See Section 8.2.3.

12.9. Debug Flags

The list of debug flags can be obtained using why3 --list-debug-flags. The following excerpt is the list of flags mentioned in this manual.

infer:loop

infer:print_ai_result

infer:print_cfg

print:inferred_invs

print:domains_loop

stack_trace

12.10. 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*, (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>

12.11. Structure of Counterexamples

Generated counterexamples can be exported in JSON format. The JSON output follows the JSON Schema given in share/ce-models.json and reproduced below.

{
    "$schema": "https://json-schema.org/draft/2020-12/schema",
    "title": "Model_parser.json_model",
    "type": "array",
    "items": {
        "type": "object",
        "properties": {
            "filename": {
                "type": "string"
            },
            "model": {
                "$comment": "list of counterexample model values, sorted by file and line number",
                "type": "array",
                "items": {
                    "type": "object",
                    "properties": {
                        "is_vc_line": {
                            "$comment": "true if the current line corresponds to the source code element from which the VC originates",
                            "type": "boolean"
                        },
                        "line": {
                            "type": "string"
                        },
                        "model_elements": {
                            "$comment": "see src/core/model_parser.mli for a description of the model_element type",
                            "type": "array",
                            "items": {
                                "type": "object",
                                "properties": {
                                    "attrs": {
                                        "type": "array",
                                        "items": {
                                            "type": "string"
                                        }
                                    },
                                    "kind": {
                                        "type": "string"
                                    },
                                    "location": {
                                        "$ref": "#/$defs/location"
                                    },
                                    "lsymbol": {
                                        "type": "object",
                                        "properties": {
                                            "name": {
                                                "type": "string"
                                            },
                                            "attrs": {
                                                "type": "array",
                                                "items": {
                                                    "type": "string"
                                                }
                                            },
                                            "loc": {
                                                "$ref": "#/$defs/location"
                                            }
                                        }
                                    },
                                    "value": {
                                        "type": "object",
                                        "properties": {
                                            "value_concrete_term": {
                                                "$ref": "#/$defs/concrete_term"
                                            },
                                            "value_term": {
                                                "$ref": "#/$defs/term"
                                            },
                                            "value_type": {
                                                "$ref": "#/$defs/type"
                                            }
                                        }
                                    }
                                }
                            }
                        }
                    }
                }
            }
        }
    },
    "$defs": {
        "location": {
            "oneOf": [
                {
                    "type": "string",
                    "pattern": "^NO_LOC$"
                },
                {
                    "type": "object",
                    "properties": {
                        "file-name": {
                            "type": "string"
                        },
                        "start-line": {
                            "type": "number"
                        },
                        "start-char": {
                            "type": "number"
                        },
                        "end-line": {
                            "type": "number"
                        },
                        "end-char": {
                            "type": "number"
                        }
                    }
                }
            ]
        },
        "type": {
            "oneOf": [
                {
                    "type": "null"
                },
                {
                    "type": "object",
                    "properties": {
                        "Tyvar": {
                            "type": "string"
                        }
                    },
                    "required": ["Tyvar"]
                },
                {
                    "type": "object",
                    "properties": {
                        "Tyapp": {
                            "type": "object",
                            "properties": {
                                "ty_symbol": {
                                    "type": "string"
                                },
                                "ty_args": {
                                    "type": "array",
                                    "items": {
                                        "$ref": "#"
                                    }
                                }
                            },
                            "required": ["ty_symbol","ty_args"]
                        }
                    },
                    "required": ["Tyapp"]
                }
            ]
        },
        "vsymbol": {
            "type": "object",
            "properties": {
                "vs_name": {
                    "type": "string"
                },
                "vs_type": {
                    "$ref": "#/$defs/type"
                }
            },
            "required": ["vs_name","vs_type"]
        },
        "term": {
            "oneOf": [
                {
                    "type": "object",
                    "properties": {
                        "Tvar": {
                            "$ref": "#/$defs/vsymbol"
                        }
                    },
                    "required": ["Tvar"]
                },
                {
                    "type": "object",
                    "properties": {
                        "Tconst": {
                            "type": "object",
                            "properties": {
                                "const_type": {
                                    "type": "string"
                                },
                                "const_value": {
                                    "type": "string"
                                }
                            },
                            "required": ["const_type","const_value"]
                        }
                    },
                    "required": ["Tconst"]
                },
                {
                    "type": "object",
                    "properties": {
                        "Tapp": {
                            "type": "object",
                            "properties": {
                                "app_ls": {
                                    "type": "string"
                                },
                                "app_args": {
                                    "type": "array",
                                    "items": {
                                        "$ref": "#"
                                    }
                                }
                            },
                            "required": ["app_ls","app_args"]
                        }
                    },
                    "required": ["Tapp"]
                },
                {
                    "type": "object",
                    "properties": {
                        "Tif": {
                            "type": "object",
                            "properties": {
                                "if": {
                                    "$ref": "#"
                                },
                                "then": {
                                    "$ref": "#"
                                },
                                "else": {
                                    "$ref": "#"
                                }
                            },
                            "required": ["if","then","else"]
                        }
                    },
                    "required": ["Tif"]
                },
                {
                    "type": "object",
                    "properties": {
                        "Teps": {
                            "type": "object",
                            "properties": {
                                "eps_vs": {
                                    "$ref": "#/$defs/vsymbol"
                                },
                                "eps_t": {
                                    "$ref": "#"
                                }
                            },
                            "required": ["eps_vs","eps_t"]
                        }
                    },
                    "required": ["Teps"]
                },
                {
                    "type": "object",
                    "properties": {
                        "Tfun": {
                            "type": "object",
                            "properties": {
                                "fun_args": {
                                    "type": "array",
                                    "items": {
                                        "$ref": "#/$defs/vsymbol"
                                    }
                                },
                                "fun_body": {
                                    "$ref": "#"
                                }
                            },
                            "required": ["fun_args","fun_body"]
                        }
                    },
                    "required": ["Tfun"]
                },
                {
                    "type": "object",
                    "properties": {
                        "Tquant": {
                            "type": "object",
                            "properties": {
                                "quant": {
                                    "type": "string"
                                },
                                "quant_vs": {
                                    "type": "array",
                                    "items": {
                                        "$ref": "#/$defs/vsymbol"
                                    }
                                },
                                "quant_t": {
                                    "$ref": "#"
                                }
                            },
                            "required": ["quant","quant_vs","quant_t"]
                        }
                    },
                    "required": ["Tquant"]
                },
                {
                    "type": "object",
                    "properties": {
                        "Tbinop": {
                            "type": "object",
                            "properties": {
                                "binop": {
                                    "type": "string"
                                },
                                "binop_t1": {
                                    "$ref": "#"
                                },
                                "binop_t2": {
                                    "$ref": "#"
                                }
                            },
                            "required": ["binop","binop_t1","binop_t2"]
                        }
                    },
                    "required": ["Tbinop"]
                },
                {
                    "type": "object",
                    "properties": {
                        "Tnot": {
                            "$ref": "#"
                        }
                    },
                    "required": ["Tnot"]
                },
                {
                    "type": "string",
                    "pattern": "^Ttrue$"
                },
                {
                    "type": "string",
                    "pattern": "^Tfalse$"
                },
                {
                    "type": "object",
                    "properties": {
                        "Tlet": {
                            "type": "string"
                        }
                    },
                    "required": ["Tlet"]
                },
                {
                    "type": "object",
                    "properties": {
                        "Tcase": {
                            "type": "string"
                        }
                    },
                    "required": ["Tcase"]
                }
            ]
        },
        "concrete_bv": {
            "type": "object",
            "properties": {
                "bv_value_as_decimal": {
                    "type": "string"
                },
                "bv_length": {
                    "type": "number"
                },
                "bv_verbatim": {
                    "type": "string"
                }
            },
            "required": ["bv_value_as_decimal","bv_length","bv_verbatim"]
        },
        "concrete_real": {
            "type": "object",
            "properties": {
                "real_value": {
                    "type": "string"
                },
                "real_verbatim": {
                    "type": "string"
                }
            },
            "required": ["real_value","real_verbatim"]
        },
        "concrete_term": {
            "oneOf": [
                {
                    "type": "object",
                    "properties": {
                        "type": {
                            "type": "string",
                            "pattern": "^Var$"
                        },
                        "val": {
                            "type": "string"
                        }
                    },
                    "required": ["type","val"]
                },
                {
                    "type": "object",
                    "properties": {
                        "type": {
                            "type": "string",
                            "pattern": "^Boolean$"
                        },
                        "val": {
                            "type": "boolean"
                        }
                    },
                    "required": ["type","val"]
                },
                {
                    "type": "object",
                    "properties": {
                        "type": {
                            "type": "string",
                            "pattern": "^String$"
                        },
                        "val": {
                            "type": "string"
                        }
                    },
                    "required": ["type","val"]
                },
                {
                    "type": "object",
                    "properties": {
                        "type": {
                            "type": "string",
                            "pattern": "^Integer$"
                        },
                        "val": {
                            "type": "object",
                            "properties": {
                                "int_value": {
                                    "type": "string"
                                },
                                "int_verbatim": {
                                    "type": "string"
                                }
                            },
                            "required": ["int_value","int_verbatim"]
                        }
                    },
                    "required": ["type","val"]
                },
                {
                    "type": "object",
                    "properties": {
                        "type": {
                            "type": "string",
                            "pattern": "^Real$"
                        },
                        "val": {
                            "$ref": "#/$defs/concrete_real"
                        }
                    },
                    "required": ["type","val"]
                },
                {
                    "type": "object",
                    "properties": {
                        "type": {
                            "type": "string",
                            "pattern": "^BitVector$"
                        },
                        "val": {
                            "$ref": "#/$defs/concrete_bv"
                        }
                    },
                    "required": ["type","val"]
                },
                {
                    "type": "object",
                    "properties": {
                        "type": {
                            "type": "string",
                            "pattern": "^Fraction$"
                        },
                        "val": {
                            "type": "object",
                            "properties": {
                                "frac_num": {
                                    "$ref": "#/$defs/concrete_real"
                                },
                                "frac_den": {
                                    "$ref": "#/$defs/concrete_real"
                                },
                                "frac_verbatim": {
                                    "type": "string"
                                }
                            },
                            "required": ["frac_num","frac_den","frac_verbatim"]
                        }
                    },
                    "required": ["type","val"]
                },
                {
                    "type": "object",
                    "properties": {
                        "type": {
                            "type": "string",
                            "pattern": "^Float$"
                        },
                        "val": {
                            "oneOf": [
                                {
                                    "type": "object",
                                    "properties": {
                                        "float_type": {
                                            "type": "string",
                                            "pattern": "^Infinity"
                                        }
                                    },
                                    "required": ["float_type"]
                                },
                                {
                                    "type": "object",
                                    "properties": {
                                        "float_type": {
                                            "type": "string",
                                            "pattern": "^Plus_zero"
                                        }
                                    },
                                    "required": ["float_type"]
                                },
                                {
                                    "type": "object",
                                    "properties": {
                                        "float_type": {
                                            "type": "string",
                                            "pattern": "^Minus_zero"
                                        }
                                    },
                                    "required": ["float_type"]
                                },
                                {
                                    "type": "object",
                                    "properties": {
                                        "float_type": {
                                            "type": "string",
                                            "pattern": "^NaN"
                                        }
                                    },
                                    "required": ["float_type"]
                                },
                                {
                                    "type": "object",
                                    "properties": {
                                        "float_type": {
                                            "type": "string",
                                            "pattern": "^Float_value"
                                        },
                                        "float_sign": {
                                            "$ref": "#/$defs/concrete_bv"
                                        },
                                        "float_exp": {
                                            "$ref": "#/$defs/concrete_bv"
                                        },
                                        "float_mant": {
                                            "$ref": "#/$defs/concrete_bv"
                                        },
                                        "float_hex": {
                                            "type": "string"
                                        }
                                    },
                                    "required": ["float_type","float_sign","float_exp","float_mant","float_hex"]
                                }
                            ]
                        }
                    },
                    "required": ["type","val"]
                },
                {
                    "type": "object",
                    "properties": {
                        "type": {
                            "type": "string",
                            "pattern": "^Apply$"
                        },
                        "val": {
                            "type": "object",
                            "properties": {
                                "app_ls": {
                                    "type": "string"
                                },
                                "app_args": {
                                    "type": "array",
                                    "items": {
                                        "$ref": "#"
                                    }
                                }
                            },
                            "required": ["app_ls","app_args"]
                        }
                    },
                    "required": ["type","val"]
                },
                {
                    "type": "object",
                    "properties": {
                        "type": {
                            "type": "string",
                            "pattern": "^If$"
                        },
                        "val": {
                            "type": "object",
                            "properties": {
                                "if": {
                                    "$ref": "#"
                                },
                                "then": {
                                    "$ref": "#"
                                },
                                "else": {
                                    "$ref": "#"
                                }
                            },
                            "required": ["if","then","else"]
                        }
                    },
                    "required": ["type","val"]
                },
                {
                    "type": "object",
                    "properties": {
                        "type": {
                            "type": "string",
                            "pattern": "^Epsilon$"
                        },
                        "val": {
                            "type": "object",
                            "properties": {
                                "eps_var": {
                                    "type": "string"
                                },
                                "eps_t": {
                                    "$ref": "#"
                                }
                            },
                            "required": ["eps_var","eps_t"]
                        }
                    },
                    "required": ["type","val"]
                },
                {
                    "type": "object",
                    "properties": {
                        "type": {
                            "type": "string",
                            "pattern": "^Function$"
                        },
                        "val": {
                            "type": "object",
                            "properties": {
                                "fun_args": {
                                    "type": "array",
                                    "items": {
                                        "type": "string"
                                    }
                                },
                                "fun_body": {
                                    "$ref": "#"
                                }
                            },
                            "required": ["fun_args","fun_body"]
                        }
                    },
                    "required": ["type","val"]
                },
                {
                    "type": "object",
                    "properties": {
                        "type": {
                            "type": "string",
                            "pattern": "^Quant$"
                        },
                        "val": {
                            "type": "object",
                            "properties": {
                                "quant": {
                                    "type": "string"
                                },
                                "quant_vars": {
                                    "type": "array",
                                    "items": {
                                        "type": "string"
                                    }
                                },
                                "quant_t": {
                                    "$ref": "#"
                                }
                            },
                            "required": ["quant","quant_vars","quant_t"]
                        }
                    },
                    "required": ["type","val"]
                },
                {
                    "type": "object",
                    "properties": {
                        "type": {
                            "type": "string",
                            "pattern": "^Binop$"
                        },
                        "val": {
                            "type": "object",
                            "properties": {
                                "binop": {
                                    "type": "string"
                                },
                                "binop_t1": {
                                    "$ref": "#"
                                },
                                "binop_t2": {
                                    "$ref": "#"
                                }
                            },
                            "required": ["binop","binop_t1","binop_t2"]
                        }
                    },
                    "required": ["type","val"]
                },
                {
                    "type": "object",
                    "properties": {
                        "type": {
                            "type": "string",
                            "pattern": "^Not$"
                        },
                        "val": {
                            "$ref": "#"
                        }
                    },
                    "required": ["type","val"]
                },
                {
                    "type": "object",
                    "properties": {
                        "type": {
                            "type": "string",
                            "pattern": "^FunctionLiteral$"
                        },
                        "val": {
                            "type": "object",
                            "properties": {
                                "funliteral_elts": {
                                    "type": "array",
                                    "items": {
                                        "type": "object",
                                        "properties": {
                                            "indice": {
                                                "$ref": "#"
                                            },
                                            "value": {
                                                "$ref": "#"
                                            }
                                        },
                                        "required": ["indice","value"]
                                    }
                                },
                                "funliteral_others": {
                                    "$ref": "#"
                                }
                            },
                            "required": ["array_elts","array_others"]
                        }
                    },
                    "required": ["type","val"]
                },
                {
                    "type": "object",
                    "properties": {
                        "type": {
                            "type": "string",
                            "pattern": "^Record$"
                        },
                        "val": {
                            "type": "array",
                            "items": {
                                "type": "object",
                                "properties": {
                                    "field": {
                                        "type": "string"
                                    },
                                    "value":{
                                        "$ref": "#"
                                    }
                                },
                                "required": ["field","value"]
                            }
                        }
                    },
                    "required": ["type","val"]
                },
                {
                    "type": "object",
                    "properties": {
                        "type": {
                            "type": "string",
                            "pattern": "^Proj$"
                        },
                        "val": {
                            "type": "object",
                            "properties": {
                                "proj_name": {
                                    "type": "string"
                                },
                                "proj_value":{
                                    "$ref": "#"
                                }
                            },
                            "required": ["proj_name","proj_value"]
                        }
                    },
                    "required": ["type","val"]
                }
            ]
        }
    }
}

12.12. Developer Documentation

12.12.1. Updating messages for syntax errors

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 9-12:
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 --interpret-error 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 --interpret-error 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 non-reserved uncapitalized identifier (token LIDENT_NQ), found "$0"