4. The Why3 API

This chapter is a tutorial for the users who want to link their own OCaml code with the Why3 library. We progressively introduce the way one can use the library to build terms, formulas, theories, proof tasks, call external provers on tasks, and apply transformations on tasks. The complete documentation for API calls is given at URL http://why3.lri.fr/api-1.5/.

We assume the reader has a fair knowledge of the OCaml language. Notice that the Why3 library must be installed, see Section 5.1.3.2. The OCaml code given below is available in the source distribution in directory examples/use_api/ together with a few other examples.

4.1. Building Propositional Formulas

The first step is to know how to build propositional formulas. The module Term gives a few functions for building these. Here is a piece of OCaml code for building the formula true \/ false.

(* opening the Why3 library *)
open Why3

(* a ground propositional goal: true or false *)
let fmla_true : Term.term = Term.t_true
let fmla_false : Term.term = Term.t_false
let fmla1 : Term.term = Term.t_or fmla_true fmla_false

The library uses the common type term both for terms (i.e., expressions that produce a value of some particular type) and formulas (i.e., Boolean-valued expressions).

Such a formula can be printed using the module Pretty providing pretty-printers.

(* printing it *)
open Format
let () = printf "@[formula 1 is:@ %a@]@." Pretty.print_term fmla1

Assuming the lines above are written in a file f.ml, it can be compiled using

ocamlfind ocamlc -package why3 -linkpkg f.ml -o f

Running the generated executable f results in the following output.

formula 1 is: true \/ false

Let us now build a formula with propositional variables: A /\ B -> A. Propositional variables must be declared first before using them in formulas. This is done as follows.

let prop_var_A : Term.lsymbol =
  Term.create_psymbol (Ident.id_fresh "A") []
let prop_var_B : Term.lsymbol =
  Term.create_psymbol (Ident.id_fresh "B") []

The type lsymbol is the type of function and predicate symbols (which we call logic symbols for brevity). Then the atoms A and B must be built by the general function for applying a predicate symbol to a list of terms. Here we just need the empty list of arguments.

let atom_A : Term.term = Term.ps_app prop_var_A []
let atom_B : Term.term = Term.ps_app prop_var_B []
let fmla2 : Term.term =
  Term.t_implies (Term.t_and atom_A atom_B) atom_A
let () = printf "@[formula 2 is:@ %a@]@." Pretty.print_term fmla2

As expected, the output is as follows.

formula 2 is: A /\ B -> A

Notice that the concrete syntax of Why3 forbids function and predicate names to start with a capital letter (except for the algebraic type constructors which must start with one). This constraint is not enforced when building those directly using library calls.

4.2. Building Tasks

Let us see how we can call a prover to prove a formula. As said in previous chapters, a prover must be given a task, so we need to build tasks from our formulas. Task can be build incrementally from an empty task by adding declaration to it, using the functions add_*_decl of module Task. For the formula true \/ false above, this is done as follows.

(* building the task for formula 1 alone *)
let task1 : Task.task = None (* empty task *)
let goal_id1 : Decl.prsymbol = Decl.create_prsymbol (Ident.id_fresh "goal1")
let task1 : Task.task = Task.add_prop_decl task1 Decl.Pgoal goal_id1 fmla1

To make the formula a goal, we must give a name to it, here “goal1”. A goal name has type prsymbol, for identifiers denoting propositions in a theory or a task. Notice again that the concrete syntax of Why3 requires these symbols to be capitalized, but it is not mandatory when using the library. The second argument of add_prop_decl is the kind of the proposition: Paxiom, Plemma or Pgoal. Notice that lemmas are not allowed in tasks and can only be used in theories.

Once a task is built, it can be printed.

(* printing the task *)
let () = printf "@[task 1 is:@\n%a@]@." Pretty.print_task task1

The task for our second formula is a bit more complex to build, because the variables A and B must be added as abstract (i.e., not defined) propositional symbols in the task.

(* task for formula 2 *)
let task2 = None
let task2 = Task.add_param_decl task2 prop_var_A
let task2 = Task.add_param_decl task2 prop_var_B
let goal_id2 = Decl.create_prsymbol (Ident.id_fresh "goal2")
let task2 = Task.add_prop_decl task2 Decl.Pgoal goal_id2 fmla2
let () = printf "@[task 2 created:@\n%a@]@." Pretty.print_task task2

Execution of our OCaml program now outputs:

task 1 is:
theory Task
  goal Goal1 : true \/ false
end

task 2 is:
theory Task
  predicate A

  predicate B

  goal Goal2 : A /\ B -> A
end

4.3. Calling External Provers

To call an external prover, we need to access the Why3 configuration file why3.conf, as it was built using the why3 config command line tool or the Detect Provers menu of the graphical IDE. The following API calls make it possible to access the content of this configuration file.

(* reads the default config file *)
let config : Whyconf.config = Whyconf.init_config None
(* the [main] section of the config file *)
let main : Whyconf.main = Whyconf.get_main config
(* the library and data directories, from the config file *)
let libdir = Whyconf.libdir main
let datadir = Whyconf.datadir main
(* all the provers detected, from the config file *)
let provers : Whyconf.config_prover Whyconf.Mprover.t =
  Whyconf.get_provers config

The type 'a Whyconf.Mprover.t is a map indexed by provers. A prover is a record with a name, a version, and an alternative description (to differentiate between various configurations of a given prover). Its definition is in the module Whyconf:

type prover =
    { prover_name : string;
      prover_version : string;
      prover_altern : string;
    }

The map provers provides the set of existing provers. In the following, we directly attempt to access a prover named “Alt-Ergo”, any version.

