Previous Up Next

Chapter 7  Language Reference

This chapter gives the grammar and semantics for Why3 and WhyML input files.

7.1  Lexical Conventions

Lexical conventions are common to Why3 and WhyML.

7.1.1  Comments

Comments are enclosed by (* and *) and can be nested.

7.1.2  Strings

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.

7.1.3  Identifiers

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.

lalpha ::= a - z_
ualpha ::= A - Z
alpha ::= lalphaualpha
suffix ::= (alphadigit')*
lident ::= lalpha suffix
uident ::= ualpha suffix
ident ::= lidentuident
lqualid ::= lidentuqualid . lident
uqualid ::= uidentuqualid . uident
qualid ::= identuqualid . ident
digit-or-us ::= 0 - 9_
alpha-no-us ::= a - zA - Z
suffix-nq ::= (alpha-no-us'* digit-or-us)* '*
lident-nq ::= lalpha suffix-nq
uident-nq ::= ualpha suffix-nq
ident-nq ::= lident-nquident-nq

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

7.1.4  Constants

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.


digit ::= 0 - 9 
hex-digit ::= digita - fA - F 
oct-digit ::= 0 - 7
bin-digit ::= 01
integer ::= digit (digit_)* decimal
  (0x0X) hex-digit (hex-digit_)* hexadecimal
  (0o0O) oct-digit (oct-digit_)* octal
  (0b0B) bin-digit (bin-digit_)* binary
real ::= digit+ exponent decimal
  digit+ . digit* exponent? 
  digit* . digit+ exponent? 
  (0x0X) hex-real h-exponent hexadecimal
hex-real ::= hex-digit+ 
  hex-digit+ . hex-digit* 
  hex-digit* . hex-digit+ 
exponent ::= (eE) (-+)? digit+ 
h-exponent ::= (pP) (-+)? digit+
Figure 7.1: Syntax for constants.

7.1.5  Operators

Prefix and infix operators are built from characters organized in four categories (op-char-1 to op-char-4).

op-char-1 ::= =<>~ 
op-char-2 ::= +- 
op-char-3 ::= */% 
op-char-4 ::= !$&?@^.:|# 
op-char ::= op-char-1 ∣ op-char-2 ∣ op-char-3 ∣ op-char-4 
infix-op-1 ::= op-char* op-char-1 op-char* 
infix-op ::= op-char+ 
prefix-op ::= op-char+ 
bang-op ::= ! op-char-4*? op-char-4*

Infix operators are classified into 4 categories, according to the characters they are built from:

7.1.6  Labels

Identifiers, terms, formulas, program expressions can all be labeled, either with a string, or with a location tag.

label ::= string 
  # filename digit+ digit+ digit+ # 
filename ::= string

A location tag consists of a file name, a line number, and starting and ending characters.

7.2  The Why3 Language

7.2.1  Terms

The syntax for terms is given in Figure 7.2. 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).


term ::= integer integer constant
  real real constant
  lqualid symbol
  prefix-op term  
  bang-op term  
  term infix-op term  
  term [ term ] brackets
  term [ term <- term ] ternary brackets
  lqualid term+ function application
  if formula then term 
   else term conditional
  let pattern = term in term local binding
  match term (, term)* with 
   (| term-case)+ end pattern matching
  ( term (, term)+ ) tuple
  { term-field+ } record
  term . lqualid field access
  { term with term-field+ } field update
  term : type cast
  label term label
  ' uident code mark
  ( term ) parentheses
pattern ::= pattern | pattern or pattern
  pattern , pattern tuple
  _ catch-all
  lident variable
  uident pattern* constructor
  ( pattern ) parentheses
  pattern as lident binding
term-case ::= pattern -> term 
term-field ::= lqualid = term ;
Figure 7.2: Syntax for terms.

7.2.2  Type Expressions

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

7.2.3  Formulas

The syntax for formulas is given Figure 7.3. 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 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).

7.2.4  Theories

The syntax for theories is given on Figure 7.4 and 7.5.


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 7.4: 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 7.5: 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 []. 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.

7.2.5  Files

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

file ::= theory*

7.3  The WhyML Language

7.3.1  Specification

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


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 7.6: 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.

7.3.2  Expressions

The syntax for program expressions is given in Figure 7.7 and Figure 7.8.


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 7.7: Syntax for program expressions (part 1).


rec-defn ::= fun-defn (with fun-defn)* 
fun-defn ::= ghost? lident label* fun-body 
fun-body ::= binder+ (: type)? spec* = spec* expr 
binder ::= ghost? lident label*param
param ::= ( (ghost? lident label*)+ : type )
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.

7.3.3  Modules

The syntax for modules is given in Figure 7.9.


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

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

7.4  The Why3 Standard Library

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

Previous Up Next