Chapter 2  Reference manual

2.1  Command line

Why is invoked as a batch compiler, given a list of input files:

If no file is given, then standard input is processed and output is named with the prefix out_why (and a suffix depending of the selected prover). The full list of command line options can be obtained with

  why --help

2.2  Syntax of input files

2.2.1  Lexical conventions

Comments are opened with (*, closed with *) and can be nested.

Identifiers are made of letters, digits, the underscore character _ and the single quote ’, starting with a letter. Additionally, they can be qualified by a label (another identifier), using the @ notation.

Keywords are the following:

2.2.2  Grammar

Logic

Syntax for terms is given Figure 2.1. Arithmetical operations have usual precedences and are left associative. The division operator / only applies on reals, not on integer. Division and modulo operations on integers come in library divisions.why in two flavors: mathematical division rounds down whereas computer division rounds to zero. The conditional construct if t₁ then t₂ else t₃ can also be written in prefix notation as if_then_else(t₁, t₂, t₃).

Syntax for predicates is given Figure 2.2. Precedences are the following (from strongest to weakest): not, and, or, implication, and forall. Implication, conjunction and disjunction are right associative. Syntactic sugar: t₁   R₁   t₂   R₂   t₃ is equivalent to t₁   R₁   t₂   and   t₂   R₂   t₃ for any relations R₁ and R₂. Example: 0 <= x < y is 0 <= x and x < y.

Syntax for logic declarations is given Figure 2.3.

---

⟨term⟩	::=	⟨constant⟩
	|	⟨term⟩ ⟨arith_op⟩ ⟨term⟩
	|	- ⟨term⟩
	|	⟨lab_identifier⟩
	|	⟨identifier⟩ ( ⟨term⟩,+ )
	|	⟨lab_identifier⟩ [ ⟨term⟩ ]
	|	if ⟨term⟩ then ⟨term⟩ else ⟨term⟩
	|	let ⟨identifier⟩ = ⟨term⟩ in ⟨term⟩
	|	( ⟨term⟩ )
⟨constant⟩	::=	⟨integer-constant⟩
	|	⟨real-constant⟩
	|	true
	|	false
	|	void
⟨arith_op⟩	::=	+ | - | * | /

Figure 2.1: Syntax of terms

---

---

⟨predicate⟩	::=	true
	|	false
	|	⟨identifier⟩
	|	⟨identifier⟩ ( ⟨term⟩,+ )
	|	⟨term⟩ ⟨relation⟩ ⟨term⟩ [ ⟨relation⟩ ⟨term⟩ ]
	|	⟨predicate⟩ -> ⟨predicate⟩
	|	⟨predicate⟩ <-> ⟨predicate⟩
	|	⟨predicate⟩ or ⟨predicate⟩
	|	⟨predicate⟩ and ⟨predicate⟩
	|	not ⟨predicate⟩
	|	if ⟨term⟩ then ⟨predicate⟩ else ⟨predicate⟩
	|	let ⟨identifier⟩ = ⟨term⟩ in ⟨predicate⟩
	|	forall ⟨identifier⟩,+ : ⟨primitive_type⟩ [ ⟨triggers⟩ ] . ⟨predicate⟩
	|	exists ⟨identifier⟩,+ : ⟨primitive_type⟩ . ⟨predicate⟩
	|	( ⟨predicate⟩ )
	|	(⟨identifier⟩ | ⟨string⟩) : ⟨predicate⟩
⟨triggers⟩	::=	[ ⟨trigger⟩|+ ]
⟨trigger⟩	::=	⟨term⟩,+
⟨primitive_type⟩	::=	int | bool | real | unit | ⟨identifier⟩ | ’ ⟨identifier⟩
	|	⟨primitive_type⟩ ⟨identifier⟩ | ( ⟨primitive_type⟩,⋆ ) ⟨identifier⟩
⟨relation⟩	::=	= | <> | < | <= | > | >=

Figure 2.2: Syntax of predicates

---

---

