Commit 8e182798 authored by MARCHE Claude's avatar MARCHE Claude

doc: API tutorial

parent cf169474
......@@ -229,6 +229,8 @@ install_no_local::
mkdir -p $(DATADIR)/why3/theories
mkdir -p $(DATADIR)/why3/theories/transform
mkdir -p $(DATADIR)/why3/drivers
mkdir -p $(OCAMLLIB)/why3
cp -f src/why.cmi src/why.cma src/why.cmxa $(OCAMLLIB)/why3
cp -f theories/*.why $(DATADIR)/why3/theories
cp -f theories/transform/*.why $(DATADIR)/why3/theories/transform
cp -f drivers/*.drv $(DATADIR)/why3/drivers
......
\chapter{The Why3 Application Programming Interface}
\label{chap:api}
\section{Building Terms and Formulas}
This chapter is a tutorial for the users who wants 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.
\section{Building Theories}
We naturally assume here a fair knowledge of the OCaml language.
\section{Building Propositional Formulas}
The first step is to know how to build propositional formulas. The
module \texttt{Term} gives a few functions for building these. Here is
a piece of OCaml code for building the formula $true \lor false$.
\begin{verbatim}
(* opening the Why3 library *)
open Why
(* a ground propositional goal: true or false *)
let fmla_true : Term.fmla = Term.f_true
let fmla_false : Term.fmla = Term.f_false
let fmla1 : Term.fmla = Term.f_or fmla_true fmla_false
\end{verbatim}
As one can guess, the type \texttt{fmla} is the type of formulas in
the library.
Such a formula can be printed using the module \texttt{Pretty}
providing pretty-printers.
\begin{verbatim}
(* printing the formula *)
open Format
let () = printf "@[formula 1 is:@ %a@]@." Pretty.print_fmla fmla1
\end{verbatim}
Assuming the lines above are written in a file \texttt{f.ml}, it can
be compiled using
\begin{verbatim}
ocamlc str.cma unix.cma nums.cma dynlink.cma \
-I +ocamlgraph -I +why3 graph.cma why.cma f.ml -o f
\end{verbatim}
Running the generated executable \texttt{f} results in the following output.
\begin{verbatim}
formula 1 is: true or false
\end{verbatim}
Let's now build a formula with propositional variables: $A \land B
\rightarrow A$. Propositional variables must be declared first before
using them in formulas. This is done as follows.
\begin{verbatim}
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") []
\end{verbatim}
The type \texttt{lsymbol} is the type of logic symbols. 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.
\begin{verbatim}
let atom_A : Term.fmla = Term.f_app prop_var_A []
let atom_B : Term.fmla = Term.f_app prop_var_B []
let fmla2 : Term.fmla =
Term.f_implies (Term.f_and atom_A atom_B) atom_A
let () = printf "@[formula 2 is:@ %a@]@." Pretty.print_fmla fmla2
\end{verbatim}
As expected, the output is as follows.
\begin{verbatim}
formula 2 is: A and B -> A
\end{verbatim}
\section{Buildings Tasks and calling External Provers}
\section{Building Terms and First-Order Formulas}
An important feature of the functions for building terms and formulas
is that they statically guarantee that only well-typed terms can be
constructed.
\section{Building Theories}
\section{Applying transformations}
%%% Local Variables:
......
......@@ -10,8 +10,9 @@ Compilation of Why3 must start with a configuration phase which is run as
This analyzes you current configuration and check if requirements hold.
Compilation requires:
\begin{itemize}
\item The Objective Caml compiler, version 3.10 or higher. It is available
as a binary package for most Unix distributions. For debian-based Linux distributions, you can install the packages
\item The Objective Caml compiler, version 3.10 or higher. It is
available as a binary package for most Unix distributions. For
debian-based Linux distributions, you can install the packages
\begin{verbatim}
ocaml ocaml-native-compilers
\end{verbatim}
......
......@@ -11,6 +11,8 @@
\begin{document}
\sloppy
\hbadness=1100
\thispagestyle{empty}
......
(***************
This file builds some goals using the API and calls
the alt-ergo prover to check them
(*
*)
******************)
(* opening the Why3 library *)
open Why
(* a ground propositional goal: true or false *)
let fmla_true : Term.fmla = Term.f_true
let fmla_false : Term.fmla = Term.f_false
let fmla1 : Term.fmla = Term.f_or fmla_true fmla_false
(* printing it *)
open Format
let () = printf "@[formula 1 is:@ %a@]@." Pretty.print_fmla fmla1
(***************
This file builds some goals using the API and calls
the alt-ergo prover to check them
(* a propositional goal: A and B implies A *)
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") []
let atom_A : Term.fmla = Term.f_app prop_var_A []
let atom_B : Term.fmla = Term.f_app prop_var_B []
let fmla2 : Term.fmla = Term.f_implies (Term.f_and atom_A atom_B) atom_A
let () = printf "@[formula 2 is:@ %a@]@." Pretty.print_fmla fmla2
******************)
(* First, we need to access the Why configuration *)
(* To build tasks and call prover, we need to access the Why configuration *)
(* reads the config file *)
let config = Whyconf.read_config None
(* the [main] section of the config file *)
let main = Whyconf.get_main config
(* builds the environment from the [loadpath] *)
let env = Env.create_env (Lexer.retrieve (Whyconf.loadpath main))
(* the [provers] of the config file *)
let provers = Whyconf.get_provers config
(* the [prover alt-ergo] section of the config file *)
let alt_ergo =
try
Util.Mstr.find "alt-ergo" provers
......@@ -29,47 +50,26 @@ let alt_ergo =
eprintf "Prover alt-ergo not installed or not configured@.";
exit 0
(* loading the Alt-Ergo driver *)
let alt_ergo_driver = Driver.load_driver env alt_ergo.Whyconf.driver
(*
a ground propositional goal: True or False
*)
let fmla_true = Term.f_true
let fmla_false = Term.f_false
let fmla1 = Term.f_or fmla_true fmla_false
let () = printf "@[formula 1 created:@ %a@]@." Pretty.print_fmla fmla1
let task1 = None
(* building the task for formula 1 alone *)
let task1 = None (* empty task *)
let goal_id1 = Decl.create_prsymbol (Ident.id_fresh "goal1")
let task1 = Task.add_prop_decl task1 Decl.Pgoal goal_id1 fmla1
let () = printf "@[task 1 created:@\n%a@]@." Pretty.print_task task1
(* printing the task *)
let () = printf "@[task 1 is:@\n%a@]@." Pretty.print_task task1
(* call Alt-Ergo *)
let result1 =
Driver.prove_task ~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
(*
a propositional goal: A and B implies B
*)
let prop_var_A = Term.create_psymbol (Ident.id_fresh "A") []
let prop_var_B = Term.create_psymbol (Ident.id_fresh "B") []
let fmla_A = Term.f_app prop_var_A []
let fmla_B = Term.f_app prop_var_B []
let fmla2 = Term.f_implies (Term.f_and fmla_A fmla_B) fmla_B
let () = printf "@[formula 2 created:@ %a@]@." Pretty.print_fmla fmla2
let task2 = None
let task2 = Task.add_logic_decl task2 [prop_var_A, None]
let task2 = Task.add_logic_decl task2 [prop_var_B, None]
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment