This chapter gives the grammar and semantics for Why3 and WhyML input files.
Lexical conventions are common to Why3 and WhyML.
Comments are enclosed by (* and *) and can be nested.
Strings are enclosed in double quotes ("). Double quotes can be
escaped in strings using the backslash character (\).
The other special sequences are \n for line feed and \t
for horizontal tab.
In the following, strings are referred to with the non-terminal
string.
Identifiers are non-empty sequences of characters among letters, digits, the underscore character and the quote character. They cannot start with a digit or a quote.
The syntax distinguishes identifiers that start with a lowercase or an uppercase letter (resp. lident and uident), and similarly, lowercase and uppercase qualified identifiers.
The restricted classes of identifiers denoted by lident-nq and uident-nq correspond to identifiers where the quote character cannot be followed by a letter. Identifiers where a quote is followed by a letter are reserved and cannot be used as identifier for declarations introduced by the user (see Section 7.2.4).
The syntax for constants is given in Figure 7.1. Integer and real constants have arbitrary precision. Integer constants may be given in base 16, 10, 8 or 2. Real constants may be given in base 16 or 10.
Figure 7.1: Syntax for constants.
Prefix and infix operators are built from characters organized in four categories (op-char-1 to op-char-4).
Infix operators are classified into 4 categories, according to the characters they are built from:
Identifiers, terms, formulas, program expressions can all be labeled, either with a string, or with a location tag.
A location tag consists of a file name, a line number, and starting and ending characters.
The syntax for terms is given in Figure 7.2. The various constructs have the following priorities and associativities, from lowest to greatest priority:
| construct | associativity |
| if then else / let in | – |
| label | – |
| cast | – |
| infix-op level 1 | left |
| infix-op level 2 | left |
| infix-op level 3 | left |
| infix-op level 4 | left |
| prefix-op | – |
| function application | left |
| brackets / ternary brackets | – |
| bang-op | – |
Note the curryfied syntax for function application, though partial application is not allowed (rejected at typing).
Figure 7.2: Syntax for terms.
The syntax for type expressions is the following:
| type | ::= | lqualid type* | type symbol |
| ∣ | ' lident | type variable | |
| ∣ | () | empty tuple type | |
| ∣ | ( type (, type)+ ) | tuple type | |
| ∣ | ( type ) | parentheses |
Built-in types are int, real, and tuple types. Note that the syntax for type expressions notably differs from the usual ML syntax (e.g. the type of polymorphic lists is written list ’a, not ’a list).
The syntax for formulas is given Figure 7.3. The various constructs have the following priorities and associativities, from lowest to greatest priority:
| construct | associativity |
| if then else / let in | – |
| label | – |
| -> / <-> | right |
| by / so | right |
\/ / || | right |
/\ / && | right |
| not | – |
| infix level 1 | left |
| infix level 2 | left |
| infix level 3 | left |
| infix level 4 | left |
| prefix | – |
Note that infix symbols of level 1 include equality (=) and disequality (<>).
Figure 7.3: Syntax for formulas.
Notice that there are two symbols for the conjunction: /\
and &&, and similarly for disjunction. They are logically
equivalent, but may be treated slightly differently by some
transformations. For instance, split transforms the goal
A /\ B into subgoals A and B, whereas it transforms
A && B into subgoals A and A -> B. Similarly, it
transforms not (A || B) into subgoals not A and
not ((not A) /\ B).
The by/so connectives are proof indications. They are
logically equivalent to their first argument, but may affect the result
of some transformations. For instance, the split_goal
transformations interpret those connectives as introduction of logical cuts
(see 10.5.5 for details).
The syntax for theories is given on Figure 7.4 and 7.5.
Figure 7.4: Syntax for theories (part 1).
Figure 7.5: Syntax for theories (part 2).
TO BE COMPLETED
TO BE COMPLETED
A declaration of the form type r = < range a b > defines a type that projects into the integer range [a,b]. Note that in order to make such a declaration the theory int.Int must be imported.
Why3 let you cast an integer literal in a range type (e.g. (42:r)) and will check at typing that the literal is in range. Defining such a range type r automatically introduces the following:
| function r'int r : int constant r'maxInt : int constant r'minInt : int |
The function r’int projects a term of type r to its integer value. The two constants represent the high bound and low bound of the range respectively.
Unless specified otherwise with the meta "keep:literal" on r, the transformation eliminate_literal introduces an axiom
| axiom r'axiom : forall i:r. r'minInt <= r'int i <= r'maxInt |
and replaces all casts of the form (42:r) with a constant and an axiom as in:
| constant rliteral7 : r axiom rliteral7_axiom : r'int rliteral7 = 42 |
This type is used in the standard library in the theories bv.BV8, bv.BV16, bv.BV32, bv.BV64.
A declaration of the form type f = < float eb sb > defines a type of floating-point numbers as specified by the IEEE-754 standard [1]. Here the literal eb represents the number of bits in the exponent and the literal sb the number of bits in the significand (including the hidden bit). Note that in order to make such a declaration the theory real.Real must be imported.
Why3 let you cast a real literal in a float type (e.g. (0.5:f)) and will check at typing that the literal is representable in the format. Note that Why3 do not implicitly round a real literal when casting to a float type, it refuses the cast if the literal is not representable.
Defining such a type f automatically introduces the following:
| predicate f'isFinite f function f'real f : real constant f'eb : int constant f'sb : int |
As specified by the IEEE standard, float formats includes infinite values and also a special NaN value (Not-a-Number) to represent results of undefined operations such as 0/0. The predicate f’isFinite indicates whether its argument is neither infinite nor NaN. The function f’real projects a finite term of type f to its real value, its result is not specified for non finite terms.
Unless specified otherwise with the meta "keep:literal" on f, the transformation eliminate_literal will introduce an axiom
| axiom f'axiom : forall x:f. f'isFinite x -> -. max_real <=. f'real x <=. max_real |
where max_real is the value of the biggest finite float in the specified format. The transformation also replaces all casts of the form (0.5:f) with a constant and an axiom as in:
| constant fliteral42 : f axiom fliteral42_axiom : f'real fliteral42 = 0.5 /\ f'isFinite fliteral42 |
This type is used in the standard library in the theories ieee_float.Float32 and ieee_float.Float64.
A Why3 input file is a (possibly empty) list of theories.
The syntax for specification clauses in programs is given in Figure 7.6.
Figure 7.6: Specification clauses in programs.
Within specifications, terms are extended with new constructs
old and at:
Within a postcondition, old t refers to the value of term t
in the prestate. Within the scope of a code mark L,
the term at t 'L refers to the value of term t at the program
point corresponding to L.
The syntax for program expressions is given in Figure 7.7 and Figure 7.8.
Figure 7.7: Syntax for program expressions (part 1).
Figure 7.8: Syntax for program expressions (part 2).
In applications, arguments are evaluated from right to left.
This includes applications of infix operators, with the only exception of
lazy operators && and || that evaluate from left to
right, lazily.
The syntax for modules is given in Figure 7.9.
Figure 7.9: Syntax for modules.
Any declaration which is accepted in a theory is also accepted in a module. Additionally, modules can introduce record types with mutable fields and declarations which are specific to programs (global variables, functions, exceptions).
A WhyML input file is a (possibly empty) list of theories and modules.
A theory defined in a WhyML file can only be used within that file. If a theory is supposed to be reused from other files, be they Why3 or WhyML files, it should be defined in a Why3 file.
The Why3 standard library provides general-purpose theories and modules, to be used in logic and/or programs. It can be browsed on-line at http://why3.lri.fr/stdlib/. Each file contains one or several theories and/or modules. To use or clone a theory/module T from file file, use the syntax file.T, since file is available in Why3’s default load path. For instance, the theory of integers and the module of references are imported as follows:
| use import int.Int use import ref.Ref |