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	::=	lalpha ∣ ualpha
lident	::=	lalpha (alpha ∣ digit ∣ ')^*
uident	::=	ualpha (alpha ∣ digit ∣ ')^*
ident	::=	lident ∣ uident
lqualid	::=	lident ∣ uqualid . lident
uqualid	::=	uident ∣ uqualid . uident
qualid	::=	ident ∣ uqualid . 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 ::= digit ∣ a - f ∣ A - F

oct-digit ::= 0 - 7

bin-digit ::= 0 ∣ 1

integer ::= digit (digit ∣ _)^* decimal

∣ (0x ∣ 0X) hex-digit (hex-digit ∣ _)^* hexadecimal

∣ (0o ∣ 0O) oct-digit (oct-digit ∣ _)^* octal

∣ (0b ∣ 0B) bin-digit (bin-digit ∣ _)^* binary

real ::= digit⁺ exponent decimal

∣ digit⁺ . digit^* exponent^?

∣ digit^* . digit⁺ exponent^?

∣ (0x ∣ 0X) hex-real h-exponent hexadecimal

hex-real ::= hex-digit⁺

∣ hex-digit⁺ . hex-digit^*

∣ hex-digit^* . hex-digit⁺

exponent ::= (e ∣ E) (- ∣ +)^? digit⁺

h-exponent ::= (p ∣ P) (- ∣ +)^? 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:

level 4: operators containing only characters from op-char-4;
level 3: those containing characters from op-char-3 or op-char-4;
level 2: those containing characters from op-char-2, op-char-3 or op-char-4;
level 1: all other operators (non-terminal infix-op-1).

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:

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

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:

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

formula ::= true ∣ false

∣ 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 ::= forall ∣ exists

binders ::= lident⁺ : type

triggers ::= [ trigger (| trigger)^* ]

trigger ::= tr-term (, tr-term)^*

tr-term ::= term ∣ formula

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 ::= (import ∣ export)^?

subst ::= with (, subst-elt)⁺

subst-elt ::= type lqualid = lqualid

∣ function lqualid = lqualid

∣ predicate lqualid = lqualid

∣ namespace (uqualid ∣ .) = (uqualid ∣ .)

∣ lemma qualid

∣ goal qualid

tqualid ::= uident ∣ ident (. 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 ::= requires ∣ ensures ∣ returns ∣ raises

∣ reads ∣ writes ∣ variant

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 ::= (assert ∣ assume ∣ check) { 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 ::= to ∣ downto

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

::=

(theory ∣ module)^*

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

digit	::=	0 - 9
hex-digit	::=	digit ∣ a - f ∣ A - F
oct-digit	::=	0 - 7
bin-digit	::=	0 ∣ 1
integer	::=	digit (digit ∣ _)^*	decimal
	∣	(0x ∣ 0X) hex-digit (hex-digit ∣ _)^*	hexadecimal
	∣	(0o ∣ 0O) oct-digit (oct-digit ∣ _)^*	octal
	∣	(0b ∣ 0B) bin-digit (bin-digit ∣ _)^*	binary
real	::=	digit⁺ exponent	decimal
	∣	digit⁺ . digit^* exponent^?
	∣	digit^* . digit⁺ exponent^?
	∣	(0x ∣ 0X) hex-real h-exponent	hexadecimal
hex-real	::=	hex-digit⁺
	∣	hex-digit⁺ . hex-digit^*
	∣	hex-digit^* . hex-digit⁺
exponent	::=	(e ∣ E) (- ∣ +)^? digit⁺
h-exponent	::=	(p ∣ P) (- ∣ +)^? digit⁺

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 ;

formula	::=	true ∣ false
	∣	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	::=	forall ∣ exists
binders	::=	lident⁺ : type
triggers	::=	[ trigger (\| trigger)^* ]
trigger	::=	tr-term (, tr-term)^*
tr-term	::=	term ∣ formula
formula-case	::=	pattern -> formula

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	::=	(import ∣ export)^?
subst	::=	with (, subst-elt)⁺
subst-elt	::=	type lqualid = lqualid
	∣	function lqualid = lqualid
	∣	predicate lqualid = lqualid
	∣	namespace (uqualid ∣ .) = (uqualid ∣ .)
	∣	lemma qualid
	∣	goal qualid
tqualid	::=	uident ∣ ident (. ident)^* . uident
type-decl	::=	lident label^* (' lident label^)^ type-defn

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)^* )
	∣	()

spec	::=	requires ∣ ensures ∣ returns ∣ raises
	∣	reads ∣ writes ∣ variant
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	::=	(assert ∣ assume ∣ check) { formula }
	∣	absurd

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	::=	to ∣ downto

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 )

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