⟨l_declaration⟩	::=	[ external ] type [ ⟨type_parameters⟩ ] ⟨identifier⟩
	|	[ external ] logic ⟨identifier⟩,+ : ⟨logic_type⟩
	|	function ⟨identifier⟩ ( ⟨logic_binder⟩,⋆ ) : ⟨primitive_type⟩
		= ⟨term⟩
	|	predicate ⟨identifier⟩ ( ⟨logic_binder⟩,⋆ ) = ⟨predicate⟩
	|	inductive ⟨identifier⟩ : ⟨logic_type⟩ =
		(| ⟨identifier⟩ : ⟨predicate⟩)⋆ }
	|	axiom ⟨identifier⟩ : ⟨predicate⟩
	|	lemma ⟨identifier⟩ : ⟨predicate⟩
	|	goal ⟨identifier⟩ : ⟨predicate⟩
⟨logic_type⟩	::=	⟨logic_arg_type⟩,⋆ -> prop
	|	⟨logic_arg_type⟩,⋆ -> ⟨primitive_type⟩
⟨logic_arg_type⟩	::=	⟨primitive_type⟩ | ⟨primitive_type⟩ array
⟨logic_binder⟩	::=	⟨identifier⟩ : ⟨primitive_type⟩
⟨type_parameters⟩	::=	’⟨identifier⟩ | ( (’⟨identifier⟩),+ )

Figure 2.3: Syntax of logic declarations

---

Programs

Syntax of types is given Figure 2.4. Syntax of annotated programs is given Figure 2.5. Syntax of input files is given Figure 2.6.

---

⟨simple_value_type⟩	::=	⟨primitive_type⟩
	|	⟨primitive_type⟩ ref
	|	⟨primitive_type⟩ array
	|	( ⟨value_type⟩ )
⟨value_type⟩	::=	⟨simple_value_type⟩
	|	⟨simple_value_type⟩ -> ⟨computation_type⟩
	|	⟨identifier⟩ : ⟨simple_value_type⟩ -> ⟨computation_type⟩
⟨computation_type⟩	::=	{ [ ⟨precondition⟩ ] }
		[ returns ⟨identifier⟩ : ] ⟨value_type⟩ ⟨effects⟩
		{ [ ⟨postcondition⟩ ] }
	|	⟨value_type⟩
⟨effects⟩	::=	[ reads ⟨identifier⟩,⋆ ] [ writes ⟨identifier⟩,⋆ ] [ raises ⟨identifier⟩,⋆ ]
⟨precondition⟩	::=	⟨assertion⟩
⟨postcondition⟩	::=	⟨assertion⟩ ⟨exn_condition⟩⋆
⟨exn_condition⟩	::=	| ⟨identifier⟩ => ⟨assertion⟩
⟨assertion⟩	::=	⟨predicate⟩ [ as ⟨identifier⟩ ]

Figure 2.4: Syntax of types

---

---

⟨prog⟩	::=	⟨constant⟩
	|	⟨identifier⟩
	|	! ⟨identifier⟩
	|	⟨identifier⟩ := ⟨prog⟩
	|	⟨identifier⟩ [ ⟨prog⟩ ]
	|	⟨identifier⟩ [ ⟨prog⟩ ] := ⟨prog⟩
	|	⟨prog⟩ ⟨infix⟩ ⟨prog⟩
	|	⟨prefix⟩ ⟨prog⟩
	|	let ⟨identifier⟩ = ⟨prog⟩ in ⟨prog⟩
	|	let ⟨identifier⟩ = ref ⟨prog⟩ in ⟨prog⟩
	|	if ⟨prog⟩ then ⟨prog⟩ [ else ⟨prog⟩ ]
	|	while ⟨prog⟩ do [ ⟨loop_annot⟩ ] ⟨prog⟩ done
	|	⟨prog⟩ ; ⟨prog⟩
	|	⟨identifier⟩ : ⟨prog⟩
	|	assert ({ ⟨assertion⟩ })+ ; ⟨prog⟩
	|	⟨prog⟩ { ⟨postcondition⟩ }
	|	⟨prog⟩ {{ ⟨postcondition⟩ }}
	|	fun ⟨binders⟩ -> ⟨prog⟩
	|	let ⟨identifier⟩ ⟨binders⟩ = ⟨prog⟩ in ⟨prog⟩
	|	let rec ⟨recfun⟩ [ in ⟨prog⟩ ]
	|	⟨prog⟩ ⟨prog⟩
	|	raise ⟨identifier⟩ [ : ⟨value_type⟩ ]
	|	raise ( ⟨identifier⟩ ⟨prog⟩ ) [ : ⟨value_type⟩ ]
	|	try ⟨prog⟩ with ⟨handler⟩|+ end
	|	absurd [ : ⟨value_type⟩ ]
	|	( ⟨prog⟩ )
	|	begin ⟨prog⟩ end