(* One prover named Alt-Ergo in the config file *)
let alt_ergo : Whyconf.config_prover =
  let fp = Whyconf.parse_filter_prover "Alt-Ergo" in
  (** all provers that have the name "Alt-Ergo" *)
  let provers = Whyconf.filter_provers config fp in
  if Whyconf.Mprover.is_empty provers then begin
      eprintf "Prover Alt-Ergo not installed or not configured@.";
      exit 1
    end else begin
      printf "Versions of Alt-Ergo found:";
      Whyconf.(Mprover.iter (fun k _ -> printf " %s" k.prover_version) provers);
      printf "@.";
      (* returning an arbitrary one *)
      snd (Whyconf.Mprover.max_binding provers)
    end

We could also get a specific version with

(* Specific version 2.3.3 of Alt-Ergo in the config file *)
let _ : Whyconf.config_prover =
  let fp = Whyconf.parse_filter_prover "Alt-Ergo,2.3.3" in
  let provers = Whyconf.filter_provers config fp in
  if Whyconf.Mprover.is_empty provers then begin
      eprintf "Prover Alt-Ergo 2.3.3 not installed or not configured, using version %s instead@."
        Whyconf.(alt_ergo.prover.prover_version) ;
    alt_ergo (* we don't want to fail this time *)
  end else
    snd (Whyconf.Mprover.max_binding provers)

The next step is to obtain the driver associated to this prover. A driver typically depends on the standard theories so these should be loaded first.

(* builds the environment from the [loadpath] *)
let env : Env.env = Env.create_env (Whyconf.loadpath main)

(* loading the Alt-Ergo driver *)
let alt_ergo_driver : Driver.driver =
  try
    Whyconf.load_driver main env alt_ergo
  with e ->
    eprintf "Failed to load driver for alt-ergo: %a@."
      Exn_printer.exn_printer e;
    exit 1

We are now ready to call the prover on the tasks. This is done by a function call that launches the external executable and waits for its termination. Here is a simple way to proceed:

(* calls Alt-Ergo *)
let result1 : Call_provers.prover_result =
  Call_provers.wait_on_call
    (Driver.prove_task
       ~limit:Call_provers.empty_limit
       ~libdir
       ~datadir
       ~command:alt_ergo.Whyconf.command
       alt_ergo_driver
       task1)

(* prints Alt-Ergo answer *)
let () = printf "@[On task 1, Alt-Ergo answers %a@."
    (Call_provers.print_prover_result ?json:None) result1

This way to call a prover is in general too naive, since it may never return if the prover runs without time limit. The function prove_task has an optional parameter limit, a record defined in module Call_provers:

type resource_limit = {
  limit_time  : int;
  limit_mem   : int;
  limit_steps : int;
}

where the field limit_time is the maximum allowed running time in seconds, and limit_mem is the maximum allowed memory in megabytes. The type prover_result is a record defined in module Call_provers:

type prover_result = {
  pr_answer : prover_answer;
  pr_status : Unix.process_status;
  pr_output : string;
  pr_time   : float;
  pr_steps  : int;		(* -1 if unknown *)
  pr_models : (prover_answer * model) list;
}

with in particular the fields:

• pr_answer: the prover answer, explained below;

• pr_time: the time taken by the prover, in seconds.

A pr_answer is the sum type defined in module Call_provers:

type prover_answer =
  | Valid
  | Invalid
  | Timeout
  | OutOfMemory
  | StepLimitExceeded
  | Unknown of string
  | Failure of string
  | HighFailure

corresponding to these kinds of answers:

• Valid: the task is valid according to the prover.

• Invalid: the task is invalid.

• Timeout: the prover exceeds the time limit.

• OutOfMemory: the prover exceeds the memory limit.

• Unknown msg: the prover cannot determine if the task is valid; the string parameter msg indicates some extra information.

• Failure msg: the prover reports a failure, it was unable to read correctly its input task.

• HighFailure: an error occurred while trying to call the prover, or the prover answer was not understood (none of the given regular expressions in the driver file matches the output of the prover).

Here is thus another way of calling the Alt-Ergo prover, on our second task.

let result2 : Call_provers.prover_result =
  Call_provers.wait_on_call
    (Driver.prove_task
       ~command:alt_ergo.Whyconf.command
       ~libdir
       ~datadir
       ~limit:{Call_provers.empty_limit with Call_provers.limit_time = 10}
       alt_ergo_driver
       task2)

let () = printf "@[On task 2, Alt-Ergo answers %a in %5.2f seconds@."
  Call_provers.print_prover_answer result1.Call_provers.pr_answer
  result1.Call_provers.pr_time

The output of our program is now as follows.

On task 1, alt-ergo answers Valid (0.01s)
On task 2, alt-ergo answers Valid in  0.01 seconds

4.4. Building Terms

An important feature of the functions for building terms and formulas is that they statically guarantee that only well-typed terms can be constructed.

Here is the way we build the formula 2+2=4. The main difficulty is to access the internal identifier for addition: it must be retrieved from the standard theory Int of the file int.why.

let two  : Term.term = Term.t_nat_const 2
let four : Term.term = Term.t_nat_const 4
let int_theory : Theory.theory = Env.read_theory env ["int"] "Int"
let plus_symbol : Term.lsymbol =
  Theory.ns_find_ls int_theory.Theory.th_export ["infix +"]
let two_plus_two : Term.term = Term.t_app_infer plus_symbol [two;two]
let fmla3 : Term.term = Term.t_equ two_plus_two four

An important point to notice as that when building the application of + to the arguments, it is checked that the types are correct. Indeed the constructor t_app_infer infers the type of the resulting term. One could also provide the expected type as follows.

let two_plus_two : Term.term = Term.fs_app plus_symbol [two;two] Ty.ty_int

When building a task with this formula, we need to declare that we use theory Int:

let task3 = None
let task3 = Task.use_export task3 int_theory
let goal_id3 = Decl.create_prsymbol (Ident.id_fresh "goal3")
let task3 = Task.add_prop_decl task3 Decl.Pgoal goal_id3 fmla3

4.5. Building Quantified Formulas

To illustrate how to build quantified formulas, let us consider the formula \(\forall x:int. x \cdot x \geq 0\). The first step is to obtain the symbols from Int.

let zero : Term.term = Term.t_nat_const 0
let mult_symbol : Term.lsymbol =
  Theory.ns_find_ls int_theory.Theory.th_export ["infix *"]
let ge_symbol : Term.lsymbol =
  Theory.ns_find_ls int_theory.Theory.th_export ["infix >="]

The next step is to introduce the variable x with the type int.

let var_x : Term.vsymbol =
  Term.create_vsymbol (Ident.id_fresh "x") Ty.ty_int

The formula \(x \cdot x \geq 0\) is obtained as in the previous example.

let x : Term.term = Term.t_var var_x
let x_times_x : Term.term = Term.t_app_infer mult_symbol [x;x]
let fmla4_aux : Term.term = Term.ps_app ge_symbol [x_times_x;zero]

To quantify on x, we use the appropriate smart constructor as follows.

let fmla4 : Term.term = Term.t_forall_close [var_x] [] fmla4_aux

4.6. Building Theories

We illustrate now how one can build theories. Building a theory must be done by a sequence of calls:

• creating a theory “under construction”, of type Theory.theory_uc;

• adding declarations, one at a time;

• closing the theory under construction, obtaining something of type Theory.theory.

Creation of a theory named My_theory is done by

let my_theory : Theory.theory_uc =
  Theory.create_theory (Ident.id_fresh "My_theory")

First let us add formula 1 above as a goal:

let my_theory : Theory.theory_uc =
  Theory.create_theory (Ident.id_fresh "My_theory")

Note that we reused the goal identifier goal_id1 that we already defined to create task 1 above.

Adding formula 2 needs to add the declarations of predicate variables A and B first:

let my_theory : Theory.theory_uc =
  Theory.add_param_decl my_theory prop_var_A
let my_theory : Theory.theory_uc =
  Theory.add_param_decl my_theory prop_var_B
let decl_goal2 : Decl.decl =
  Decl.create_prop_decl Decl.Pgoal goal_id2 fmla2
let my_theory : Theory.theory_uc = Theory.add_decl my_theory decl_goal2

Adding formula 3 is a bit more complex since it uses integers, thus it requires to “use” the theory int.Int. Using a theory is indeed not a primitive operation in the API: it must be done by a combination of an “export” and the creation of a namespace. We provide a helper function for that:

(* helper function: [use th1 th2] insert the equivalent of a
   "use import th2" in theory th1 under construction *)
let use th1 th2 =
  let name = th2.Theory.th_name in
  Theory.close_scope
    (Theory.use_export (Theory.open_scope th1 name.Ident.id_string) th2)
    ~import:true

Addition of formula 3 is then

let my_theory : Theory.theory_uc = use my_theory int_theory
let decl_goal3 : Decl.decl =
  Decl.create_prop_decl Decl.Pgoal goal_id3 fmla3
let my_theory : Theory.theory_uc = Theory.add_decl my_theory decl_goal3

Addition of goal 4 is nothing more complex:

let decl_goal4 : Decl.decl =
  Decl.create_prop_decl Decl.Pgoal goal_id4 fmla4
let my_theory : Theory.theory_uc = Theory.add_decl my_theory decl_goal4

Finally, we close our theory under construction as follows.

let my_theory : Theory.theory = Theory.close_theory my_theory

We can inspect what we did by printing that theory:

let () = printf "@[my new theory is as follows:@\n@\n%a@]@."
                Pretty.print_theory my_theory

which outputs

my new theory is as follows:

theory My_theory
  (* use BuiltIn *)

  goal goal1 : true \/ false

  predicate A

  predicate B

  goal goal2 : A /\ B -> A

  (* use int.Int *)

  goal goal3 : (2 + 2) = 4

  goal goal4 : forall x:int. (x * x) >= 0
end

From a theory, one can compute at once all the proof tasks it contains as follows:

let my_tasks : Task.task list =
  List.rev (Task.split_theory my_theory None None)

Note that the tasks are returned in reverse order, so we reverse the list above.

We can check our generated tasks by printing them:

let () =
  printf "Tasks are:@.";
  let _ =
    List.fold_left
      (fun i t -> printf "Task %d: %a@." i Pretty.print_task t; i+1)
      1 my_tasks
  in ()

One can run provers on those tasks exactly as we did above.

4.7. Operations on Terms and Formulas, Transformations

The following code illustrates a simple recursive functions of formulas. It explores the formula and when a negation is found, it tries to push it down below a conjunction, a disjunction or a quantifier.

open Term

let rec negate (t:term) : term =
  match t.t_node with
  | Ttrue -> t_false
  | Tfalse -> t_true
  | Tnot t -> t
  | Tbinop(Tand,t1,t2) -> t_or (negate t1) (negate t2)
  | Tbinop(Tor,t1,t2) -> t_and (negate t1) (negate t2)
  | Tquant(Tforall,tq) ->
     let vars,triggers,t' = t_open_quant tq in
     let tq' = t_close_quant vars triggers (negate t') in
     t_exists tq'
  | Tquant(Texists,tq) ->
     let vars,triggers,t' = t_open_quant tq in
     let tq' = t_close_quant vars triggers (negate t') in
     t_forall tq'
  | _ -> t_not t

let rec traverse (t:term) : term =
  match t.t_node with
  | Tnot t -> t_map traverse (negate t)
  | _ -> t_map traverse t

The following illustrates how to turn such an OCaml function into a transformation in the sense of the Why3 API. Moreover, it registers that transformation to make it available for example in Why3 IDE.

let negate_goal pr t = [Decl.create_prop_decl Decl.Pgoal pr (traverse t)]

let negate_trans = Trans.goal negate_goal

let () = Trans.register_transform
           "push_negations_down" negate_trans
           ~desc:"In the current goal,@ push negations down,@ \
                  across logical connectives."

The directory src/transform contains the code for the many transformations that are already available in Why3.

4.8. Proof Sessions

See the example examples/use_api/create_session.ml of the distribution for an illustration on how to manipulate proof sessions from an OCaml program.

4.9. ML Programs

One can build WhyML programs starting at different steps of the WhyML pipeline (parsing, typing, VC generation). We present here two choices. The first is to build an untyped syntax trees, and then call the Why3 typing procedure to build typed declarations. The second choice is to directly build the typed declaration. The first choice use concepts similar to the WhyML language but errors in the generation are harder to debug since they are lost inside the typing phase, the second choice use more internal notions but it is easier to pinpoint the functions wrongly used. Section 4.9.1 and Section 4.9.4 follow choice one and Section 4.9.5 choice two.

4.9.1. Untyped syntax tree

The examples of this section are available in the file examples/use_api/mlw_tree.ml of the distribution.

The first step is to build an environment as already illustrated in Section 4.3, open the OCaml module Ptree (“parse tree”) which contains the type constructors for the parsing trees, and finally the OCaml module Ptree_helpers which contains helpers for building those trees and a more concise and friendly manner than the low-level constructors. The latter two OCaml modules are documented in the online API documentation, respectively for Ptree and Ptree_helpers.

open Why3
let config : Whyconf.config = Whyconf.init_config None
let main : Whyconf.main = Whyconf.get_main config
let libdir = Whyconf.libdir main
let datadir = Whyconf.datadir main
let env : Env.env = Env.create_env (Whyconf.loadpath main)
open Ptree
open Ptree_helpers

Each of our example programs will build a module. Let us consider the Why3 code.

module M1
  use int.Int
  goal g : 2 + 2 = 4
end

The Ocaml code that programmatically builds it is as follows.

let mod_M1 =
  (* use int.Int *)
  let use_int_Int = use ~import:false (["int";"Int"]) in
  (* goal g : 2 + 2 = 4 *)
  let g =
    let two = tconst 2 in
    let four = tconst 4 in
    let add_int = qualid ["Int";Ident.op_infix "+"] in
    let two_plus_two = tapp add_int [two ; two] in
    let eq_int = qualid ["Int";Ident.op_infix "="] in
    let goal_term = tapp eq_int  [four ; two_plus_two] in
    Dprop(Decl.Pgoal, ident "g", goal_term)
  in
  (ident "M1",[use_int_Int ; g])

Most of the code is not using directly the Ptree constructors but instead makes uses of the helper functions that are given in the Ptree_helpers module. Notice ident which builds an identifier (type Ptree.ident) optionally with attributes and location and use which lets us import some other modules and in particular the ones from the standard library. At the end, our module is no more than the identifier and a list of two declarations (Ptree.decl list).

We want now to build a program equivalent to the following code in concrete Why3 syntax.

module M2
  let f (x:int) : int
    requires { x=6 }
    ensures { result=42 }
   = x*7
end

The OCaml code that programmatically build this Why3 function is as follows.

let eq_symb = qualid [Ident.op_infix "="]
let int_type_id = qualid ["int"]
let int_type = PTtyapp(int_type_id,[])
let mul_int = qualid ["Int";Ident.op_infix "*"]

let mod_M2 =
  (* use int.Int *)
  let use_int_Int = use ~import:false (["int";"Int"]) in
  (* f *)
  let f =
    let id_x = ident "x" in
    let pre = tapp eq_symb [tvar (Qident id_x); tconst 6] in
    let result = ident "result" in
    let post = tapp eq_symb [tvar (Qident result); tconst 42] in
    let spec = {
      sp_pre = [pre];
      sp_post = [Loc.dummy_position,[pat_var result,post]];
      sp_xpost = [];
      sp_reads = [];
      sp_writes = [];
      sp_alias = [];
      sp_variant = [];
      sp_checkrw = false;
      sp_diverge = false;
      sp_partial = false;
    }
    in
    let body = eapp mul_int [evar (Qident id_x); econst 7] in
    let f =
      Efun(one_binder ~pty:int_type "x", None, pat Pwild,
           Ity.MaskVisible, spec, body)
    in
    Dlet(ident "f",false,Expr.RKnone, expr f)
  in
  (ident "M2",[use_int_Int ; f])

We want now to build a program equivalent to the following code in concrete Why3 syntax.

module M3
  let f() : int
     requires { true }
     ensures { result >= 0 }
   = let x = ref 42 in !x
end

We need to import the ref.Ref module first. The rest is similar to the first example, the code is as follows.

let ge_int = qualid ["Int";Ident.op_infix ">="]

let mod_M3 =
  (* use int.Int *)
  let use_int_Int = use ~import:false (["int";"Int"]) in
  (* use ref.Ref *)
  let use_ref_Ref = use ~import:false (["ref";"Ref"]) in
  (* f *)
  let f =
    let result = ident "result" in
    let post = term(Tidapp(ge_int,[tvar (Qident result);tconst 0])) in
    let spec = {
      sp_pre = [];
      sp_post = [Loc.dummy_position,[pat_var result,post]];
      sp_xpost = [];
      sp_reads = [];
      sp_writes = [];
      sp_alias = [];
      sp_variant = [];
      sp_checkrw = false;
      sp_diverge = false;
      sp_partial = false;
    }
    in
    let body =
      let e1 = eapply (evar (qualid ["Ref";"ref"])) (econst 42) in
      let id_x = ident "x" in
      let qid = qualid ["Ref";Ident.op_prefix "!"] in
      let e2 = eapply (evar qid) (evar (Qident id_x)) in
      expr(Elet(id_x,false,Expr.RKnone,e1,e2))
    in
    let f = Efun(unit_binder (),None,pat Pwild,Ity.MaskVisible,spec,body)
    in
    Dlet(ident "f",false,Expr.RKnone, expr f)
  in
  (ident "M3",[use_int_Int ; use_ref_Ref ; f])

The next example makes use of arrays.

module M4
  let f (a:array int) : unit
    requires { a.length >= 1 }
    ensures { a[0] = 42 }
   = a[0] <- 42
end

The corresponding OCaml code is as follows.

let array_int_type = PTtyapp(qualid ["Array";"array"],[int_type])

let length = qualid ["Array";"length"]

let array_get = qualid ["Array"; Ident.op_get ""]

let array_set = qualid ["Array"; Ident.op_set ""]

let mod_M4 =
  (* use int.Int *)
  let use_int_Int = use ~import:false (["int";"Int"]) in
  (* use array.Array *)
  let use_array_Array = use ~import:false (["array";"Array"]) in
  (* use f *)
  let f =
    let id_a = ident "a" in
    let pre =
      tapp ge_int [tapp length [tvar (Qident id_a)]; tconst 1]
    in
    let post =
      tapp eq_symb [tapp array_get [tvar (Qident id_a); tconst 0];
                       tconst 42]
    in
    let spec = {
      sp_pre = [pre];
      sp_post = [Loc.dummy_position,[pat Pwild,post]];
      sp_xpost = [];
      sp_reads = [];
      sp_writes = [];
      sp_alias = [];
      sp_variant = [];
      sp_checkrw = false;
      sp_diverge = false;
      sp_partial = false;
    }
    in
    let body =
      eapp array_set [evar (Qident id_a); econst 0; econst 42]
    in
    let f = Efun(one_binder ~pty:array_int_type "a",
                 None,pat Pwild,Ity.MaskVisible,spec,body)
    in
    Dlet(ident "f", false, Expr.RKnone, expr f)
  in
  (ident "M4",[use_int_Int ; use_array_Array ; f])

Having declared all the programs we wanted to write, we can now close the module and the file, and get as a result the set of modules of our file.

let mlw_file = Modules [mod_M1 ; mod_M2 ; mod_M3 ; mod_M4]

4.9.2. Alternative, top-down, construction of parsing trees

The way we build our modules above is somehow bottom-up: builds the terms and the program expressions, then the declarations that contain them, then the modules containing the latter declarations. An alternative provided by other helpers is to build those modules in a top-down way, which may be more natural since this the order they occur in the concrete syntax. We show below how to construct a similar list of module as above, with only the last module for conciseness:

let mlw_file =
  let uc = F.create () in
  let uc = F.begin_module uc "M5" in
  let uc = F.use uc ~import:false ["int";"Int"] in
  let uc = F.use uc ~import:false ["array";"Array"] in
  let uc = F.begin_let uc "f" (one_binder ~pty:array_int_type "a") in
  let id_a = Qident (ident "a") in
  let pre = tapp ge_int [tapp length [tvar id_a]; tconst 1] in
  let uc = F.add_pre uc pre in
  let post =
    tapp eq_symb [tapp array_get [tvar id_a; tconst 0];
                  tconst 42]
  in
  let uc = F.add_post uc post in
  let body = eapp array_set [evar id_a; econst 0; econst 42] in
  let uc = F.add_body uc body in
  let uc = F.end_module uc in
  F.get_mlw_file uc

The construction above is functional, in the sense that the uc variable holds the necessary data for the modules under construction. For simplicity it is also possible to use an imperative variant which transparently handles the state of modules under construction.

let mlw_file =
  I.begin_module "M6";
  I.use ~import:false ["int";"Int"];
  I.use ~import:false ["array";"Array"];
  I.begin_let "f" (one_binder ~pty:array_int_type "a");
  let id_a = Qident (ident "a") in
  let pre = tapp ge_int [tapp length [tvar id_a]; tconst 1] in
  I.add_pre pre;
  let post =
    tapp eq_symb [tapp array_get [tvar id_a; tconst 0];
                  tconst 42]
  in
  I.add_post post;
  let body = eapp array_set [evar id_a; econst 0; econst 42] in
  I.add_body body;
  I.end_module ();
  I.get_mlw_file ()

Beware though that the latter approach is not thread-safe and cannot be used in re-entrant manner.

4.9.3. Using the parsing trees

Module Mlw_printer provides functions to print elements of Ptree in concrete whyml syntax.

let () = printf "%a@." (Mlw_printer.pp_mlw_file ~attr:true) mlw_file

The typing of the modules is carried out by function Typing.type_mlw_file, which produces a mapping of module names to typed modules.

let mods = Typing.type_mlw_file env [] "myfile.mlw" mlw_file

Typing errors are reported by exceptions Located of position * exn from module Loc. However, the positions in our declarations, which are provided by the exception, cannot be used to identify the position in the (printed) program, because the locations do not correspond to any concrete syntax.

Alternatively, we can give every Ptree element in our declarations above a unique location (for example using the function Mlw_printer.next_pos). When a located error is encountered, the function Mlw_printer.with_marker can then be used to instruct Mlw_printer to insert the error as a comment just before the syntactic element with the given location.

let _mods =
  try
    Typing.type_mlw_file env [] "myfile.mlw" mlw_file
  with Loc.Located (loc, e) -> (* A located exception [e] *)
    let msg = asprintf "%a" Exn_printer.exn_printer e in
    printf "%a@."
      (Mlw_printer.with_marker ~msg loc (Mlw_printer.pp_mlw_file ~attr:true))
      mlw_file;
    exit 1

