Please find in attachment a more complete example file mlw.ml that
includes the construction of the small program
let f (a:array int)
requires { a.length >= 1 }
ensures { a[0] = 42 }
= a[0] <- 42
Hope this helps,
Le 02/05/2018 à 22:20, Gian Pietro Farina a écrit :
Hi, and thanks for the reply.
Sorry if my questions sound naive.
I've now read that part of the manual and I can now load the module
Array.
But I have some difficulties, for instance:
I am trying to build formulas and terms such as a[0]>1 /\ a[1]>2 ==>
a[0]+a[1]>3 .
I fail though in even understanding how to build a term of type
"array". While for "first order" terms like integers or naturals it
works ok.
I would also eventually like to quantify existentially over a its indices.
I m trying to read this http://why3.lri.fr/stdlib-0.81/array.mlw.html
but I don't understand how to do things in ocaml.
Cheers,
GP
On Wed, May 2, 2018 at 5:37 AM, Claude Marché <claude.mar...@inria.fr
<mailto:claude.mar...@inria.fr>> wrote:
Hello,
I guess you already read the chapter 4 of the manual
(http://why3.lri.fr/doc/api.html#sec30
<http://why3.lri.fr/doc/api.html#sec30>). The importation of
modules and the manipulation of programs is not documented yet,
but you can find some examples of use in the directory
examples/use_api of the distribution: files mlw.ml <http://mlw.ml>
and mlw_tree.ml <http://mlw_tree.ml>.
Indeed there is a subtle distinction between modules and theories.
Arrays are in a module and not in a theory. Specifically, the
importation of a module is done using Mlw_module.read_module. see
http://why3.lri.fr/api/Mlw_module.html
<http://why3.lri.fr/api/Mlw_module.html>
Do not hesitate to request for more help on any specific use of
the API
- Claude
Le 01/05/2018 à 23:55, Gian Pietro Farina a écrit :
Hello,
I would like to use the Ocaml api of why3 in my project where
I need to send to the smt solvers
queries in the theory of arrays. How do I load a theory in my
project?
Best regards,
Gian Pietro
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
<mailto:Why3-club@lists.gforge.inria.fr>
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
<https://lists.gforge.inria.fr/mailman/listinfo/why3-club>
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
<mailto:Why3-club@lists.gforge.inria.fr>
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
<https://lists.gforge.inria.fr/mailman/listinfo/why3-club>
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2018 -- Inria - CNRS - Paris-Sud University *)
(* *)
(* This software is distributed under the terms of the GNU Lesser *)
(* General Public License version 2.1, with the special exception *)
(* on linking described in file LICENSE. *)
(* *)
(********************************************************************)
(*******************
This file builds some MLW modules using the API
******************)
(* opening the Why3 library *)
open Why3
(* 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
(* builds the environment from the [loadpath] *)
let env : Env.env = Env.create_env (Whyconf.loadpath main)
let int_theory : Theory.theory =
Env.read_theory env ["int"] "Int"
let mul_int : Term.lsymbol =
Theory.ns_find_ls int_theory.Theory.th_export ["infix *"]
let ge_int : Term.lsymbol =
Theory.ns_find_ls int_theory.Theory.th_export ["infix >="]
let unit_type = Ty.ty_tuple []
(* start a module named "Program" *)
let m = Mlw_module.create_module env (Ident.id_fresh "Program")
(* declaration of
let f (_dummy:unit) : unit
requires { true }
ensures { true }
=
assert { 6*7 = 42 }
*)
let d =
let args =
[Mlw_ty.create_pvsymbol (Ident.id_fresh "_dummy") Mlw_ty.ity_unit]
in
let result = Term.create_vsymbol (Ident.id_fresh "result") unit_type in
let spec = {
Mlw_ty.c_pre = Term.t_true;
c_post = Mlw_ty.create_post result Term.t_true;
c_xpost = Mlw_ty.Mexn.empty;
c_effect = Mlw_ty.eff_empty;
c_variant = [];
c_letrec = 0;
}
in
let body =
let c6 = Term.t_nat_const 6 in
let c7 = Term.t_nat_const 7 in
let c42 = Term.t_nat_const 42 in
let p =
Term.t_equ (Term.t_app_infer mul_int [c6;c7]) c42
in
Mlw_expr.e_assert Mlw_expr.Aassert p
in
let lambda = {
Mlw_expr.l_args = args;
l_expr = body;
l_spec = spec;
}
in
let def = Mlw_expr.create_fun_defn (Ident.id_fresh "f") lambda in
Mlw_decl.create_rec_decl [def]
(*
declaration of
let f (_dummy:unit) : unit
requires { true }
ensures { result = 0 }
=
let x = ref 0 in
!x
*)
(* import the ref.Ref module *)
let ref_module : Mlw_module.modul =
Mlw_module.read_module env ["ref"] "Ref"
let ref_type : Mlw_ty.T.itysymbol =
Mlw_module.ns_find_its ref_module.Mlw_module.mod_export ["ref"]
(* the "ref" function *)
let ref_fun : Mlw_expr.psymbol =
Mlw_module.ns_find_ps ref_module.Mlw_module.mod_export ["ref"]
(* the "!" function *)
let get_fun : Mlw_expr.psymbol =
Mlw_module.ns_find_ps ref_module.Mlw_module.mod_export ["prefix !"]
let d2 =
let args =
[Mlw_ty.create_pvsymbol (Ident.id_fresh "_dummy") Mlw_ty.ity_unit]
in
let result = Term.create_vsymbol (Ident.id_fresh "result") Ty.ty_int in
let spec = {
Mlw_ty.c_pre = Term.t_true;
c_post = Mlw_ty.create_post result Term.t_true;
c_xpost = Mlw_ty.Mexn.empty;
c_effect = Mlw_ty.eff_empty;
c_variant = [];
c_letrec = 0;
}
in
let body =
(* building expression "ref 0" *)
let e =
(* recall that "ref" has polymorphic type "(v:'a) -> ref 'a".
We need to build an instance of it *)
(* we build "ref int" with a *fresh* region *)
let ity = Mlw_ty.ity_app_fresh ref_type [Mlw_ty.ity_int] in
(* e1 : the appropriate instance of "ref" *)
let e1 = Mlw_expr.e_arrow ref_fun [Mlw_ty.ity_int] ity in
(* we apply it to 0 *)
let c0 = Mlw_expr.e_const (Number.const_of_int 0) Mlw_ty.ity_int in
Mlw_expr.e_app e1 [c0]
in
(* building the first part of the let x = ref 0 *)
let letdef, var_x = Mlw_expr.create_let_pv_defn (Ident.id_fresh "x") e in
(* building expression "!x" *)
let bang_x =
(* recall that "!" as type "ref 'a -> 'a" *)
let e1 = Mlw_expr.e_arrow get_fun [var_x.Mlw_ty.pv_ity] Mlw_ty.ity_int in
Mlw_expr.e_app e1 [Mlw_expr.e_value var_x]
in
(* the complete body *)
Mlw_expr.e_let letdef bang_x
in
let lambda = {
Mlw_expr.l_args = args;
l_expr = body;
l_spec = spec;
}
in
let def = Mlw_expr.create_fun_defn (Ident.id_fresh "f") lambda in
Mlw_decl.create_rec_decl [def]
(* let f (a:array int)
requires { a.length >= 1 }
ensures { a[0] = 42 }
= a[0] <- 42
*)
let array_module : Mlw_module.modul =
Mlw_module.read_module env ["array"] "Array"
let array_theory : Theory.theory =
array_module.Mlw_module.mod_theory
let array_type : Mlw_ty.T.itysymbol =
Mlw_module.ns_find_its array_module.Mlw_module.mod_export ["array"]
let ls_length : Term.lsymbol =
Theory.ns_find_ls array_theory.Theory.th_export ["length"]
(* the "[]" logic symbol *)
let ls_select : Term.lsymbol =
Theory.ns_find_ls array_theory.Theory.th_export ["mixfix []"]
(* the "[]<-" program symbol *)
let store_fun : Mlw_expr.psymbol =
Mlw_module.ns_find_ps array_module.Mlw_module.mod_export ["mixfix []<-"]
let d3 =
try
let ity = Mlw_ty.ity_app_fresh array_type [Mlw_ty.ity_int] in
let a = Mlw_ty.create_pvsymbol (Ident.id_fresh "a") ity in
let result = Term.create_vsymbol (Ident.id_fresh "result") (Ty.ty_tuple []) in
let pre =
Term.ps_app ge_int
[Term.t_app_infer ls_length [Term.t_var
a.Mlw_ty.pv_vs];Term.t_nat_const 1]
in
let post =
Term.ps_app Term.ps_equ
[Term.t_app_infer ls_select [Term.t_var
a.Mlw_ty.pv_vs;Term.t_nat_const 0 ] ;
Term.t_nat_const 42 ]
in
let spec = {
Mlw_ty.c_pre = pre;
c_post = Mlw_ty.create_post result post;
c_xpost = Mlw_ty.Mexn.empty;
c_effect = Mlw_ty.eff_empty;
c_variant = [];
c_letrec = 0;
}
in
(* building expression "a[0]<-42" *)
let e1 = Mlw_expr.e_arrow store_fun [ity;Mlw_ty.ity_int;Mlw_ty.ity_int]
Mlw_ty.ity_unit in
let body =
Mlw_expr.e_app e1
[Mlw_expr.e_value a;
Mlw_expr.e_const (Number.const_of_int 0) Mlw_ty.ity_int;
Mlw_expr.e_const (Number.const_of_int 42) Mlw_ty.ity_int]
in
let lambda = {
Mlw_expr.l_args = [a];
l_expr = body;
l_spec = spec;
}
in
let def = Mlw_expr.create_fun_defn (Ident.id_fresh "f") lambda in
Mlw_decl.create_rec_decl [def]
with e -> Format.eprintf "Error: %a@." Exn_printer.exn_printer e;
exit 1
(* TODO: continue *)
(*
let () = Printexc.record_backtrace true
let () =
try
let _buggy : Mlw_module.module_uc = Mlw_module.add_pdecl ~wp:true m d in
()
with Not_found ->
Printexc.print_backtrace stderr;
flush stderr
*)
(*
Local Variables:
compile-command: "ocaml -I ../../lib/why3 unix.cma nums.cma str.cma dynlink.cma
../../lib/why3/why3.cma mlw.ml"
End:
*)
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