⟨infix⟩	::=	+ | - | * | / | = | <> | < | <= | > | >= | || | &&
⟨prefix⟩	::=	- | not
⟨binders⟩	::=	( ⟨identifier⟩,+ : ⟨value_type⟩ )+
⟨recfun⟩	::=	⟨identifier⟩ ⟨binders⟩ : value_type
		{ variant ⟨wf_arg⟩ } = ⟨prog⟩
⟨loop_annot⟩	::=	{ [ invariant ⟨assertion⟩ ] [ variant ⟨wf_arg⟩ ] }
⟨wf_arg⟩	::=	⟨term⟩ [ for ⟨identifier⟩ ]
⟨handler⟩	::=	⟨identifier⟩ -> ⟨prog⟩
	|	⟨identifier⟩ ⟨identifier⟩ -> ⟨prog⟩

Figure 2.5: Syntax of annotated programs

---

---

⟨file⟩	::=	⟨declaration⟩⋆
⟨declaration⟩	::=	let ⟨identifier⟩ [ ⟨binders⟩ ] = ⟨prog⟩
	|	let rec ⟨recfun⟩
	|	[ external ] parameter ⟨identifier⟩,+ : ⟨value_type⟩
	|	exception ⟨identifier⟩ [ of ⟨primitive_type⟩ ]
	|	⟨l_declaration⟩

Figure 2.6: Syntax of input files

---

2.3  Semantics

2.3.1  Logic

The abstract syntax for types (τ), terms (t) and predicates (P) is given by the following grammars:

A theory Σ is a finite list of declarations δ where

Typing

Well-formed types (Σ⊢τ wf):

Well-typed terms (Σ⊢ t:τ):

   

where σ is a mapping from type variables to types, naturally extended to types with σ((τ₁,…,τ_n) s) = (σ(τ₁),…,σ(τ_n)) s. We write Subst(σ,Σ) whenever Σ⊢σ(α) wf holds for any type variable α.

Well-typed predicates (Σ⊢P wf):

Well-formed theories (⊢Σ wf):

Well-formed definitions of functions and predicates:

Then, as far as typing and validity in concerned, the function f (resp. the predicate p) is added to Σ as logic f:τ₁,…,τ_n→τ (resp. logic p:τ₁,…,τ_n→prop).

Validity

Validity is defined as a set of natural deduction rules (Σ⊨ P). For the sake of clarity, we write Σ,P for Σ,axiom P in the following. A substitution σ over from type variables to types in extended to terms and predicates in the obvious way. We write P[t/x] for the substitution of all the occurrences of a free variable x in P by a term t.

Deduction rules for equality:

Arithmetic: An arithmetic proposition P is a proposition built from variables of type int, integers constants, the functions symbols add_int and sub_int, the predicates lt_int, le_int, gt_int, ge_int and the equality. If x₁,…,x_n are the free variables of P, we write x₁,…,x_n⊨_A P whenever P is valid in Presburger arithmetic (which is decidable). Then we have the following deduction rule for arithmetic:

2.3.2  Programs

Program types (θ) and specifications (κ) are classified as follows:

A value of type θ is either an immutable variable of a pure type (τ), a reference containing a value of a pure type (τ ref) or a function of type (x:θ)→{p} θ′ є {q} mapping the formal parameter x to the specification of its body, that is a precondition p, the type θ′ for the returned value, an effect є and a postcondition q. An effect is made of tree lists of variables: the references possibly accessed (reads), the references possibly modified (writes) and the exceptions possibly raised (raises). A postcondition q is made of several parts: one for the normal termination and one for each possibly raised exception (E stands for an exception name).

When a function specification {p} θ є {q} has no precondition and no postcondition (both being ⊤) and no effect (є is made of three empty lists) it can be shortened to θ. In particular, (x₁:θ₁)→⋯→(x_n:θ_n)→κ denotes the type of a function with n arguments that has no effect as long as it not applied to n arguments. Note that functions can be partially applied.

The syntax for program expressions is given in Figure 2.7. In particular, programs contain pure terms (t) made of constants, variables, dereferences (written !x) and application of function symbols from the logic to pure terms. loop e {invariant p variant t} is an infinite loop of body e, invariant p and which termination is ensured by the variant t.

---

t  ::=  x  |  !x  |  f(t,…,t)        e  ::=  t    |  let x = e in e    |  let x = ref e in e    |  if e then e else e    |  loop e {invariant p variant t}    |  L:e    |  raise (E e):θ    |  try e with E x→e end    |  assert {p}; e    |  e {q}    |  e {{q}}    |  fun (x:θ)→{p} e    |  rec x (x:θ)…(x:θ):θ {variant t}={p} e    |  e e

Figure 2.7: Abstract syntax of program expressions

---

Syntactic sugar.

The traditional sequence construct is only syntactic sugar for a let-in binder where the variable does not occur in e₂:

The assignment construct is syntactic sugar for the application of the function ref_set from Why’s prelude (see 2.4):

We also simplify the raise construct whenever both the exception contents and the whole raise expression have type unit:

The traditional while loop is also syntactic sugar for a combination of an infinite loop and the use of an exception Exit to exit the loop:

Typing

The typing of program expressions is straightforward, with polymorphism but no type inference.

Operational semantics

The language is strict (all arguments always evaluated before the function call), with a left-to-right evaluation order.

Weakest preconditions

Programs correctness is defined using a calculus of weakest preconditions. We note wp(e,q;r) the weakest precondition for a program expression e and a postcondition q;r where q is the property to hold when terminating normally and r = E₁⇒ q₁; …; E_n⇒ q_n is the set of properties to hold for each possibly uncaught exception. Expressing the correctness of a program e is simply a matter of computing wp(e,True).

The rules for the basic constructs are the following:

On the case of an exception free sequence, we retrieve the usual rule:

The cases of exceptions and annotations are also straightforward:

The last implication r′⇒ r is actually an abuse for the conjunction of all implications for each postcondition part. The case of an infinite loop is more subtle:

where ω stands for the set of references possibly modified by the loop body (the writes part of e’s effect). Here the weakest precondition expresses that the invariant must hold initially and that for each turn in the loop (represented by ω), either p is preserved by e and e decreases the value of t (to ensure termination), or e raises an exception and thus must establish r directly.

By combining this rule and the rule for the conditional, we can retrieve the rule for the usual while loop:

Finally, we give the rules for functions and function calls. Since a function cannot be mentioned within the postcondition, the weakest preconditions for function constructs fun and rec are only expressing the correctness of the function body:

where ρ stands for the set of references possibly accessed by the loop body (the reads part of e’s effect). In the case of a recursive function, wp(L:e,True) must be computed within an environment where f is assumed to have type (x₁:θ₁)→⋯→(x_n:θ_n)→{p∧ t<at(t,L)} θ є {q} i.e. where the decreasing of the variant t has been added to the precondition of f.

The case of a function call e1 e2 can be simplified to the case of an application x₁ x₂ of one variable to another, using the following transformation if needed:

Then assuming that x₁ has type (x:θ)→{p′} θ′ є {q′}, we define

that is (1) the precondition of the function must hold and (2) its postcondition must imply the expected property q whatever the values of the modified references and of the result are. Note that q and q′ may contain exceptional parts and thus the implication is again an abuse for the conjunction of all implications for each postcondition part.

In the case of an assignment x := e the rules above combined with the specification of ref_set give (assuming that result does not occur in q):

And in the case of the assigment of a side-effect free expression t, it simplifies to

which is equivalent to the usual rule wp(x := t,q) = q[x← t].

2.4  Prelude

Apart from the type names unit, bool, int, real, and the type constructor ref, nothing is built-in in the Why tool. But two prelude files are read before considering the files given on the command line. The prelude files are

