Previous Up Next

Chapter 2  Reference manual

2.1  Command line

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

why [options] file1filen

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.

identifier::=letter⟩ (⟨letter⟩ | 0..9 | _ | )
letter::=A..Z | a..z
lab_identifier::=identifier⟩ [ @ [ ⟨identifier⟩ ] ]

Keywords are the following:

absurd     and     array     as     assert
axiom     begin     bool     do     done
else     end     exception     exists     external
false     for     forall     fun     function
goal     if     in     int     invariant
lemma     let     logic     not     of
or     parameter     predicate     prop     raise
raises     reads     real     rec     ref
returns     then     true     try     type
unit     variant     void     while     with

2.2.2  Grammar


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 t1 then t2 else t3 can also be written in prefix notation as if_then_else(t1, t2, t3).

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: t1   R1   t2   R2   t3 is equivalent to t1   R1   t2   and   t2   R2   t3 for any relations R1 and R2. Example: 0 <= x < y is 0 <= x and x < y.

Syntax for logic declarations is given Figure 2.3.

 |term⟩ ⟨arith_op⟩ ⟨term
 |identifier(term,+ )
arith_op::=+ | - | * | /

Figure 2.1: Syntax of terms

 |identifier(term,+ )
 |term⟩ ⟨relation⟩ ⟨term⟩ [ ⟨relation⟩ ⟨term⟩ ]
 |forallidentifier,+ :primitive_type⟩ [ ⟨triggers⟩ ] .predicate
 |existsidentifier,+ :primitive_type.predicate
 |(⟨identifier⟩ | ⟨string⟩) :predicate
triggers::=[trigger|+ ]
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 ] logicidentifier,+ :logic_type
|functionidentifier(logic_binder, ) :primitive_type
|predicateidentifier(logic_binder, ) =predicate
  (|identifier:predicate⟩) }
logic_type::=logic_arg_type, -> prop
|logic_arg_type, ->primitive_type
logic_arg_type::=primitive_type⟩ | ⟨primitive_typearray
type_parameters::=identifier⟩ | ( (identifier⟩),+ )

Figure 2.3: Syntax of logic declarations


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.

computation_type::={ [ ⟨precondition⟩ ] }
  [ returnsidentifier: ] ⟨value_type⟩ ⟨effects
  { [ ⟨postcondition⟩ ] }
effects::=[ readsidentifier, ] [ writesidentifier, ] [ raisesidentifier, ]
postcondition::=assertion⟩ ⟨exn_condition
assertion::=predicate⟩ [ asidentifier⟩ ]

Figure 2.4: Syntax of types

 |identifier[prog] :=prog
 |prog⟩ ⟨infix⟩ ⟨prog
 |prefix⟩ ⟨prog
 |letidentifier= refproginprog
 |ifprogthenprog⟩ [ elseprog⟩ ]
 |whileprogdo [ ⟨loop_annot⟩ ] ⟨progdone
 |assert ({assertion})+ ;prog
 |letidentifier⟩ ⟨binders=proginprog
 |let recrecfun⟩ [ inprog⟩ ]
 |prog⟩ ⟨prog
 |raiseidentifier⟩ [ :value_type⟩ ]
 |raise (identifier⟩ ⟨prog) [ :value_type⟩ ]
 |tryprogwithhandler|+ end
 |absurd [ :value_type⟩ ]
infix::=+ | - | * | / | = | <> | < | <= | > | >= | || | &&
prefix::=- | not
binders::=(identifier,+ :value_type)+
recfun::=identifier⟩ ⟨binders: value_type
  { variantwf_arg} =prog
loop_annot::={ [ invariantassertion⟩ ] [ variantwf_arg⟩ ] }
wf_arg::=term⟩ [ foridentifier⟩ ]
 |identifier⟩ ⟨identifier->prog

Figure 2.5: Syntax of annotated programs

declaration::=letidentifier⟩ [ ⟨binders⟩ ] =prog
 |let recrecfun
 |[ external ] parameteridentifier,+ :value_type
