api.tex 15.1 KB
 MARCHE Claude committed Jul 02, 2011 1 \chapter{The \why API}  Jean-Christophe Filliatre committed Aug 21, 2012 2 \label{chap:api}\index{API}  Guillaume Melquiond committed Oct 02, 2017 3 %HEVEA\cutname{api.html}  MARCHE Claude committed Sep 06, 2010 4   Andrei Paskevich committed Dec 20, 2010 5 This chapter is a tutorial for the users who want to link their own  MARCHE Claude committed Jul 02, 2011 6 OCaml code with the \why library. We progressively introduce the way  MARCHE Claude committed Dec 08, 2010 7 8 one can use the library to build terms, formulas, theories, proof tasks, call external provers on tasks, and apply transformations on  MARCHE Claude committed Mar 17, 2017 9 10 11 tasks. The complete documentation for API calls is given\begin{latexonly} at URL~\urlapi{}.\end{latexonly} %HEVEA at this \ahref{\urlapi}{URL}.  MARCHE Claude committed Dec 08, 2010 12   MARCHE Claude committed Dec 16, 2010 13 We assume the reader has a fair knowledge of the OCaml  MARCHE Claude committed Jul 02, 2011 14 language. Notice that the \why library must be installed, see  MARCHE Claude committed Jul 02, 2011 15 Section~\ref{sec:installlib}. The OCaml code given below is available in  MARCHE Claude committed Oct 10, 2013 16 17 the source distribution in directory \verb|examples/use_api/| together with a few other examples.  MARCHE Claude committed Sep 06, 2010 18   MARCHE Claude committed Apr 09, 2018 19 \lstset{language={[Objective]Caml}}  MARCHE Claude committed Dec 08, 2010 20 21 22 23 24  \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  MARCHE Claude committed Oct 10, 2013 25 26 a piece of OCaml code for building the formula $\mathit{true} \lor \mathit{false}$.  Guillaume Melquiond committed Jun 05, 2018 27 \lstinputlisting{generated/logic__opening.ml}  Andrei Paskevich committed Jun 18, 2011 28 The library uses the common type \texttt{term} both for terms  Guillaume Melquiond committed Oct 11, 2012 29 30 (\ie expressions that produce a value of some particular type) and formulas (\ie boolean-valued expressions).  Andrei Paskevich committed Jun 18, 2011 31 32 33 34 % To distinguish terms from formulas, one can look at the % \texttt{t_ty} field of the \texttt{term} record: in formulas, % this field has the value \texttt{None}, and in terms, % \texttt{Some t}, where \texttt{t} is of type \texttt{Ty.ty}.  MARCHE Claude committed Dec 08, 2010 35 36 37  Such a formula can be printed using the module \texttt{Pretty} providing pretty-printers.  Guillaume Melquiond committed Jun 05, 2018 38 \lstinputlisting{generated/logic__printformula.ml}  MARCHE Claude committed Dec 08, 2010 39 40 41 42  Assuming the lines above are written in a file \texttt{f.ml}, it can be compiled using \begin{verbatim}  MARCHE Claude committed Apr 11, 2018 43 ocamlfind ocamlc -package why3 -linkpkg f.ml -o f  MARCHE Claude committed Dec 08, 2010 44 45 46 \end{verbatim} Running the generated executable \texttt{f} results in the following output. \begin{verbatim}  Andrei Paskevich committed Jun 30, 2011 47 formula 1 is: true \/ false  MARCHE Claude committed Dec 08, 2010 48 49 \end{verbatim}  Guillaume Melquiond committed Feb 01, 2013 50 Let us now build a formula with propositional variables: $A \land B  MARCHE Claude committed Dec 08, 2010 51 52 \rightarrow A$. Propositional variables must be declared first before using them in formulas. This is done as follows.  Guillaume Melquiond committed Jun 05, 2018 53 \lstinputlisting{generated/logic__declarepropvars.ml}  Andrei Paskevich committed Jun 18, 2011 54 55 56 57 The type \texttt{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.  Guillaume Melquiond committed Jun 05, 2018 58 \lstinputlisting{generated/logic__declarepropatoms.ml}  MARCHE Claude committed Dec 08, 2010 59 60 61  As expected, the output is as follows. \begin{verbatim}  Andrei Paskevich committed Jun 30, 2011 62 formula 2 is: A /\ B -> A  MARCHE Claude committed Dec 08, 2010 63 \end{verbatim}  Andrei Paskevich committed Jul 02, 2011 64 65 66 67 Notice that the concrete syntax of \why 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.  MARCHE Claude committed Dec 08, 2010 68   MARCHE Claude committed Dec 17, 2010 69 \section{Building Tasks}  MARCHE Claude committed Dec 08, 2010 70   Guillaume Melquiond committed Feb 01, 2013 71 Let us see how we can call a prover to prove a formula. As said in  MARCHE Claude committed Dec 08, 2010 72 73 74 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  Guillaume Melquiond committed Feb 01, 2013 75 76 \texttt{add\_*\_decl} of module \texttt{Task}. For the formula $\mathit{true} \lor \mathit{false}$ above, this is done as follows.  Guillaume Melquiond committed Jun 05, 2018 77 \lstinputlisting{generated/logic__buildtask.ml}  Guillaume Melquiond committed Oct 30, 2012 78 To make the formula a goal, we must give a name to it, here goal1''. A  MARCHE Claude committed Dec 08, 2010 79 80 goal name has type \texttt{prsymbol}, for identifiers denoting propositions in a theory or a task. Notice again that the concrete  MARCHE Claude committed Jul 02, 2011 81 syntax of \why requires these symbols to be capitalized, but it is not  MARCHE Claude committed Dec 08, 2010 82 83 mandatory when using the library. The second argument of \texttt{add\_prop\_decl} is the kind of the proposition:  Guillaume Melquiond committed Feb 01, 2013 84 85 86 \texttt{Paxiom}, \texttt{Plemma} or \texttt{Pgoal}. Notice that lemmas are not allowed in tasks and can only be used in theories.  MARCHE Claude committed Dec 08, 2010 87   Andrei Paskevich committed Dec 20, 2010 88 Once a task is built, it can be printed.  Guillaume Melquiond committed Jun 05, 2018 89 \lstinputlisting{generated/logic__printtask.ml}  MARCHE Claude committed Dec 08, 2010 90   Andrei Paskevich committed Dec 20, 2010 91 The task for our second formula is a bit more complex to build, because  Guillaume Melquiond committed Oct 11, 2012 92 the variables A and B must be added as abstract (\ie not defined)  Andrei Paskevich committed Mar 18, 2012 93 propositional symbols in the task.  Guillaume Melquiond committed Jun 05, 2018 94 \lstinputlisting{generated/logic__buildtask2.ml}  MARCHE Claude committed Dec 08, 2010 95 96 97 98 99  Execution of our OCaml program now outputs: \begin{verbatim} task 1 is: theory Task  Andrei Paskevich committed Jun 30, 2011 100  goal Goal1 : true \/ false  MARCHE Claude committed Dec 08, 2010 101 102 103 104 end task 2 is: theory Task  Andrei Paskevich committed Jun 30, 2011 105  predicate A  Andrei Paskevich committed Dec 20, 2010 106   Andrei Paskevich committed Jun 30, 2011 107  predicate B  Andrei Paskevich committed Dec 20, 2010 108   Andrei Paskevich committed Jun 30, 2011 109  goal Goal2 : A /\ B -> A  MARCHE Claude committed Dec 08, 2010 110 111 112 113 end \end{verbatim} \section{Calling External Provers}  MARCHE Claude committed May 07, 2018 114 \label{sec:api:callingprovers}  MARCHE Claude committed Sep 06, 2010 115   Guillaume Melquiond committed Jun 24, 2014 116 To call an external prover, we need to access the \why configuration  Andrei Paskevich committed Jul 02, 2011 117 file \texttt{why3.conf}, as it was built using the \texttt{why3config}  MARCHE Claude committed Dec 08, 2010 118 119 120 command line tool or the \textsf{Detect Provers} menu of the graphical IDE. The following API calls allow to access the content of this configuration file.  Guillaume Melquiond committed Jun 05, 2018 121 \lstinputlisting{generated/logic__getconf.ml}  François Bobot committed Jan 25, 2012 122 The type \texttt{'a Whyconf.Mprover.t} is a map indexed by provers. A  Guillaume Melquiond committed Feb 01, 2013 123 124 125 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 \texttt{Whyconf}:  Guillaume Melquiond committed Jun 05, 2018 126 \lstinputlisting{generated/whyconf__provertype.ml}  François Bobot committed Jan 25, 2012 127 128 The map \texttt{provers} provides the set of existing provers. In the following, we directly  MARCHE Claude committed Apr 09, 2018 129 attempt to access a prover named Alt-Ergo'', any version.  Guillaume Melquiond committed Jun 05, 2018 130 \lstinputlisting{generated/logic__getanyaltergo.ml}  François Bobot committed Jan 25, 2012 131 We could also get a specific version with :  Guillaume Melquiond committed Jun 05, 2018 132 \lstinputlisting{generated/logic__getaltergo200.ml}  MARCHE Claude committed Sep 06, 2010 133   MARCHE Claude committed Dec 16, 2010 134 135 136 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.  Guillaume Melquiond committed Jun 05, 2018 137 \lstinputlisting{generated/logic__getdriver.ml}  MARCHE Claude committed Dec 08, 2010 138 139 140  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  Andrei Paskevich committed Dec 20, 2010 141 termination. Here is a simple way to proceed:  Guillaume Melquiond committed Jun 05, 2018 142 \lstinputlisting{generated/logic__callprover.ml}  Andrei Paskevich committed Dec 20, 2010 143 This way to call a prover is in general too naive, since it may never  MARCHE Claude committed Dec 16, 2010 144 return if the prover runs without time limit. The function  MARCHE Claude committed Apr 09, 2018 145 146 \texttt{prove\_task} has an optional parameter \texttt{limit}, a record defined in module \texttt{Call\_provers}:  Guillaume Melquiond committed Jun 05, 2018 147 \lstinputlisting{generated/call_provers__resourcelimit.ml}  MARCHE Claude committed Apr 09, 2018 148 149 150 where the field \texttt{limit\_time} is the maximum allowed running time in seconds, and \texttt{limit\_mem} is the maximum allowed memory in megabytes. The type \texttt{prover\_result} is a record defined in module \texttt{Call\_provers}:  Guillaume Melquiond committed Jun 05, 2018 151 \lstinputlisting{generated/call_provers__proverresult.ml}  MARCHE Claude committed Apr 09, 2018 152 with in particular the fields:  MARCHE Claude committed Dec 08, 2010 153 \begin{itemize}  Andrei Paskevich committed Dec 20, 2010 154 155 \item \texttt{pr\_answer}: the prover answer, explained below; \item \texttt{pr\_time} : the time taken by the prover, in seconds.  MARCHE Claude committed Dec 08, 2010 156 \end{itemize}  MARCHE Claude committed Apr 09, 2018 157 A \texttt{pr\_answer} is the sum type defined in module \texttt{Call\_provers}:  Guillaume Melquiond committed Jun 05, 2018 158 \lstinputlisting{generated/call_provers__proveranswer.ml}  MARCHE Claude committed Apr 09, 2018 159 corresponding to these kinds of answers:  MARCHE Claude committed Dec 08, 2010 160 161 162 \begin{itemize} \item \texttt{Valid}: the task is valid according to the prover. \item \texttt{Invalid}: the task is invalid.  MARCHE Claude committed Apr 09, 2018 163 164 \item \texttt{Timeout}: the prover exceeds the time limit. \item \texttt{OutOfMemory}: the prover exceeds the memory limit.  MARCHE Claude committed Dec 16, 2010 165 \item \texttt{Unknown} $msg$: the prover can't determine if the task  Andrei Paskevich committed Dec 20, 2010 166  is valid; the string parameter $msg$ indicates some extra  MARCHE Claude committed Dec 16, 2010 167  information.  MARCHE Claude committed Apr 09, 2018 168 \item \texttt{Failure} $msg$: the prover reports a failure, \eg it  MARCHE Claude committed Dec 16, 2010 169 170  was unable to read correctly its input task. \item \texttt{HighFailure}: an error occurred while trying to call the  MARCHE Claude committed Apr 09, 2018 171  prover, or the prover answer was not understood (\eg none of the  Andrei Paskevich committed Dec 20, 2010 172 173  given regular expressions in the driver file matches the output of the prover).  MARCHE Claude committed Dec 08, 2010 174 \end{itemize}  MARCHE Claude committed Dec 16, 2010 175 176 Here is thus another way of calling the Alt-Ergo prover, on our second task.  Guillaume Melquiond committed Jun 05, 2018 177 \lstinputlisting{generated/logic__calltimelimit.ml}  MARCHE Claude committed Dec 08, 2010 178 179 180 181 182 183 184 The output of our program is now as follows. \begin{verbatim} On task 1, alt-ergo answers Valid (0.01s) On task 2, alt-ergo answers Valid in 0.01 seconds \end{verbatim} \section{Building Terms}  MARCHE Claude committed Dec 08, 2010 185 186 187 188 189  An important feature of the functions for building terms and formulas is that they statically guarantee that only well-typed terms can be constructed.  Andrei Paskevich committed Dec 20, 2010 190 Here is the way we build the formula $2+2=4$. The main difficulty is to  MARCHE Claude committed Dec 09, 2010 191 access the internal identifier for addition: it must be retrieved from  Guillaume Melquiond committed Jun 23, 2018 192 193 the standard theory \texttt{Int} of the file \texttt{int.why}. % (see Chap~\ref{sec:library}).  Guillaume Melquiond committed Jun 05, 2018 194 \lstinputlisting{generated/logic__buildfmla.ml}  MARCHE Claude committed Dec 08, 2010 195 196 197 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 \texttt{t\_app\_infer} infers the type of the resulting  MARCHE Claude committed Dec 09, 2010 198 term. One could also provide the expected type as follows.  Guillaume Melquiond committed Jun 05, 2018 199 \lstinputlisting{generated/logic__buildtermalt.ml}  MARCHE Claude committed Dec 08, 2010 200   Andrei Paskevich committed Dec 20, 2010 201 202 When building a task with this formula, we need to declare that we use theory \texttt{Int}:  Guillaume Melquiond committed Jun 05, 2018 203 \lstinputlisting{generated/logic__buildtaskimport.ml}  MARCHE Claude committed Dec 08, 2010 204 205 206  \section{Building Quantified Formulas}  Andrei Paskevich committed Dec 20, 2010 207 208 209 To illustrate how to build quantified formulas, let us consider the formula $\forall x:int. x*x \geq 0$. The first step is to obtain the symbols from \texttt{Int}.  Guillaume Melquiond committed Jun 05, 2018 210 \lstinputlisting{generated/logic__quantfmla1.ml}  MARCHE Claude committed Dec 08, 2010 211 The next step is to introduce the variable $x$ with the type int.  Guillaume Melquiond committed Jun 05, 2018 212 \lstinputlisting{generated/logic__quantfmla2.ml}  Andrei Paskevich committed Dec 20, 2010 213 The formula $x*x \geq 0$ is obtained as in the previous example.  Guillaume Melquiond committed Jun 05, 2018 214 \lstinputlisting{generated/logic__quantfmla3.ml}  MARCHE Claude committed Jul 02, 2011 215 To quantify on $x$, we use the appropriate smart constructor as follows.  Guillaume Melquiond committed Jun 05, 2018 216 \lstinputlisting{generated/logic__quantfmla4.ml}  Andrei Paskevich committed Dec 20, 2010 217   MARCHE Claude committed Dec 08, 2010 218 219 \section{Building Theories}  MARCHE Claude committed Nov 09, 2012 220 221 222 We illustrate now how one can build theories. Building a theory must be done by a sequence of calls: \begin{itemize}  Guillaume Melquiond committed Feb 01, 2013 223 \item creating a theory under construction'', of type \verb|Theory.theory_uc|;  Guillaume Melquiond committed Mar 10, 2014 224 \item adding declarations, one at a time;  MARCHE Claude committed Nov 09, 2012 225 226 227 \item closing the theory under construction, obtaining something of type \verb|Theory.theory|. \end{itemize}  Guillaume Melquiond committed Jun 26, 2014 228 Creation of a theory named \verb|My_theory| is done by  Guillaume Melquiond committed Jun 05, 2018 229 \lstinputlisting{generated/logic__buildth1.ml}  Guillaume Melquiond committed Jun 26, 2014 230 First let us add formula 1 above as a goal:  Guillaume Melquiond committed Jun 05, 2018 231 \lstinputlisting{generated/logic__buildth2.ml}  MARCHE Claude committed Nov 09, 2012 232 233 234 235 236 Note that we reused the goal identifier \verb|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:  Guillaume Melquiond committed Jun 05, 2018 237 \lstinputlisting{generated/logic__buildth3.ml}  MARCHE Claude committed Nov 09, 2012 238 239 240 241 242 243  Adding formula 3 is a bit more complex since it uses integers, thus it requires to use'' the theory \verb|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:  Guillaume Melquiond committed Jun 05, 2018 244 \lstinputlisting{generated/logic__buildth4.ml}  MARCHE Claude committed Nov 09, 2012 245 Addition of formula 3 is then  Guillaume Melquiond committed Jun 05, 2018 246 \lstinputlisting{generated/logic__buildth5.ml}  MARCHE Claude committed Nov 09, 2012 247 248  Addition of goal 4 is nothing more complex:  Guillaume Melquiond committed Jun 05, 2018 249 \lstinputlisting{generated/logic__buildth6.ml}  MARCHE Claude committed Nov 09, 2012 250 251  Finally, we close our theory under construction as follows.  Guillaume Melquiond committed Jun 05, 2018 252 \lstinputlisting{generated/logic__buildth7.ml}  MARCHE Claude committed Nov 09, 2012 253   Guillaume Melquiond committed Jun 26, 2014 254 We can inspect what we did by printing that theory:  Guillaume Melquiond committed Jun 05, 2018 255 \lstinputlisting{generated/logic__printtheory.ml}  MARCHE Claude committed Nov 09, 2012 256 257 which outputs \begin{verbatim}  MARCHE Claude committed Apr 09, 2018 258 259 my new theory is as follows:  MARCHE Claude committed Nov 09, 2012 260 261 theory My_theory (* use BuiltIn *)  MARCHE Claude committed Mar 17, 2017 262   MARCHE Claude committed Nov 09, 2012 263  goal goal1 : true \/ false  MARCHE Claude committed Mar 17, 2017 264   MARCHE Claude committed Nov 09, 2012 265  predicate A  MARCHE Claude committed Mar 17, 2017 266   MARCHE Claude committed Nov 09, 2012 267  predicate B  MARCHE Claude committed Mar 17, 2017 268   MARCHE Claude committed Nov 09, 2012 269  goal goal2 : A /\ B -> A  MARCHE Claude committed Mar 17, 2017 270   MARCHE Claude committed Nov 09, 2012 271  (* use int.Int *)  MARCHE Claude committed Mar 17, 2017 272   MARCHE Claude committed Nov 09, 2012 273  goal goal3 : (2 + 2) = 4  MARCHE Claude committed Mar 17, 2017 274   MARCHE Claude committed Nov 09, 2012 275 276 277  goal goal4 : forall x:int. (x * x) >= 0 end \end{verbatim}  MARCHE Claude committed Nov 09, 2012 278 279 280  From a theory, one can compute at once all the proof tasks it contains as follows:  Guillaume Melquiond committed Jun 05, 2018 281 \lstinputlisting{generated/logic__splittheory.ml}  MARCHE Claude committed Nov 09, 2012 282 283 Note that the tasks are returned in reverse order, so we reverse the list above.  MARCHE Claude committed Nov 09, 2012 284 285  We can check our generated tasks by printing them:  Guillaume Melquiond committed Jun 05, 2018 286 \lstinputlisting{generated/logic__printalltasks.ml}  MARCHE Claude committed Nov 09, 2012 287 288  One can run provers on those tasks exactly as we did above.  MARCHE Claude committed Dec 08, 2010 289   MARCHE Claude committed May 07, 2018 290 \section{Operations on Terms and Formulas, Transformations}  MARCHE Claude committed Sep 06, 2010 291   MARCHE Claude committed May 07, 2018 292 The following code illustrates a simple recursive functions of  MARCHE Claude committed May 29, 2018 293 formulas. It explores the formula and when a negation is found, it  MARCHE Claude committed May 07, 2018 294 295 tries to push it down below a conjunction, a disjunction or a quantifier.  Guillaume Melquiond committed Jun 05, 2018 296 \lstinputlisting{generated/transform__negate.ml}  MARCHE Claude committed Dec 08, 2010 297   MARCHE Claude committed May 07, 2018 298 The following illustrates how to turn such an OCaml function into a  Sylvain Dailler committed Jun 21, 2018 299 transformation in the sense of the Why3 API. Moreover, it registers that  MARCHE Claude committed May 07, 2018 300 transformation to make it available for example in Why3 IDE.  Guillaume Melquiond committed Jun 05, 2018 301 \lstinputlisting{generated/transform__register.ml}  MARCHE Claude committed Dec 08, 2010 302   MARCHE Claude committed May 07, 2018 303 304 The directory \verb|src/transform| contains the code for the many transformations that are already available in Why3.  MARCHE Claude committed Dec 15, 2010 305   Guillaume Melquiond committed Jun 26, 2014 306 \section{Proof Sessions}  MARCHE Claude committed Nov 09, 2012 307   MARCHE Claude committed Jun 28, 2014 308 309 310 See the example \verb|examples/use_api/create_session.ml| of the distribution for an illustration on how to manipulate proof sessions from an OCaml program.  MARCHE Claude committed Nov 09, 2012 311   Guillaume Melquiond committed Jun 26, 2014 312 \section{ML Programs}  MARCHE Claude committed Jun 06, 2013 313   MARCHE Claude committed May 07, 2018 314 315 316 317 318 319 320 321 322 323 324 The simplest way to build \whyml programs from OCaml is to build untyped syntax trees for such programs, and then call the \why typing procedure to build typed declarations. The examples of this section are available in the file \verb|examples/use_api/mlw_tree.ml| of the distribution. The first step is to build an environment as already illustrated in Section~\ref{sec:api:callingprovers}, and open the OCaml module \verb|Ptree| which contains most of the OCaml functions we need in this section.  Guillaume Melquiond committed Jun 05, 2018 325 \lstinputlisting{generated/mlw_tree__buildenv.ml}  MARCHE Claude committed May 07, 2018 326 327 328 329 330  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 \verb|Program|.  Guillaume Melquiond committed Jun 05, 2018 331 \lstinputlisting{generated/mlw_tree__openmodule.ml}  MARCHE Claude committed May 07, 2018 332 333 Notice the use of a first simple helper function \verb|mk_ident| to build an identifier without  Sylvain Dailler committed Jun 21, 2018 334 any attributes nor any location.  MARCHE Claude committed May 07, 2018 335 336 337 338 339  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 \verb|int.Int|.  Guillaume Melquiond committed Jun 05, 2018 340 \lstinputlisting{generated/mlw_tree__useimport.ml}  MARCHE Claude committed May 07, 2018 341 342  We want now to build a program equivalent to the following code in concrete Why3 syntax.  Guillaume Melquiond committed Jun 05, 2018 343 \lstinputlisting[language=why3]{generated/mlw_tree__source1.ml}  MARCHE Claude committed May 07, 2018 344 345  The OCaml code that programmatically build this Why3 function is as follows.  Guillaume Melquiond committed Jun 05, 2018 346 \lstinputlisting{generated/mlw_tree__code1.ml}  MARCHE Claude committed May 07, 2018 347 348 This code makes uses of helper functions that are given in Figure~\ref{fig:helpers}. \begin{figure}[t]  Guillaume Melquiond committed Jun 05, 2018 349  \lstinputlisting{generated/mlw_tree__helper1.ml}  MARCHE Claude committed May 07, 2018 350 351 352 353 354  \caption{Helper functions for building WhyML programs} \label{fig:helpers} \end{figure} We want now to build a program equivalent to the following code in concrete Why3 syntax.  Guillaume Melquiond committed Jun 05, 2018 355 \lstinputlisting[language=why3]{generated/mlw_tree__source2.ml}  MARCHE Claude committed May 07, 2018 356 We need to import the \verb|ref.Ref| module first. The rest is similar to the first example, the code is as follows  Guillaume Melquiond committed Jun 05, 2018 357 \lstinputlisting{generated/mlw_tree__code2.ml}  MARCHE Claude committed May 07, 2018 358 359  The next example makes use of arrays.  Guillaume Melquiond committed Jun 05, 2018 360 \lstinputlisting[language=why3]{generated/mlw_tree__source3.ml}  MARCHE Claude committed May 07, 2018 361 The corresponding OCaml code is as follows  Guillaume Melquiond committed Jun 05, 2018 362 \lstinputlisting{generated/mlw_tree__code3.ml}  MARCHE Claude committed May 07, 2018 363 364 365 366  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.  Guillaume Melquiond committed Jun 05, 2018 367 \lstinputlisting{generated/mlw_tree__closemodule.ml}  MARCHE Claude committed May 07, 2018 368 369  We can then construct the proofs tasks for our module, and then try to  Sylvain Dailler committed Jun 21, 2018 370 call the Alt-Ergo prover. The rest of that code is using OCaml  MARCHE Claude committed May 07, 2018 371 functions that were already introduced before.  Guillaume Melquiond committed Jun 05, 2018 372 \lstinputlisting{generated/mlw_tree__checkingvcs.ml}  MARCHE Claude committed Dec 08, 2010 373   MARCHE Claude committed Sep 06, 2010 374 375 376 377 378 %%% Local Variables: %%% mode: latex %%% TeX-PDF-mode: t %%% TeX-master: "manual" %%% End: