Previous Up Next

Chapter 3  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 this URL.

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

3.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 truefalse.

(* 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: ABA. 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.

3.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 truefalse 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

3.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 why3config command line tool or the Detect Provers menu of the graphical IDE. The following API calls allow to access the content of this configuration file.

(* reads the config file *) let config : Whyconf.config = Whyconf.read_config None (* the [main] section of the config file *) let main : Whyconf.main = Whyconf.get_main config (* 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 0 end else snd (Whyconf.Mprover.max_binding provers)

We could also get a specific version with :

(* Specific version 2.0.0 of Alt-Ergo in the config file *) let alt_ergo_2_0_0 : Whyconf.config_prover = let fp = Whyconf.parse_filter_prover "Alt-Ergo,2.0.0" in let provers = Whyconf.filter_provers config fp in if Whyconf.Mprover.is_empty provers then begin eprintf "Prover Alt-Ergo 2.0.0 not installed or not configured@."; exit 0 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.Whyconf.driver [] 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 ~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 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_model : model; }

with in particular the fields:

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:

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 ~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

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

3.5  Building Quantified Formulas

To illustrate how to build quantified formulas, let us consider the formula ∀ x:int. x*x ≥ 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*x ≥ 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

3.6  Building Theories

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

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 decl_goal1 : Decl.decl = Decl.create_prop_decl Decl.Pgoal goal_id1 fmla1 let my_theory : Theory.theory_uc = Theory.add_decl my_theory decl_goal1

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.

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

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

3.9  ML Programs

The simplest way to build WhyML programs from OCaml is to build untyped syntax trees for such programs, and then call the Why3 typing procedure to build typed declarations.

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 3.3, and open the OCaml module Ptree which contains most of the OCaml functions we need in this section.

open Why3 let config : Whyconf.config = Whyconf.read_config None let main : Whyconf.main = Whyconf.get_main config let env : Env.env = Env.create_env (Whyconf.loadpath main) open Ptree

To contain all the example programs we are going to build we need a module. We start the creation of that module using the following declarations, that first introduces a pseudo “file” to hold the module, then the module itself called Program.

let () = Typing.open_file env [] (* empty pathname *) let mk_ident s = { id_str = s; id_ats = []; id_loc = Loc.dummy_position } let () = Typing.open_module (mk_ident "Program")

Notice the use of a first simple helper function mk_ident to build an identifier without any attributes nor any location.

To write our programs, we need to import some other modules from the standard library. The following introduces two helper functions for building qualified identifiers and importing modules, and finally imports int.Int.

let mk_qid l = let rec aux l = match l with | [] -> assert false | [x] -> Qident(mk_ident x) | x::r -> Qdot(aux r,mk_ident x) in aux (List.rev l) let use_import (f, m) = let m = mk_ident m in let loc = Loc.dummy_position in Typing.open_scope loc m; Typing.add_decl loc (Ptree.Duse (Qdot (Qident (mk_ident f), m))); Typing.close_scope loc ~import:true let use_int_Int = use_import ("int","Int")

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

let f1 (x:int) : unit requires { x=6 } ensures { result=42 } = x*7

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

let eq_symb = mk_qid [Ident.op_infix "="] let int_type_id = mk_qid ["int"] let int_type = PTtyapp(int_type_id,[]) let mul_int = mk_qid ["Int";Ident.op_infix "*"] let d1 : decl = let id_x = mk_ident "x" in let pre = mk_tapp eq_symb [mk_var id_x; mk_tconst "6"] in let result = mk_ident "result" in let post = mk_tapp eq_symb [mk_var result; mk_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 = mk_eapp mul_int [mk_evar id_x; mk_econst "7"] in let f1 = Efun(param1 id_x int_type, None, Ity.MaskVisible, spec, body) in Dlet(mk_ident "f1",false,Expr.RKnone, mk_expr f1) let () = try Typing.add_decl Loc.dummy_position d1 with e -> Format.printf "Exception raised during typing of d:@ %a@." Exn_printer.exn_printer e

This code makes uses of helper functions that are given in Figure 3.1.


let mk_expr e = { expr_desc = e; expr_loc = Loc.dummy_position } let mk_term t = { term_desc = t; term_loc = Loc.dummy_position } let mk_pat p = { pat_desc = p; pat_loc = Loc.dummy_position } let pat_var id = mk_pat (Pvar id) let mk_var id = mk_term (Tident (Qident id)) let param0 = [Loc.dummy_position, None, false, Some (PTtuple [])] let param1 id ty = [Loc.dummy_position, Some id, false, Some ty] let mk_tconst s = mk_term (Tconst Number.(ConstInt { ic_negative = false ; ic_abs = int_literal_dec s })) let mk_econst s = mk_expr (Econst Number.(ConstInt { ic_negative = false ; ic_abs = int_literal_dec s })) let mk_tapp f l = mk_term (Tidapp(f,l)) let mk_eapp f l = mk_expr (Eidapp(f,l)) let mk_evar x = mk_expr(Eident(Qident x))
Figure 3.1: Helper functions for building WhyML programs

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

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 = mk_qid ["Int";Ident.op_infix ">="] let use_ref_Ref = use_import ("ref","Ref") let d2 = let result = mk_ident "result" in let post = mk_term(Tidapp(ge_int,[mk_var result;mk_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 = mk_eapp (mk_qid ["Ref";"ref"]) [mk_econst "42"] in let id_x = mk_ident "x" in let e2 = mk_eapp (mk_qid ["Ref";Ident.op_prefix "!"]) [mk_evar id_x] in mk_expr(Elet(id_x,false,Expr.RKlocal,e1,e2)) in let f = Efun(param0,None,Ity.MaskVisible,spec,body) in Dlet(mk_ident "f2",false,Expr.RKnone, mk_expr f) let () = try Typing.add_decl Loc.dummy_position d2 with e -> Format.printf "Exception raised during typing of d2:@ %a@." Exn_printer.exn_printer e

The next example makes use of arrays.

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

The corresponding OCaml code is as follows

let () = use_import ("array","Array") let array_int_type = PTtyapp(mk_qid ["Array";"array"],[int_type]) let length = mk_qid ["Array";"length"] let array_get = mk_qid ["Array"; Ident.op_get ""] let array_set = mk_qid ["Array"; Ident.op_set ""] let d3 = let id_a = mk_ident "a" in let pre = mk_tapp ge_int [mk_tapp length [mk_var id_a]; mk_tconst "1"] in let post = mk_tapp eq_symb [mk_tapp array_get [mk_var id_a; mk_tconst "0"]; mk_tconst "42"] in let spec = { sp_pre = [pre]; sp_post = [Loc.dummy_position,[mk_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 = mk_eapp array_set [mk_evar id_a; mk_econst "0"; mk_econst "42"] in let f = Efun(param1 id_a array_int_type, None,Ity.MaskVisible,spec,body) in Dlet(mk_ident "f3", false, Expr.RKnone, mk_expr f) let () = try Typing.add_decl Loc.dummy_position d3 with e -> Format.printf "Exception raised during typing of d3:@ %a@." Exn_printer.exn_printer e

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, under the form of a map of module names to modules.

let () = Typing.close_module Loc.dummy_position let mods : Pmodule.pmodule Wstdlib.Mstr.t = Typing.close_file ()

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 = 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 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 0 end else snd (Whyconf.Mprover.max_binding provers) let alt_ergo_driver : Driver.driver = try Whyconf.load_driver main env alt_ergo.Whyconf.driver [] 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 ~command:alt_ergo.Whyconf.command alt_ergo_driver t) in printf "@[On task %d, alt-ergo answers %a@." i Call_provers.print_prover_result r; i+1 ) 1 my_tasks in ()

Previous Up Next