|exceptionidentifier⟩ [ ofprimitive_type⟩ ]

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:

    τ ::= α  |  (τ,…,τ) s 
    t ::= x  |  f(t,…,t
    P ::= p(t,…,t
 |  ⊤  |  ⊥  |  P ∧ P  |  P ∨ P  |  ¬ P  |  P⇒ P 
 |  ∀ x:τ. P  |  ∃ x:τ. P

A theory Σ is a finite list of declarations δ where

  δ ::= 
 s  |  x:τ  |  logic f:∀
. τ,…,τ→τ 
      logic p:∀
. τ,…,τ→prop  |   axiom ∀
P  |  lemma ∀
P  |  goal ∀


Well-formed types (Σ⊢τ wf):

Σ⊢α wf
type (α1,…,αns∈Σ    ∀ i, Σ⊢τi wf
Σ⊢(τ1,…,τns wf

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

Σ⊢ x
      logic f:∀
. τ1,…,τn→τ∈Σ 
      Subst(σ,Σ)    ∀ i,  Σ⊢ ti:σ(τi
Σ⊢ f(t1,…,tn):σ(τ)
where σ is a mapping from type variables to types, naturally extended to types with σ((τ1,…,τns) = (σ(τ1),…,σ(τn)) s. We write Subst(σ,Σ) whenever Σ⊢σ(α) wf holds for any type variable α.

Well-typed predicates (Σ⊢P wf):

      logic p:∀
. τ1,…,τnprop∈Σ    Subst(σ,Σ)    ∀ i, Σ⊢ ti:σ(τi
Σ⊢⊤ wf
Σ⊢⊥ wf
Σ⊢P1 wf    Σ⊢P2 wf
Σ⊢P1∧ P2 wf
Σ⊢P1 wf    Σ⊢P2 wf
Σ⊢P1∨ P2 wf
Σ⊢P wf
Σ⊢¬ P wf
Σ⊢P1 wf    Σ⊢P2 wf
Σ⊢P1⇒ P2 wf
Σ,x:τ⊢P wf
Σ⊢∀ x:τ. P wf
Σ,x:τ⊢P wf
Σ⊢∃ x:τ. P wf

Well-formed theories (⊢Σ wf):

⊢∅ wf
type s∉Σ
⊢Σ,type (α1,…,αns wf
x∉Σ    Σ⊢τ wf
⊢Σ,x:τ wf
logic f∉Σ    ∀ i,  Σ⊢τi wf
⊢Σ,logic f:∀
. τ1,…,τn→τn+1 wf
logic p∉Σ    ∀ i,  Σ⊢τi wf
⊢Σ,logic p:∀
. τ1,…,τnprop wf
Σ⊢P wf
⊢Σ,axiom ∀
P wf
Σ⊢P wf
⊢Σ,goal ∀
P wf

Well-formed definitions of functions and predicates:

Σ⊢τi wf    Σ,x11,…,xnn⊢ t
Σ⊢function f(x11,…,xnn) : τ = t wf
Σ⊢τi wf    Σ,x11,…,xnnP wf
Σ⊢predicate p(x11,…,xnn) = P wf

Then, as far as typing and validity in concerned, the function f (resp. the predicate p) is added to Σ as logic f1,…,τn→τ (resp. logic p1,…,τnprop).


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.

axiom ∀
P∈Σ    Subst(σ,Σ)
Σ⊨ Q     Σ,Q⊨ P
Σ⊨ P
Σ⊨⊥    Σ⊢P wf
Σ⊨ P
Σ⊢P wf
Σ⊨ P∨¬ P
Σ⊨ P    Σ⊨ Q
Σ⊨ P∧ Q
Σ⊨ P∧ Q
Σ⊨ P
Σ⊨ P∧ Q
Σ⊨ Q
Σ⊨ P    Σ⊢Q wf
Σ⊨ P∨ Q
Σ⊨ Q    Σ⊢P wf
Σ⊨ P∨ Q
Σ⊨ P∨ Q    Σ,P⊨ R    Σ,Q⊨ R
Σ⊨ R
Σ⊢P wf    Σ,P⊨⊥
Σ⊨¬ P
Σ⊨ P    Σ⊨¬ P
Σ⊢P wf    Σ,P⊨ Q
Σ⊨ P⇒ Q
Σ⊨ P⇒ Q    Σ⊨ P
Σ⊨ Q
x∉Σ    Σ⊢τ wf     Σ,x:τ⊨ P
Σ⊨∀ x:τ. P
Σ⊨∀ x:τ. P    Σ⊢ t
Σ⊨ P[t/x]
Σ⊢ t:τ    x∉Σ    Σ⊨ P[t/x]
Σ⊨∃ x:τ. P
Σ⊨∃ x:τ. P    x∉Σ    Σ,x:τ,P⊨ Q
Σ⊨ Q

Deduction rules for equality:

Σ⊢ t
Σ⊨ t=t
Σ⊨ x=y    Σ,z:τ⊢P wf     Σ⊨ P[x/z]
Σ⊨ P[y/z]

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 x1,…,xn are the free variables of P, we write x1,…,xnA P whenever P is valid in Presburger arithmetic (which is decidable). Then we have the following deduction rule for arithmetic:

x1,…,xnA P
Σ⊨∀ x1:int. …∀ xn:int.  P

2.3.2  Programs

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

    θ ::= τ  |  τ ref  |  (x:θ) →κ 
    κ ::= {p} θ є {q
    q ::= p;E⇒ p;…;E⇒ p 
    є ::=     reads x,…,x writes x,…,x   raises E,…,E 

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, (x11)→⋯→(xnn)→κ 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
 raise (E e):θ 
 try e with E xe end 
 assert {p}; e 
 e {q
 e {{q}} 
 fun (x:θ)→{pe 
 rec x (x:θ)…(x:θ):θ {variant t}={pe 
 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 e2:

e1; e2  ≡  let _ = e1 in e2

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

  x := e  ≡  ref_set x e

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

  raise E  ≡  raise (E void):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:

    while e1 do e2 {invariant p variant t}  ≡ 
          loop   if e1 then e2 else raise Exit 
          {invariant   p   variant   t
       with   Exit _   ->   void   end


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 = E1q1; …; Enqn 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:

    wp(t,q;r)q[result ← t
wp(let x = e1 in e2,q;r)= wp(e1,wp(e2,q;r)[xresult];r
    wp(let x = ref e1 in e2,q;r)= wp(e1,wp(e2,q;r)[xresult];r
    wp(if e1 then e2 else e3,q;r)= wp(e1,if result then wp(e2,q;relse wp(e3,q;r);r
    wp(L:e,q;r)= wp(e,q;r)[at(x,L)← x

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

  wp(e1; e2,q) = wp(e1,wp(e2,q))

The cases of exceptions and annotations are also straightforward:

    wp(raise (E e):θ,q;r)wp(e,r(E);r
    wp(try e1 with E xe2 end,q;r)wp(e1,q;Ewp(e2,q;r)[xresult];r
       wp(assert {p}; e,q;r)= p ∧ wp(e,q;r
    wp(e {q′;r′},q;r)= wp(e,q′ ∧ q;r′∧ r
    wp(e {{q′;r′}},q;r)= wp(e,q′;r′) ∧ ∀ω.∀result.q′⇒ q∧ r′⇒ r 

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:

    wp(loop e {invariant p variant t},q;r)p  ∧  ∀ω.    p ⇒ wp(L:e,p∧ t<at(t,L);r

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:

 wp(while e1 do e2 {invariant p variant t},q;r
   =p  ∧  ∀ω.   p ⇒ 
 wp(L:if e1 then e2 else raise E, p∧ t<at(t,L),E⇒ q;r
   =p  ∧  ∀ω.   p ⇒ 
 wp(e1,if result then wp(e2,p∧ t<at(t,L)) else q,r)[at(x,L)← x]

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:

    wp(fun (x:θ)→{pe,q;r)q  ∧  ∀ x.∀ρ. p ⇒wp(e,True)
    wp(rec f (x11)…(xnn):θ {variant t}={pe,q;r)
q  ∧  ∀ x1.…∀ xn.∀ρ.  p ⇒wp(L:e,True)

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 (x11)→⋯→(xnn)→{pt<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 ee2 can be simplified to the case of an application x1 x2 of one variable to another, using the following transformation if needed:

    e1 e2 ≡  let x1 = e1 in let x2 = e2 in x1 x2

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

  wp(x1 x2,q) = p′[x← x2]  ∧  ∀ω. ∀result.  (q′[x← x2] ⇒ q)[old(t)← t]

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

  wp(x := e,q;r) = wp(e,x=result ⇒ q;r

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

  wp(x := t,q) = (x=t ⇒ q)

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

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

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

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

(* 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 are mapped as follows:

τ array(array τ), from module WhyArrays

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

: repeatedly simplifies access/updateusing combinations and array_length expressions
: rewrites access (update t i vi into v, simplifies with WhyArrays and attempts omega on every subgoal
: rewrites access (update t i vj 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 are mapped as follows:

unitunit, from theory why
τ arraywarray[τ], from theory why

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.

Previous Up Next