Finally, we can then construct the proofs tasks for our typed module, and then try to call the Alt-Ergo prover. The rest of that code is using OCaml functions that were already introduced before.

let my_tasks : Task.task list =
  let mods =
    Wstdlib.Mstr.fold
      (fun _ m acc ->
       List.rev_append
         (Task.split_theory m.Pmodule.mod_theory None None) acc)
      mods []
  in List.rev mods



let provers : Whyconf.config_prover Whyconf.Mprover.t =
  Whyconf.get_provers config

let alt_ergo : Whyconf.config_prover =
  let fp = Whyconf.parse_filter_prover "Alt-Ergo,2.3.3" in
  let provers = Whyconf.filter_provers config fp in
  if Whyconf.Mprover.is_empty provers then begin
    eprintf "Prover Alt-Ergo 2.3.3 not installed or not configured@.";
    exit 1
  end else
    snd (Whyconf.Mprover.max_binding provers)

let alt_ergo_driver : Driver.driver =
  try
    Whyconf.load_driver main env alt_ergo
  with e ->
    eprintf "Failed to load driver for alt-ergo: %a@."
      Exn_printer.exn_printer e;
    exit 1

let () =
  List.iteri (fun i t ->
      let call =
        Driver.prove_task ~limit:Call_provers.empty_limit
          ~libdir ~datadir
          ~command:alt_ergo.Whyconf.command alt_ergo_driver t in
      let r = Call_provers.wait_on_call call in
      printf "@[On task %d, alt-ergo answers %a@." (succ i)
        (Call_provers.print_prover_result ?json:None) r)
    my_tasks

4.9.4. Use attributes to infer loop invariants

In this section we build a module containing a let declaration with a while loop and an attribute that triggers the inference of loop invariants during VC generation. For more information about the inference of loop invariants refer to Section 5.5 and Section 8.5. The examples shown below are available in the file examples/use_api/mlw_tree_infer_invs.ml.

We build an environment and define the some helper functions exactly as in Section 4.9.1. Additionally we create two other helper functions as follows:

(* ... *)
let pat_wild = mk_pat Pwild
let pat_var id = mk_pat (Pvar id)

let mk_ewhile e1 i v e2 = mk_expr (Ewhile (e1,i,v,e2))

Our goal is now to build a program equivalent to the following. Note that the let declaration contains an attribute [@infer] which will trigger the inference of loop invariants during VC generation (make sure that the why3 library was compiled with support for infer-loop, see Section 5.5 for more information).

module M1
  use int.Int
  use ref.Refint
  let f [@infer] (x:ref int) : unit
    requires { !x <= 100 }
    ensures  { !x = 100 }
  = while (!x < 100) do
      variant { 100 - !x }
      incr x
    done
end

The OCaml code that builds such a module is shown below.

let int_type_id  = mk_qualid ["int"]
let int_type     = PTtyapp(int_type_id,[])
let ref_int_type = PTtyapp (mk_qualid ["ref"], [int_type])
let ref_access   = mk_qualid ["Refint"; Ident.op_prefix "!"]
let ref_assign   = mk_qualid ["Refint"; Ident.op_infix ":="]
let ref_int_incr = mk_qualid ["Refint"; "incr"]
let l_int        = mk_qualid ["Int";Ident.op_infix "<"]
let le_int       = mk_qualid ["Int";Ident.op_infix "<="]
let plus_int     = mk_qualid ["Int";Ident.op_infix "+"]
let minus_int    = mk_qualid ["Int";Ident.op_infix "-"]
let eq_symb      = mk_qualid [Ident.op_infix "="]

let mod_M1 =
  (* use int.Int *)
  let use_int_Int    = use_import (["int";"Int"]) in
  let use_ref_Refint = use_import (["ref";"Refint"]) in
  (* f *)
  let f =
    let id_x  = mk_ident "x" in
    let var_x = mk_var id_x in
    let t_x   = mk_tapp ref_access [var_x] in
    let pre   = mk_tapp le_int [t_x; mk_tconst 100] in
    let post  = mk_tapp eq_symb [t_x; mk_tconst 100] in
    let spec  = {
      sp_pre     = [pre];
      sp_post    = [Loc.dummy_position,[pat_var (mk_ident "result"), post]];
      sp_xpost   = [];
      sp_reads   = [];
      sp_writes  = [];
      sp_alias   = [];
      sp_variant = [];
      sp_checkrw = false;
      sp_diverge = false;
      sp_partial = false;
    }
    in
    let var_x      = mk_evar (Qident id_x) in
    (* !x *)
    let e_x        = mk_eapp ref_access [var_x] in
    (* !x < 100 *)
    let while_cond = mk_eapp l_int [e_x; mk_econst 100] in
    (* 100 - !x *)
    let while_vari = mk_tapp minus_int [mk_tconst 100; t_x], None in
    (* incr x *)
    let incr       = mk_apply (mk_evar ref_int_incr) var_x in
    (* while (!x < 100) do variant { 100 - !x } incr x done *)
    let while_loop = mk_ewhile while_cond [] [while_vari] incr in
    let f =
      Efun(param1 id_x ref_int_type, None, mk_pat Pwild,
           Ity.MaskVisible, spec, while_loop)
    in
    let attr = ATstr (Ident.create_attribute "infer") in
    let id = { (mk_ident "f") with id_ats = [attr] } in
    Dlet(id,false,Expr.RKnone, mk_expr f)
  in
  (mk_ident "M1",[use_int_Int; use_ref_Refint; f])

Optionally, the debugging flags mentioned in Section 8.5 can be enabled by using the API as follows (the line(s) corresponding to the desired flag(s) should be uncommented).

