itp.tex 3.74 KB
 MARCHE Claude committed Feb 01, 2014 1 2 3 4 5 6 7  \chapter{Interactive Proof Assistants} \section{On using an interactive proof assistant from Why3} \todo{expliquer les principes}  MARCHE Claude committed Feb 01, 2014 8 9 ... We then provide specific information about some ITPs.  MARCHE Claude committed Feb 01, 2014 10 11 \section{Theory Realizations} \label{sec:realizations}  Guillaume Melquiond committed Mar 23, 2012 12   Jean-Christophe committed Jul 11, 2012 13 14 15 Given a \why theory, one can use a proof assistant to make a \emph{realization} of this theory, that is to provide definitions for some of its uninterpreted symbols and proofs for some of its  Jean-Christophe committed Jul 12, 2012 16 axioms. This way, one can show the consistency of an axiomatized  Jean-Christophe committed Jul 11, 2012 17 18 theory and/or make a connection to an existing library (of the proof assistant) to ease some proofs.  Guillaume Melquiond committed Sep 19, 2012 19 Currently, realizations are supported for the proof assistants Coq and PVS.  Jean-Christophe committed Jul 11, 2012 20   MARCHE Claude committed Feb 01, 2014 21 \subsection{Generating a realization}  Guillaume Melquiond committed Mar 23, 2012 22 23 24  Generating the skeleton for a theory is done by passing to \why the \verb+--realize+ option, a driver suitable for realizations, the names of  Jean-Christophe committed Jul 12, 2012 25 the theories to realize, and a target directory.  Guillaume Melquiond committed Sep 19, 2012 26 \index{realize@\verb+--realize+}  Guillaume Melquiond committed Mar 23, 2012 27 28  \begin{verbatim}  Jean-Christophe committed Jul 11, 2012 29 why3 --realize -D path/to/drivers/prover-realize.drv  Guillaume Melquiond committed Mar 23, 2012 30 31  -T env_path.theory_name -o path/to/target/dir/ \end{verbatim}  Guillaume Melquiond committed Sep 19, 2012 32 33 \index{driver@\verb+--driver+} \index{theory@\verb+--theory+}  Guillaume Melquiond committed Sep 19, 2012 34   Guillaume Melquiond committed Mar 23, 2012 35 36 The name of the generated file is inferred from the theory name. If the target directory already contains a file with the same name, \why  Jean-Christophe committed Jul 12, 2012 37 extracts all the parts that it assumes to be user-edited and merges them in  Guillaume Melquiond committed Mar 23, 2012 38 39 the generated file.  Guillaume Melquiond committed May 07, 2012 40 Note that \why does not track dependencies between realizations and  Jean-Christophe committed Jul 12, 2012 41 42 43 44 theories, so a realization will become outdated if the corresponding theory is modified. It is up to the user to handle such dependencies, for instance using a \texttt{Makefile}.  Guillaume Melquiond committed May 07, 2012 45   MARCHE Claude committed Feb 01, 2014 46 \subsection{Using realizations inside proofs}  Guillaume Melquiond committed Mar 23, 2012 47   Jean-Christophe committed Jul 12, 2012 48 49 50 51 52 If a theory has been realized, the \why printer for the corresponding prover will no longer output declarations for that theory but instead simply put a directive to load the realization. In order to tell the printer that a given theory is realized, one has to add a meta declaration in the corresponding theory section of the driver.  Guillaume Melquiond committed Sep 19, 2012 53 54 \index{driver file}  Guillaume Melquiond committed Mar 23, 2012 55 56 \begin{verbatim} theory env_path.theory_name  Guillaume Melquiond committed Oct 30, 2012 57  meta "realized_theory" "env_path.theory_name", "optional_naming"  Guillaume Melquiond committed Mar 23, 2012 58 59 end \end{verbatim}  Guillaume Melquiond committed Sep 19, 2012 60   Guillaume Melquiond committed Sep 19, 2012 61 The first parameter is the theory name for \why. The second  Guillaume Melquiond committed Mar 23, 2012 62 63 64 parameter, if not empty, provides a name to be used inside generated scripts to point to the realization, in case the default name is not suitable for the interactive prover.  Guillaume Melquiond committed Oct 30, 2012 65 \index{realized_theory@\verb+realized_theory+}  Guillaume Melquiond committed Mar 23, 2012 66   MARCHE Claude committed Feb 01, 2014 67 \subsection{Shipping libraries of realizations}  Guillaume Melquiond committed Mar 23, 2012 68 69 70  While modifying an existing driver file might be sufficient for local use, it does not scale well when the realizations are to be shipped to  Guillaume Melquiond committed Sep 19, 2012 71 72 73 other users. Instead, one should create two additional files: a configuration file that indicates how to modify paths, provers, and editors, and a driver file that contains only the needed  Guillaume Melquiond committed Oct 30, 2012 74 \verb+meta "realized_theory"+ declarations. The configuration file should be as  Guillaume Melquiond committed Sep 19, 2012 75 follows.  Guillaume Melquiond committed Sep 19, 2012 76 \index{configuration file}  Guillaume Melquiond committed Mar 23, 2012 77 78 79 80 81  \begin{verbatim} [main] loadpath="path/to/theories"  Guillaume Melquiond committed Sep 19, 2012 82 83 [prover_modifiers] name="Coq"  Guillaume Melquiond committed Mar 23, 2012 84 option="-R path/to/vo/files Logical_directory"  Guillaume Melquiond committed Sep 19, 2012 85 86 87 88 89 90 91 92 driver="path/to/file/with/meta.drv" [editor_modifiers coqide] option="-R path/to/vo/files Logical_directory" [editor_modifiers proofgeneral-coq] option="--eval \"(setq coq-load-path (cons '(\\\"path/to/vo/files\\\" \ \\\"Logical_directory\\\") coq-load-path))\""  Guillaume Melquiond committed Mar 23, 2012 93 94 \end{verbatim}  Guillaume Melquiond committed Sep 19, 2012 95 96 This configuration file can be passed to \why thanks to the \verb+--extra-config+ option.  Guillaume Melquiond committed Sep 19, 2012 97 \index{extra-config@\verb+--extra-config+}  Guillaume Melquiond committed Sep 19, 2012 98 99 100 101 \index{prover_modifiers@\verb+prover_modifiers+} \index{editor_modifiers@\verb+editor_modifiers+} \index{option@\verb+option+} \index{driver@\verb+driver+}  MARCHE Claude committed Jul 19, 2012 102 103   MARCHE Claude committed Feb 01, 2014 104 105 \input{./coq.tex}  MARCHE Claude committed Feb 01, 2014 106 107 \input{./coq_tactic.tex}  MARCHE Claude committed Feb 01, 2014 108 109 110 111 112 \input{./isabelle.tex} \input{./pvs.tex}  MARCHE Claude committed Jul 19, 2012 113 114 115 116 117 %%% Local Variables: %%% mode: latex %%% TeX-PDF-mode: t %%% TeX-master: "manual" %%% End: