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

The syntax distinguishes lowercase and uppercase identifiers and, similarly, lowercase and uppercase qualified identifiers.

lalpha ::= a - z_
ualpha ::= A - Z
alpha ::= lalphaualpha
lident ::= lalpha (alphadigit')*
uident ::= ualpha (alphadigit')*
ident ::= lidentuident
lqualid ::= lidentuqualid . lident
uqualid ::= uidentuqualid . uident
qualid ::= identuqualid . ident

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 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 : formula  
  lemma ident : formula  
  goal ident : formula  
  use imp-exp tqualid (as uident)? 
  clone imp-exp tqualid (as uident)? subst? 
  namespace import? uident decl* end 
logic-decl ::= function-decl 
  predicate-decl
constant-decl ::= lident label* : type 
  lident label* : type = term
function-decl ::= lident label* type-param* : type 
  lident label* type-param* : type = term
predicate-decl ::= lident label* type-param* 
  lident label* type-param* = formula
inductive-decl ::= lident label* type-param* = 
   |? ind-case (| ind-case)* 
ind-case ::= ident 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 label* (' lident 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
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).

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 label* mdecl* end
mdecl ::= decl theory declaration
  type mtype-decl (with mtype-decl)* mutable types
  type lident (' lident)* invariant+ added invariant
  let ghost? lident label* pgm-defn 
  let rec rec-defn 
  val ghost? lident label* pgm-decl 
  exception lident label* type? 
  namespace import? uident mdecl* end 
mtype-decl ::= lident label* (' lident 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 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