• /usr/local/lib/why/prelude.why, and
• /usr/local/lib/why/arrays.why

(unless your library path is set differently). The interpretation of this prelude is prover-dependent. It is possible not to load the prelude using the command-line option --no-prelude, or to load only the first prelude file using the command-line option --no-arrays. The remaining of this section describes the contents of the prelude files.

2.4.1  prelude.why

(* Built-in types: unit, bool, int, real *)

(********)
(* unit *)
(********)

logic eq_unit : unit,unit -> prop
logic neq_unit : unit,unit -> prop

parameter eq_unit_ : x:unit -> y:unit -> {} bool {if result then x=y else x<>y}
parameter neq_unit_: x:unit -> y:unit -> {} bool {if result then x<>y else x=y}


(********)
(* bool *)
(********)

logic eq_bool : bool,bool -> prop
logic neq_bool : bool,bool -> prop

parameter eq_bool_ : x:bool -> y:bool -> {} bool {if result then x=y else x<>y}
parameter neq_bool_: x:bool -> y:bool -> {} bool {if result then x<>y else x=y}

(* these are needed for WP *)

parameter strict_bool_and_ : 
  b1:bool -> b2:bool ->  
  {} bool { if result then b1=true and b2=true 
                      else (b1=false or b1=true and b2=false) }

parameter strict_bool_or_ : 
  b1:bool -> b2:bool -> 
  {} bool { if result then b1=true or b1=false and b2=true 
                      else (b1=false and b2=false) }

parameter bool_not_ : 
  b:bool -> {} bool { if result then b=false else b=true }


(* non built-in are in bool.why *)

(************)
(* Integers *)
(************)

logic lt_int : int,int -> prop  (* <  *)
logic le_int : int,int -> prop  (* <= *)
logic gt_int : int,int -> prop  (* >  *)
logic ge_int : int,int -> prop  (* >= *)
logic eq_int : int,int -> prop  (* =  *)
logic neq_int : int,int -> prop (* <> *)

(* < <= > >= = and <> in programs: *)
parameter lt_int_ : x:int -> y:int -> {} bool { if result then x<y else x>=y }
parameter le_int_ : x:int -> y:int -> {} bool { if result then x<=y else x>y }
parameter gt_int_ : x:int -> y:int -> {} bool { if result then x>y else x<=y }
parameter ge_int_ : x:int -> y:int -> {} bool { if result then x>=y else x<y }
parameter eq_int_ : x:int -> y:int -> {} bool { if result then x=y else x<>y }
parameter neq_int_ : x:int -> y:int -> {} bool { if result then x<>y else x=y }

logic add_int : int,int -> int (* + *)
logic sub_int : int,int -> int (* - *)
logic mul_int : int,int -> int (* * *)
(*
logic div_int : int,int -> int (* / in logic only *)
logic mod_int : int,int -> int (* % in logic only *)
*)
logic neg_int : int -> int     (* prefix - *)

(* / and % in programs: *)
(*
parameter div_int_ : x:int -> y:int -> { y<>0 } int { result = x / y }
parameter mod_int_ : x:int -> y:int -> { y<>0 } int { result = x % y }
*)

(* Default well-founded ordering over integers *)

predicate zwf_zero(a:int, b:int) = 0 <= b and a < b

(**************)
(* references *)
(**************)