(* let () = Debug.set_flag Infer_cfg.infer_print_ai_result *)
(* let () = Debug.set_flag Infer_cfg.infer_print_cfg *)
(* let () = Debug.set_flag Infer_loop.print_inferred_invs *)

Another option is to register a function to be executed immediately after the invariants are inferred. The function should have type (expr * term) list -> unit, where expr corresponds to a while loop and term to the respective inferred invariant. The function can be registered using the function Infer_loop.register_hook.

In the following example a sequence of three functions are registered. The first function will write the invariants to the standard output, the second to a file named inferred_invs.out, and the third will save the inferred invariants in inv_terms.

let print_to_std invs =
  let print_inv fmt (_,t) = Pretty.print_term fmt t in
  Format.printf "The following invariants were generated:@\n%a@."
    (Pp.print_list Pp.newline2 print_inv) invs

let print_to_file invs =
  let print_inv fmt (_,t) = Pretty.print_term fmt t in
  let fmt = Format.formatter_of_out_channel (open_out "inferred_invs.out") in
  Format.fprintf fmt "Generated invariants:@\n%a@."
    (Pp.print_list Pp.newline2 print_inv) invs

let inv_terms = ref []

let save_invs invs =
  inv_terms := List.map snd invs

let () =
  Infer_loop.register_hook (fun i ->
      print_to_std i; print_to_file i; save_invs i)

Finally the code for closing the modules, printing it to the standard output, typing it, and so on is exactly the same as in the previous section, thus we omit it in here. Note that in practice, the invariants are only inferred when invoking Typing.type_mlw_file.

4.9.5. Typed declaration

The examples of this section are available in the file examples/use_api/mlw_expr.ml of the distribution.

The first step to build an environment as already illustrated in Section 4.3.

open Why3
let config : Whyconf.config = Whyconf.init_config None
let main : Whyconf.main = Whyconf.get_main config
let libdir = Whyconf.libdir main
let datadir = Whyconf.datadir main
let env : Env.env = Env.create_env (Whyconf.loadpath main)

To write our programs, we need to import some other modules from the standard library integers and references. The only subtleties is to get logic functions from the logical part of the modules mod_theory.Theory.th_export and the program functions from mod_export.

let int_module : Pmodule.pmodule =
  Pmodule.read_module env ["int"] "Int"

let ge_int : Term.lsymbol =
  Theory.ns_find_ls int_module.Pmodule.mod_theory.Theory.th_export
    [Ident.op_infix ">="]

let ref_module : Pmodule.pmodule =
  Pmodule.read_module env ["ref"] "Ref"

let ref_type : Ity.itysymbol =
  Pmodule.ns_find_its ref_module.Pmodule.mod_export ["ref"]

(* the "ref" function *)
let ref_fun : Expr.rsymbol =
  Pmodule.ns_find_rs ref_module.Pmodule.mod_export ["ref"]

(* the "!" function *)
let get_fun : Expr.rsymbol =
  Pmodule.ns_find_rs ref_module.Pmodule.mod_export [Ident.op_prefix "!"]

We want now to build a program equivalent to the following code in concrete Why3 syntax.

     let f2 () : int
        requires { true }
        ensures { result >= 0 }
      = let x = ref 42 in !x

The OCaml code that programmatically build this Why3 function is as follows.

let d2 =
  let id = Ident.id_fresh "f" in
  let post =
    let result =
      Term.create_vsymbol (Ident.id_fresh "result") Ty.ty_int
    in
    let post = Term.ps_app ge_int [Term.t_var result; Term.t_nat_const 0] in
    Ity.create_post result post
  in
  let body =
    (* building expression "ref 42" *)
    let e =
      let c0 = Expr.e_const (Constant.int_const_of_int 42) Ity.ity_int in
      let refzero_type = Ity.ity_app ref_type [Ity.ity_int] [] in
      Expr.e_app ref_fun [c0] [] refzero_type
    in
    (* building the first part of the let x = ref 42 *)
    let id_x = Ident.id_fresh "x" in
    let letdef, var_x = Expr.let_var id_x e in
    (* building expression "!x" *)
    let bang_x = Expr.e_app get_fun [Expr.e_var var_x] [] Ity.ity_int in
    (* the complete body *)
    Expr.e_let letdef bang_x
  in
  let arg_unit =
    let unit = Ident.id_fresh "unit" in
    Ity.create_pvsymbol unit Ity.ity_unit
  in
  let def,_rs = Expr.let_sym id
      (Expr.c_fun [arg_unit] [] [post] Ity.Mxs.empty Ity.Mpv.empty body) in
  Pdecl.create_let_decl def

Having declared all the programs we wanted to write, we can now create the module and generate the VCs.

let mod2 =
  let uc : Pmodule.pmodule_uc =
    Pmodule.create_module env (Ident.id_fresh "MyModule")
  in
  let uc = Pmodule.use_export uc int_module in
  let uc = Pmodule.use_export uc ref_module in
  let uc = Pmodule.add_pdecl ~vc:true uc d2 in
  Pmodule.close_module uc

We can then construct the proofs tasks for our module, and then try to call the Alt-Ergo prover. The rest of that code is using OCaml functions that were already introduced before.

let my_tasks : Task.task list =
  Task.split_theory mod2.Pmodule.mod_theory None None

open Format

let () =
  printf "Tasks are:@.";
  let _ =
    List.fold_left
      (fun i t -> printf "Task %d: %a@." i Pretty.print_task t; i+1)
      1 my_tasks
  in ()

let provers : Whyconf.config_prover Whyconf.Mprover.t =
  Whyconf.get_provers config

