Previous Up Next

Chapter 6  Language Reference

In this chapter, we describe the syntax and semantics of WhyML.

6.1  Lexical Conventions

Blank characters are space, horizontal tab, carriage return, and line feed. Blanks separate lexemes but are otherwise ignored. Comments are enclosed by (* and *) and can be nested. Note that (*) does not start a comment.

Strings are enclosed in double quotes ("). Double quotes can be escaped inside strings using the backslash character (\). The other special sequences are \n for line feed and \t for horizontal tab. In the following, strings are referred to with the non-terminal string.

The syntax for numerical constants is given by the following rules:

digit::=09
hex-digit::=09afAF
oct-digit::=07
bin-digit::=01
integer::=digit (digit_)* 
 (0x0X) hex-digit (hex-digit_)* 
 (0o0O) oct-digit (oct-digit_)* 
 (0b0B) bin-digit (bin-digit_)* 
real::=digit+ exponent 
 digit+ . digit* exponent? 
 digit* . digit+ exponent? 
 (0x0X) hex-digit+ h-exponent 
 (0x0X) hex-digit+ . hex-digit* h-exponent? 
 (0x0X) hex-digit* . hex-digit+ h-exponent? 
exponent::=(eE) (-+)? digit+
h-exponent::=(pP) (-+)? digit+

Integer and real constants have arbitrary precision. Integer constants can be given in base 10, 16, 8 or 2. Real constants can be given in base 10 or 16. Notice that the exponent in hexadecimal real constants is written in base 10.

Identifiers are composed of letters, digits, underscores, and primes. The syntax distinguishes identifiers that start with a lowercase letter or an underscore (lident), identifiers that start with an uppercase letter (uident), and identifiers that start with a prime (qident, used exclusively for type variables):

alpha::=azAZ
suffix::=alphadigit'_
lident::=(az) suffix*_ suffix+
uident::=(AZ) suffix*
qident::=' (az) suffix*

Identifiers that contain a prime followed by a letter, such as int32’max, are reserved for symbols introduced by Why3 and cannot be used for user-defined symbols.

In order to refer to symbols introduced in different namespaces (scopes), we can put a dot-separated “qualifier prefix” in front of an identifier (e.g. Map.S.get). This allows us to use the symbol get from the scope Map.S without importing it in the current namespace:

qualifier::=(uident .)+
lqualid::=qualifier? lident
uqualid::=qualifier? uident

All parenthesised expressions in WhyML (types, patterns, logical terms, program expressions) admit a qualifier before the opening parenthesis, e.g. Map.S.(get m i). This imports the indicated scope into the current namespace during the parsing of the expression under the qualifier. For the sake of convenience, the parentheses can be omitted when the expression itself is enclosed in parentheses, square brackets or curly braces.

Prefix and infix operators are built from characters organized in four precedence groups (op-char-1 to op-char-4), with optional primes at the end:

op-char-1::==<>~ 
op-char-2::=+- 
op-char-3::=*/\% 
op-char-4::=!$&?@^.:|# 
op-char-1234::=op-char-1 ∣ op-char-2 ∣ op-char-3 ∣ op-char-4 
op-char-234::=op-char-2 ∣ op-char-3 ∣ op-char-4 
op-char-34::=op-char-3 ∣ op-char-4 
infix-op-1::=op-char-1234* op-char-1 op-char-1234* '* 
infix-op-2::=op-char-234* op-char-2 op-char-234* '* 
infix-op-3::=op-char-34* op-char-3 op-char-34* '* 
infix-op-4::=op-char-4+ '* 
prefix-op::=op-char-1234+ '* 
tight-op::=(!?) op-char-4* '*

Infix operators from a high-numbered group bind stronger than the infix operators from a low-numbered group. For example, infix operator .*. from group 3 would have a higher precedence than infix operator ->- from group 1. Prefix operators always bind stronger than infix operators. The so-called “tight operators” are prefix operators that have even higher precedence than the juxtaposition (application) operator, allowing us to write expressions like inv !x without parentheses.

Finally, any identifier, term, formula, or expression in a WhyML source can be tagged either with a string attribute or a location:

attribute::=[@ ... ] attribute
 [# string digit+ digit+ digit+ ] location

An attribute cannot contain newlines or closing square brackets; leading and trailing spaces are ignored. A location consists of a file name in double quotes, a line number, and starting and ending character positions.

6.2  Type expressions

WhyML features an ML-style type system with polymorphic types, variants (sum types), and records that can have mutable fields. The syntax for type expressions is the following:

type::=lqualid type-arg+ polymorphic type symbol
 type -> type mapping type (right-associative)
 type-arg
type-arg::=lqualid monomorphic type symbol (sort)
 qident type variable
 () unit type
 ( type (, type)+ ) tuple type
 { type } snapshot type
 qualifier? ( type ) type in a scope

Built-in types are int (arbitrary precision integers), real (real numbers), bool, the arrow type (also called the mapping type), and the tuple types. The empty tuple type is also called the unit type and can be written as unit.

Note that the syntax for type expressions notably differs from the usual ML syntax. In particular, the type of polymorphic lists is written list ’a, and not ’a list.

Snapshot types are specific to WhyML, they denote the types of ghost values produced by pure logical functions in WhyML programs. A snapshot of an immutable type is the type itself: thus, {int} is the same as int and {list ’a} is the same as list ’a. A snapshot of a mutable type, however, represents a snapshot value which cannot be modified anymore. Thus, a snapshot array a of type {array int} can be read from (a[42] is accepted) but not written into (a[42] <- 0 is rejected). Generally speaking, a program function that expects an argument of a mutable type will accept an argument of the corresponding snapshot type as long as it is not modified by the function.

6.3  Logical expressions: terms and formulas


term::=integer integer constant
 real real constant
 truefalse Boolean constant
 () empty tuple
 qualid qualified identifier
 qualifier? ( term ) term in a scope
 qualifier? begin term end idem
 tight-op term tight operator
 { term-field+ } record
 { term with term-field+ } record update
 term . lqualid record field access
 term [ term ] '* collection access
 term [ term <- term ] '* collection update
 term [ term .. term ] '* collection slice
 term [ term .. ] '* right-open slice
 term [ .. term ] '* left-open slice
 term term+ application
 prefix-op term prefix operator
 term infix-op-4 term infix operator 4
 term infix-op-3 term infix operator 3
 term infix-op-2 term infix operator 2
 term at uident past value
 old term initial value
 term infix-op-1 term infix operator 1
 ... continued in Fig. 6.2
term-field::=lqualid = term ; field = value
qualid::=qualifier? (lident-extuident) qualified identifier
lident-ext::=lident lowercase identifier
 ( ident-op ) operator identifier
 ( ident-op ) (_') alpha suffix* associated identifier
ident-op::=infix-op-1 infix operator 1
 infix-op-2 infix operator 2
 infix-op-3 infix operator 3
 infix-op-4 infix operator 4
 prefix-op _ prefix operator
 tight-op _? tight operator
 [ ] '* collection access
 [ <- ] '* collection update
 [ ] '* <- in-place update
 [ .. ] '* collection slice
 [ _ .. ] '* right-open slice
 [ .. _ ] '* left-open slice
Figure 6.1: WhyML terms (part I).


term::=... see Fig. 6.1
 not term negation
 term /\ term conjunction
 term && term asymmetric conjunction
 term \/ term disjunction
 term || term asymmetric disjunction
 term by term proof indication
 term so term consequence indication
 term -> term implication
 term <-> term equivalence
 term : type type cast
 attribute+ term attributes
 term (, term)+ tuple
 quantifier quant-vars triggers? . term quantifier
 ... continued in Fig. 6.3
quantifier::=forallexists
quant-vars::=quant-cast (, quant-cast)*
quant-cast::=binder+ (: type)?
binder::=_bound-var
bound-var::=lident attribute*
triggers::=[ trigger (| trigger)* ] 
trigger::=term (, term)*
Figure 6.2: WhyML terms (part II).

A significant part of a typical WhyML source file is occupied by non-executable logical content intended for specification and proof: function contracts, assertions, definitions of logical functions and predicates, axioms, lemmas, etc.

Logical expressions are called terms. Boolean terms are called formulas. Internally, Why3 distinguishes the proper formulas (produced by predicate symbols, propositional connectives and quantifiers) and the terms of type bool (produced by Boolean variables and logical functions that return bool). However, this distinction is not enforced on the syntactical level, and Why3 will perform the necessary conversions behind the scenes.

The syntax of WhyML terms is given in Figures 6.1-6.3. The constructions are listed in the order of decreasing precedence. For example, as was mentioned above, tight operators have the highest precedence of all operators, so that -p.x denotes the negation of the record field p.x, whereas !p.x denotes the field x of a record stored in the reference p.

An operator in parentheses acts as an identifier referring to that operator, for example, in a definition. To distinguish between prefix and infix operators, an underscore symbol is appended at the end: for example, (-) refers to the binary subtraction and (-_) to the unary negation. Tight operators cannot be used as infix operators, and thus do not require disambiguation.

In addition to prefix and infix operators, WhyML supports several mixfix bracket operators to manipulate various collection types: dictionaries, arrays, sequences, etc. Bracket operators do not have any predefined meaning and may be used to denote access and update operations for various user-defined collection types. We can introduce multiple bracket operations in the same scope by disambiguating them with primes after the closing bracket: for example, a[i] may denote array access and s[i]’ sequence access. Notice that the in-place update operator a[i] <- v cannot be used inside logical terms: all effectful operations are restricted to program expressions. To represent the result of a collection update, we should use a pure logical update operator a[i <- v] instead.

WhyML supports “associated” names for operators, obtained by adding a suffix after the parenthesised operator name. For example, an axiom that represents the specification of the infix operator (+) may be called (+)’spec or (+)_spec. As with normal identifiers, names with a letter after a prime, such as (+)’spec, can only be introduced by Why3, and not by the user in a WhyML source.

The at and old operators are used inside postconditions and assertions to refer to the value of a mutable program variable at some past moment of execution (see the next section for details). These operators have higher precedence than the infix operators from group 1 (infix-op-1): old i > j is parsed as (old i) > j and not as old (i > j).

Infix operators from groups 2-4 are left-associative. Infix operators from group 1 are non-associative and can be chained. For example, the term 0 <= i < j < length a is parsed as the conjunction of three inequalities 0 <= i, i < j, and j < length a.

As with normal identifiers, we can put a qualifier over a parenthesised operator, e.g. Map.S.([]) m i. Also, as noted above, a qualifier can be put over a parenthesised term, and the parentheses can be omitted if the term is a record or a record update.

The propositional connectives in WhyML formulas are listed in Figure 6.2. The non-standard connectives — asymmetric conjunction (&&), asymmetric disjunction (||), proof indication (by), and consequence indication (so) — are used to control the goal-splitting transformations of Why3 and provide integrated proofs for WhyML assertions, postconditions, lemmas, etc. The semantics of these connectives follows the rules below:

For example, full splitting of the goal (A by (exists x. B so C)) && D produces four subgoals: exists x. B (the premise is verified), forall x. B -> C (the premise justifies the conclusion), (exists x. B /\ C) -> A (the proof justifies the affirmation), and finally, A -> D (the proof of A is discarded and A is used to prove D).

The behaviour of the splitting transformations is further controlled by attributes [@stop_split] and [@case_split]. Consult Section 9.5.5 for details.

Among the propositional connectives, not has the highest precedence, && has the same precedence as /\ (weaker than negation), || has the same precedence as \/ (weaker than conjunction), by, so, ->, and <-> all have the same precedence (weaker than disjunction). All binary connectives except equivalence are right-associative. Equivalence is non-associative and is chained instead: A <-> B <-> C is transformed into a conjunction of A <-> B and B <-> C. To reduce ambiguity, WhyML forbids to place a non-parenthesised implication at the right-hand side of an equivalence: A <-> B -> C is rejected.


term::=... see Fig. 6.1 and 6.2
 if term then term else term conditional
 match term with term-case+ end pattern matching
 let pattern = term in term let-binding
 let symbol param+ = term in term mapping definition
 fun param+ -> term unnamed mapping
term-case::=| pattern -> term
pattern::=binder variable or ‘_
 () empty tuple
 { (lqualid = pattern ;)+ } record pattern
 uqualid pattern* constructor
 ghost pattern ghost sub-pattern
 pattern as ghost? bound-var named sub-pattern
 pattern , pattern tuple pattern
 pattern | pattern “or” pattern
 qualifier? ( pattern ) pattern in a scope
symbol::=lident-ext attribute* user-defined symbol
param::=type-arg unnamed typed
 binder (un)named untyped
 ( ghost? type ) unnamed typed
 ( ghost? binder ) (un)named untyped
 ( ghost? binder+ : type ) multi-variable typed
Figure 6.3: WhyML terms (part III).

In Figure 6.3, we find the more advanced term constructions: conditionals, let-bindings, pattern matching, and local function definitions, either via the let-in construction or the fun keyword. The pure logical functions defined in this way are called mappings; they are first-class values of “arrow” type τ1 -> τ2.

The patterns are similar to those of OCaml, though the when clauses and numerical constants are not supported. Unlike in OCaml, as binds stronger than the comma: in the pattern (p1,p2 as x), variable x is bound to the value matched by pattern p2. Also notice the closing end after the match-with term. A let-in construction with a non-trivial pattern is translated as a match-with term with a single branch.

Inside logical terms, pattern matching must be exhaustive: WhyML rejects a term like let Some x = o in …, where o is a variable of an option type. In program expressions, non-exhaustive pattern matching is accepted and a proof obligation is generated to show that the values not covered cannot occur in execution.

The syntax of parameters in user-defined operations—first-class mappings, top-level logical functions and predicates, and program functions—is rather flexible in WhyML. Like in OCaml, the user can specify the name of a parameter without its type and let the type be inferred from the definition. Unlike in OCaml, the user can also specify the type of the parameter without giving its name. This is convenient when the symbol declaration does not provide the actual definition or specification of the symbol, and thus only the type signature is of relevance. For example, one can declare an abstract binary function that adds an element to a set simply by writing function add ’a (set ’a) : set ’a. A standalone non-qualified lowercase identifier without attributes is treated as a type name when the definition is not provided, and as a parameter name otherwise.

Ghost patterns, ghost variables after as, and ghost parameters in function definitions are only used in program code, and not allowed in logical terms.

6.4  Program expressions

The syntax of program expressions is given in Figures 6.4-6.5. As before, the constructions are listed in the order of decreasing precedence. The rules for tight, prefix, infix, and bracket operators are the same as for logical terms. In particular, the infix operators from group 1 can be chained. Notice that binary operators && and || denote here the usual lazy conjunction and disjunction, respectively.


expr::=integer integer constant
 real real constant
 truefalse Boolean constant
 () empty tuple
 qualid identifier in a scope
 qualifier? ( expr ) expression in a scope
 qualifier? begin expr end idem
 tight-op expr tight operator
 { (lqualid = expr ;)+ } record
 { expr with (lqualid = expr ;)+ } record update
 expr . lqualid record field access
 expr [ expr ] '* collection access
 expr [ expr <- expr ] '* collection update
 expr [ expr .. expr ] '* collection slice
 expr [ expr .. ] '* right-open slice
 expr [ .. expr ] '* left-open slice
 expr expr+ application
 prefix-op expr prefix operator
 expr infix-op-4 expr infix operator 4
 expr infix-op-3 expr infix operator 3
 expr infix-op-2 expr infix operator 2
 expr infix-op-1 expr infix operator 1
 not expr negation
 expr && expr lazy conjunction
 expr || expr lazy disjunction
 expr : type type cast
 attribute+ expr attributes
 ghost expr ghost expression
 expr (, expr)+ tuple
 expr <- expr assignment
 ... continued in Fig. 6.5
Figure 6.4: WhyML program expressions (part I).

Keyword ghost marks the expression as ghost code added for verification purposes. Ghost code is removed from the final code intended for execution, and thus cannot affect the computation of the program results nor the content of the observable memory.

Assignment updates in place a mutable record field or an element of a collection. The former can be done simultaneously on a tuple of values: x.f, y.g <- a, b. The latter form, a[i] <- v, amounts to a call of the ternary bracket operator ([]<-) and cannot be used in a multiple assignment.


expr::=... see Fig. 6.4
 expr spec+ added specification
 if expr then expr (else expr)? conditional
 match expr with (| pattern -> expr)+ end pattern matching
 qualifier? begin spec+ expr end abstract block
 expr ; expr sequence
 let pattern = expr in expr let-binding
 let fun-defn in expr local function
 let rec fun-defn (with fun-defn)* in expr recursive function
 fun param+ spec* -> spec* expr unnamed function
 any result spec* arbitrary value
fun-defn::=fun-head spec* = spec* expr function definition
fun-head::=ghost? kind? symbol param+ (: result)? function header
kind::=functionpredicatelemma function kind
result::=ret-type 
 ( ret-type (, ret-type)* ) 
 ( ret-name (, ret-name)* ) 
ret-type::=ghost? type unnamed result
ret-name::=ghost? binder : type named result
spec::=requires { term } pre-condition
 ensures { term } post-condition
 returns { (| pattern -> term)+ } post-condition
 raises { (| pattern -> term)+ } exceptional post-c.
 raises { uqualid (, uqualid)* } raised exceptions
 reads { lqualid (, lqualid)* } external reads
 writes { path (, path)* } memory writes
 alias { alias (, alias)* } memory aliases
 variant { variant (, variant)* } termination variant
 diverges may not terminate
 (readswritesalias) { } empty effect
path::=lqualid (. lqualid)* v.field1.field2
alias::=path with path arg1 with result
variant::=term (with lqualid)? variant + WF-order
Figure 6.5: WhyML program expressions (part II).

6.5  The Why3 Language

6.5.1  Terms

The syntax for terms is given in Figure 6.1. The various constructs have the following priorities and associativities, from lowest to greatest priority:

constructassociativity
if then else / let in
label
cast
infix-op level 1left
infix-op level 2left
infix-op level 3left
infix-op level 4left
prefix-op
function applicationleft
brackets / ternary brackets
bang-op

Note the curryfied syntax for function application, though partial application is not allowed (rejected at typing).

6.5.2  Formulas

The syntax for formulas is given Figure 6.6. The various constructs have the following priorities and associativities, from lowest to greatest priority:

constructassociativity
if then else / let in
label
-> / <->right
by / soright
\/ / ||right
/\ / &&right
not
infix level 1left
infix level 2left
infix level 3left
infix level 4left
prefix

Note that infix symbols of level 1 include equality (=) and disequality (<>).


formula::=truefalse 
 formula -> formula implication
 formula <-> formula equivalence
 formula /\ formula conjunction
 formula && formula asymmetric conj.
 formula \/ formula disjunction
 formula || formula asymmetric disj.
 formula by formula proof indication
 formula so formula consequence indication
 not formula negation
 lqualid symbol
 prefix-op term 
 term infix-op term 
 lqualid term+ predicate application
 if formula then formula 
  else formula conditional
 let pattern = term in formula local binding
 match term (, term)+ with 
  (| formula-case)+ end pattern matching
 quantifier binders (, binders)* 
  triggers? . formula quantifier
 label formula label
 ( formula ) parentheses
quantifier::=forallexists
binders::=lident+ : type
triggers::=[ trigger (| trigger)* ] 
trigger::=tr-term (, tr-term)* 
tr-term::=termformula 
formula-case::=pattern -> formula
Figure 6.6: Syntax for formulas.

Notice that there are two symbols for the conjunction: /\ and &&, and similarly for disjunction. They are logically equivalent, but may be treated slightly differently by some transformations. For instance, split transforms the goal A /\ B into subgoals A and B, whereas it transforms A && B into subgoals A and A -> B. Similarly, it transforms not (A || B) into subgoals not A and not ((not A) /\ B). The by/so connectives are proof indications. They are logically equivalent to their first argument, but may affect the result of some transformations. For instance, the split_goal transformations interpret those connectives as introduction of logical cuts (see 9.5.5 for details).

6.5.3  Theories

The syntax for theories is given on Figure 6.7 and 6.8.


theory::=theory uident-nq label* decl* end
decl::=type type-decl (with type-decl)* 
 constant constant-decl 
 function function-decl (with logic-decl)* 
 predicate predicate-decl (with logic-decl)* 
 inductive inductive-decl (with inductive-decl)* 
 coinductive inductive-decl (with inductive-decl)* 
 axiom ident-nq : formula 
 lemma ident-nq : formula 
 goal ident-nq : formula 
 use imp-exp tqualid (as uident)? 
 clone imp-exp tqualid (as uident)? subst? 
 namespace import? uident-nq decl* end 
logic-decl::=function-decl 
 predicate-decl
constant-decl::=lident-nq label* : type 
 lident-nq label* : type = term
function-decl::=lident-nq label* type-param* : type 
 lident-nq label* type-param* : type = term
predicate-decl::=lident-nq label* type-param* 
 lident-nq label* type-param* = formula
inductive-decl::=lident-nq label* type-param* = 
  |? ind-case (| ind-case)* 
ind-case::=ident-nq label* : formula 
imp-exp::=(importexport)?
subst::=with (, subst-elt)+
subst-elt::=type lqualid = lqualid 
 function lqualid = lqualid 
 predicate lqualid = lqualid 
 namespace (uqualid.) = (uqualid.) 
 lemma qualid 
 goal qualid 
tqualid::=uidentident (. ident)* . uident 
type-decl::=lident-nq label* (' lident-nq label*)* type-defn
Figure 6.7: Syntax for theories (part 1).


type-defn::=  abstract type
 = type alias type
 = |? type-case (| type-case)* algebraic type
 = { record-field (; record-field)* } record type
 < range integer integer > range type
 < float integer integer > float type
type-case::=uident label* type-param*
record-field::=lident label* : type
type-param::=' lident 
 lqualid 
 ( lident+ : type ) 
 ( type (, type)* ) 
 ()
Figure 6.8: Syntax for theories (part 2).

Algebraic types

TO BE COMPLETED

Record types

TO BE COMPLETED

Range types

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.

Floating-point Types

A declaration of the form type f = < float eb sb > defines a type of floating-point numbers as specified by the IEEE-754 standard [8]. Here the literal eb represents the number of bits in the exponent and the literal sb the number of bits in the significand (including the hidden bit). Note that in order to make such a declaration the theory real.Real must be imported.

Why3 let you cast a real literal in a float type (e.g. (0.5:f)) and will check at typing that the literal is representable in the format. Note that Why3 do not implicitly round a real literal when casting to a float type, it refuses the cast if the literal is not representable.

Defining such a type f automatically introduces the following:

predicate f'isFinite f function f'real f : real constant f'eb : int constant f'sb : int

As specified by the IEEE standard, float formats includes infinite values and also a special NaN value (Not-a-Number) to represent results of undefined operations such as 0/0. The predicate f’isFinite indicates whether its argument is neither infinite nor NaN. The function f’real projects a finite term of type f to its real value, its result is not specified for non finite terms.

Unless specified otherwise with the meta "keep:literal" on f, the transformation eliminate_literal will introduce an axiom

axiom f'axiom : forall x:f. f'isFinite x -> -. max_real <=. f'real x <=. max_real

where max_real is the value of the biggest finite float in the specified format. The transformation also replaces all casts of the form (0.5:f) with a constant and an axiom as in:

constant fliteral42 : f axiom fliteral42_axiom : f'real fliteral42 = 0.5 /\ f'isFinite fliteral42

This type is used in the standard library in the theories ieee_float.Float32 and ieee_float.Float64.

6.5.4  Files

A Why3 input file is a (possibly empty) list of theories.

file::=theory*

6.6  The WhyML Language

6.6.1  Specification

The syntax for specification clauses in programs is given in Figure 6.9.


spec::=requiresensuresreturnsraises 
 readswritesvariant
requires::=requires { formula }
ensures::=ensures { formula }
returns::=returns { |? formula-case (| formula-case)* }
reads::=reads { term (, term)* }
writes::=writes { term (, term)* }
raises::=raises { |? raises-case (| raises-case)* } 
 raises { uqualid (, uqualid)* }
raises-case::=uqualid pattern? -> formula
variant::=variant { one-variant (, one-variant)+ }
one-variant::=term (with variant-rel)?
variant-rel::=lqualid
invariant::=invariant { formula } 
assertion::=(assertassumecheck) { formula } 
 absurd
Figure 6.9: Specification clauses in programs.

Within specifications, terms are extended with new constructs old and at:

term::=... 
 old term 
 at term ' uident 
  

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.

6.6.2  Expressions

The syntax for program expressions is given in Figure 6.10 and Figure 6.11.


expr::=integer integer constant
 real real constant
 lqualid symbol
 prefix-op expr 
 expr infix-op expr 
 expr [ expr ] brackets
 expr [ expr ] <- expr brackets assignment
 expr [ expr infix-op-1 expr ] ternary brackets
 expr expr+ function application
 fun binder+ spec* -> spec* expr lambda abstraction
 let rec rec-defn in expr recursive functions
 let fun-defn in expr local function
 if expr then expr (else expr)? conditional
 expr ; expr sequence
 loop invariant* variant? expr end infinite loop
 while expr while loop
  do invariant* variant? expr done 
 for lident = expr to-downto expr for loop
  do invariant* expr done 
 assertion assertion
 raise uqualid exception raising
 raise ( uqualid expr ) 
 try expr with (| handler)+ end exception catching
 any type spec* 
 abstract expr spec* blackbox
 let pattern = expr in expr local binding
 match expr (, expr)* with pattern matching
  |? expr-case (| expr-case)* end 
 ( expr (, expr)+ ) tuple
 { expr-field+ } record
 expr . lqualid field access
 expr . lqualid <- expr field assignment
 { expr with expr-field+ } field update
 expr : type cast
 ghost expr ghost expression
 label expr label
 ' uident : expr code mark
 ( expr ) parentheses
expr-case::=pattern -> expr 
expr-field::=lqualid = expr ; 
handler::=uqualid pattern? -> expr
to-downto::=todownto
Figure 6.10: Syntax for program expressions (part 1).


expr::=... see Fig. 6.4
 expr spec+ added specification
 if expr then expr (else expr)? conditional
 match expr with (| pattern -> expr)+ end pattern matching
 qualifier? begin spec+ expr end abstract block
 expr ; expr sequence
 let pattern = expr in expr let-binding
 let fun-defn in expr local function
 let rec fun-defn (with fun-defn)* in expr recursive function
 fun param+ spec* -> spec* expr unnamed function
 any result spec* arbitrary value
fun-defn::=fun-head spec* = spec* expr function definition
fun-head::=ghost? kind? symbol param+ (: result)? function header
kind::=functionpredicatelemma function kind
result::=ret-type 
 ( ret-type (, ret-type)* ) 
 ( ret-name (, ret-name)* ) 
ret-type::=ghost? type unnamed result
ret-name::=ghost? binder : type named result
spec::=requires { term } pre-condition
 ensures { term } post-condition
 returns { (| pattern -> term)+ } post-condition
 raises { (| pattern -> term)+ } exceptional post-c.
 raises { uqualid (, uqualid)* } raised exceptions
 reads { lqualid (, lqualid)* } external reads
 writes { path (, path)* } memory writes
 alias { alias (, alias)* } memory aliases
 variant { variant (, variant)* } termination variant
 diverges may not terminate
 (readswritesalias) { } empty effect
path::=lqualid (. lqualid)* v.field1.field2
alias::=path with path arg1 with result
variant::=term (with lqualid)? variant + WF-order
Figure 6.11: Syntax for program expressions (part 2).

In applications, arguments are evaluated from right to left. This includes applications of infix operators, with the only exception of lazy operators && and || that evaluate from left to right, lazily.

6.6.3  Modules

The syntax for modules is given in Figure 6.12.


module::=module uident-nq label* mdecl* end
mdecl::=decl theory declaration
 type mtype-decl (with mtype-decl)* mutable types
 type lident-nq (' lident-nq)* invariant+ added invariant
 let ghost? lident-nq label* pgm-defn 
 let rec rec-defn 
 val ghost? lident-nq label* pgm-decl 
 exception lident-nq label* type? 
 namespace import? uident-nq mdecl* end 
mtype-decl::=lident-nq label* (' lident-nq label*)* 
  mtype-defn 
mtype-defn::=  abstract type
 = type alias type
 = |? type-case (| type-case)* invariant* algebraic type
 = { mrecord-field (; mrecord-field)* } record type
  invariant*
mrecord-field::=ghost? mutable? lident-nq label* : type
pgm-defn::=fun-body 
 = fun binder+ spec* -> spec* expr 
pgm-decl::=: type global variable
 param (spec* param)+ : type spec* abstract function
Figure 6.12: Syntax for modules.

Any declaration which is accepted in a theory is also accepted in a module. Additionally, modules can introduce record types with mutable fields and declarations which are specific to programs (global variables, functions, exceptions).

6.6.4  Files

A WhyML input file is a (possibly empty) list of theories and modules.

file::=(theorymodule)*

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.

6.7  The Why3 Standard Library

The Why3 standard library provides general-purpose modules, to be used in logic and/or programs. It can be browsed on-line at http://why3.lri.fr/stdlib/. Each file contains one or several modules. To use or clone a module M from file file, use the syntax file.M, since file is available in Why3’s default load path. For instance, the module of integers and the module of references are imported as follows:

use import int.Int use import ref.Ref

A sub-directory mach/ provides various modules to model machine arithmetic. For instance, the module of 63-bit integers and the module of arrays indexed by 63-bit integers are imported as follows:

use import mach.int.Int63 use import mach.array.Array63

In particular, the types and operations from these modules are mapped to native OCaml’s types and operations when Why3 code is extracted to OCaml (see Section 7.2).


Previous Up Next