(* Built-in type constructor: 'a ref *)
(* References. := is syntactic sugar for ref_set: *)

parameter ref_set : x:'a ref -> v:'a -> {} unit writes x { x = v }

2.4.2  arrays.why

(* Arrays.
   Type 'a array is a built-in shortcut for 'a farray ref, where 'a farray
   is the following abstract type for purely applicative arrays *)

type 'a farray

logic access : 'a farray, int -> 'a
logic update : 'a farray, int, 'a -> 'a farray

axiom access_update : 
  forall a : 'a farray. forall i : int. forall v : 'a.
  access(update(a,i,v), i) = v

axiom access_update_neq : 
  forall a : 'a farray. forall i : int. forall j : int. forall v : 'a.
  i <> j -> access(update(a,i,v), j) = access(a,j)

(* Length *)

logic array_length : 'a farray -> int

parameter array_length_ : 
  a:'a array -> {} int reads a { result=array_length(a) }

(* t[e] is syntactic sugar for (array_get t e) *)
parameter array_get :
  a:'a array -> i:int -> 
    { 0 <= i < array_length(a) } 'a reads a { result = access(a,i) }

(* t [e1] := e2 is syntactic sugar for (array_set t e1 e2) *)
parameter array_set : 
  a:'a array -> i:int -> v:'a -> 
    { 0 <= i < array_length(a) } unit writes a { a = update(a@,i,v) }

(* Sorted arrays *)

predicate sorted_array(t:int farray, i:int, j:int) = 
  forall k1,k2:int. i <= k1 <= k2 <= j -> t[k1] <= t[k2]

(* Arrays permutations *)

predicate exchange(a1:'a farray, a2:'a farray, i:int, j:int) = 
  array_length(a1) = array_length(a2) and
  a1[i] = a2[j] and a2[i] = a1[j] and
  forall k:int. (k <> i and k <> j) -> a1[k] = a2[k]

logic permut : 'a farray, 'a farray, int, int -> prop

axiom permut_refl :
  forall t:'a farray. forall l,u:int. permut(t,t,l,u)

axiom permut_sym :
  forall t1,t2:'a farray. forall l,u:int.
  permut(t1,t2,l,u) -> permut(t2,t1,l,u)

axiom permut_trans :
  forall t1,t2,t3:'a farray. forall l,u:int.
  permut(t1,t2,l,u) -> permut(t2,t3,l,u) -> permut(t1,t3,l,u)

axiom permut_exchange :
  forall a1,a2:'a farray. forall l,u,i,j:int. 
  l <= i <= u -> l <= j <= u -> exchange(a1,a2,i,j) -> permut(a1,a2,l,u)

axiom exchange_upd :
  forall a:'a farray. forall i,j:int.
  exchange(a,update(update(a,i,a[j]),j,a[i]),i,j)

axiom permut_weakening :
  forall a1,a2:'a farray. forall l1,r1,l2,r2:int.
  (*forall x_,y_:'a farray [permut(a1,a2,l2,r2),permut(x_,y_,l1,r1)].*)
  l1 <= l2 <= r2 <= r1 -> permut(a1,a2,l2,r2) -> permut(a1,a2,l1,r1)

axiom permut_eq :
  forall a1,a2:'a farray. forall l,u:int.
  l <= u -> permut(a1,a2,l,u) ->
  forall i:int. (i < l or u < i) -> a2[i] = a1[i]

predicate permutation(a1:'a array, a2:'a array) =
  permut(a1,a2,0,array_length(a1)-1)


(* Axioms about array_length *)

axiom array_length_update :
  forall a:'a farray. forall i:int. forall v:'a.
  array_length(update(a,i,v)) = array_length(a)

axiom permut_array_length :
  forall a1,a2:'a farray. forall l,u:int. 
  permut(a1,a2,l,u) -> array_length(a1) = array_length(a2)

2.5  Provers specificities

2.5.1  Coq

Several Coq modules are delivered with Why. If installation is properly done, they should be found in subdirectory user-contrib of the Coq standard library (usually /usr/lib/coq unless some other path was specified when installing Coq).

Types.

Types are mapped as follows:

Arrays.

Arrays are introduced in module WhyArrays. Some tactics are provided to help the user simplifying array expressions in proof obligations:

WhyArrays

: repeatedly simplifies access/updateusing combinations and array_length expressions

AccessSame

: rewrites access (update t i v) i into v, simplifies with WhyArrays and attempts omega on every subgoal

AccessOther

: rewrites access (update t i v) j into access t j, simplifies with WhyArrays and attempts omega on every subgoal

ArraySubst t

: similar to subst t, with additional simplifications

2.5.2  PVS

Types.

Types are mapped as follows:

Arrays.

An array whose elements are of type T is a PVS value of type warray[T]. This type is defined in the theory why_arrays, as a pair of an integer, the array length, and a function mapping indices to elements :

     warray: TYPE = [ n:int, [ below(n) -> T ] ]

Two other theories, why_int_array_pred and why_array_pred, introduce the various predicates over arrays presented in Section 2.4.