let alt_ergo : Whyconf.config_prover =
  let fp = Whyconf.parse_filter_prover "Alt-Ergo" in
  (** all provers that have the name "Alt-Ergo" *)
  let provers = Whyconf.filter_provers config fp in
  if Whyconf.Mprover.is_empty provers then begin
    eprintf "Prover Alt-Ergo not installed or not configured@.";
    exit 1
  end else
    snd (Whyconf.Mprover.max_binding provers)

let alt_ergo_driver : Driver.driver =
  try
    Whyconf.load_driver main env alt_ergo
  with e ->
    eprintf "Failed to load driver for alt-ergo: %a@."
      Exn_printer.exn_printer e;
    exit 1

let () =
  let _ =
    List.fold_left
      (fun i t ->
       let r =
         Call_provers.wait_on_call
           (Driver.prove_task
              ~limit:Call_provers.empty_limit
              ~libdir
              ~datadir
              ~command:alt_ergo.Whyconf.command
              alt_ergo_driver
              t)
       in
       printf "@[On task %d, alt-ergo answers %a@."
              i (Call_provers.print_prover_result ?json:None) r;
       i+1
      )
      1 my_tasks
  in ()

4.10. Generating counterexamples

That feature is presented in details in Section 6.3.7, which should be read first. The counterexamples can also be generated using the API. The following explains how to change the source code (mainly adding attributes) in order to display counterexamples and how to parse the result given by Why3. To illustrate this, we will adapt the examples from Section 4.1 to display counterexamples.

4.10.1. Attributes and locations on identifiers

For variables to be used for counterexamples they need to contain an attribute called model_trace and a location. This attribute states the name the user wants the variable to be named in the output of the counterexamples pass. Usually, people put a reference to their program AST node in this attribute; this helps them to parse and display the results given by Why3. The locations are also necessary as every counterexamples values with no location will not be displayed. For example, an assignment of the source language such as the following will probably trigger the creation of an identifier (for the left value) in a user subsequent tasks:

x := !y + 1

This means that the ident generated for x will hold both a model_trace and a location.

The example becomes the following:

let make_attribute (name: string) : Ident.attribute =
  Ident.create_attribute ("model_trace:" ^ name)
let prop_var_A : Term.lsymbol =
  (* [user_position file line left_col right_col] *)
  let loc = Loc.user_position "myfile.my_ext" 28 0 0  in
  let attrs = Ident.Sattr.singleton (make_attribute "my_A") in
  Term.create_psymbol (Ident.id_fresh ~attrs ~loc "A") []

In the above, we defined a proposition identifier with a location and a model_trace.

4.10.2. Attributes in formulas

Now that variables are tagged, we can define formulas. To define a goal formula for counterexamples, we need to tag it with the [@vc:annotation] attribute. This attribute is automatically added when using the VC generation of Why3, but on a user-built task, this needs to be added. We also need to add a location for this goal. The following is obtained for the simple formula linking A and B:

let atom_A : Term.term = Term.ps_app prop_var_A []
let atom_B : Term.term = Term.ps_app prop_var_B []
(* Voluntarily wrong verification condition *)
let fmla2 : Term.term =
  Term.t_implies atom_A (Term.t_and atom_A atom_B)
(* We add a location and attribute to indicate the start of a goal *)
let fmla2 : Term.term =
  let loc = Loc.user_position "myfile.my_ext" 42 28 91  in
  let attrs = Ident.Sattr.singleton Ity.annot_attr in
  (* Note that this remove any existing attribute/locations on fmla2 *)
  Term.t_attr_set ~loc attrs fmla2

Note: the transformations used for counterexamples will create new variables for each variable occurring inside the formula tagged by vc:annotation. These variables are duplicates located at the VC line. They allow giving all counterexample values located at that VC line.

4.10.3. Counterexamples output formats

Several output formats are available for counterexamples. For users who want to pretty-print their counterexamples values, we recommend to use the JSON output as follows:

(* prints CVC4 answer *)
let () = printf "@[On task 1, CVC4,1.7 answers %a@."
    (Call_provers.print_prover_result ?json:None) result1

let () = printf "Model is %t@."
    (fun fmt ->
       match Check_ce.select_model_last_non_empty
                result1.Call_provers.pr_models with
       | Some m -> Json_base.print_json fmt (Model_parser.json_model m)
       | None -> fprintf fmt "unavailable")

4.10.4. Checking counterexamples

Counterexamples can be checked using the API, too. Here is an example for the selecting a counterexample from the result pr of proving a sub-goal of pmodule pm:

let () =
  let rac = Pinterp.mk_rac ~ignore_incomplete:false
      (Rac.Why.mk_check_term_lit config env ~why_prover:"alt-ergo" ()) in
  let model, clsf = Opt.get_exn (Failure "No good model found")
      (Check_ce.select_model ~check_ce:true rac env pm models) in
  printf "%a@." (Check_ce.print_model_classification
                   ~check_ce:true ?verb_lvl:None ?json:None) (model, clsf)

The API also permits running only one of the two RAC executions (giant-step, in this case):

let () =
  let model = Opt.get_exn (Failure "No non-empty model")
      (Check_ce.select_model_last_non_empty models) in
  let loc = Opt.get_exn (Failure "No model term location")
      (Model_parser.get_model_term_loc model) in
  let rs = Opt.get_exn (Failure "No procedure symbol found")
      (Check_ce.find_rs pm loc) in
  let rac = Pinterp.mk_rac ~ignore_incomplete:false
      (Rac.Why.mk_check_term_lit config env ~why_prover:"alt-ergo" ()) in
  let oracle = Check_ce.oracle_of_model pm model in
  let env = Pinterp.mk_empty_env env pm in
  let ctx = Pinterp.mk_ctx env ~do_rac:true ~rac ~giant_steps:true ~oracle () in
  let res = Check_ce.rac_execute ctx rs in
  printf "%a@." (Check_ce.print_rac_result ?verb_lvl:None) res