itp.tex 4.64 KB
Newer Older
 MARCHE Claude committed Feb 01, 2014 1 \chapter{Interactive Proof Assistants}  Guillaume Melquiond committed Oct 02, 2017 2 %HEVEA\cutname{itp.html}  MARCHE Claude committed Feb 01, 2014 3   MARCHE Claude committed Mar 13, 2014 4 % ... We then provide specific information about some ITPs.  MARCHE Claude committed Feb 01, 2014 5   MARCHE Claude committed Mar 13, 2014 6 7 8 9 10 11 12 13 14 15 16 17 18 19 \section{Using an Interactive Proof Assistant to Discharge Goals} Instead of calling an automated theorem prover to discharge a goal, \why offers the possibility to call an interactive theorem prover instead. In that case, the interaction is decomposed into two distinct phases: \begin{itemize} \item Edition of a proof script for the goal, typically inside a proof editor provided by the external interactive theorem prover; \item Replay of an existing proof script. \end{itemize} An example of such an interaction is given in the tutorial section~\ref{sec:gui}.  Piotr Trojanek committed Aug 29, 2014 20 Some proof assistants offer more than one possible editor, \eg a  MARCHE Claude committed Mar 13, 2014 21 22 23 choice between the use of a dedicated editor and the use of the Emacs editor and the ProofGeneral mode. Selection of the preferred mode can be made in \texttt{why3ide} preferences, under the Editors'' tab.  MARCHE Claude committed Feb 01, 2014 24   MARCHE Claude committed Feb 01, 2014 25 26 \section{Theory Realizations} \label{sec:realizations}  Guillaume Melquiond committed Mar 23, 2012 27   Jean-Christophe committed Jul 11, 2012 28 29 30 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 31 axioms. This way, one can show the consistency of an axiomatized  Jean-Christophe committed Jul 11, 2012 32 33 theory and/or make a connection to an existing library (of the proof assistant) to ease some proofs.  MARCHE Claude committed Mar 13, 2014 34 %Currently, realizations are supported for the proof assistants Coq and PVS.  Jean-Christophe committed Jul 11, 2012 35   MARCHE Claude committed Feb 01, 2014 36 \subsection{Generating a realization}  Guillaume Melquiond committed Mar 23, 2012 37   Guillaume Melquiond committed Jun 03, 2014 38 39 Generating the skeleton for a theory is done by passing to the \texttt{realize} command a driver suitable for realizations, the names of  Jean-Christophe committed Jul 12, 2012 40 the theories to realize, and a target directory.  Guillaume Melquiond committed Jun 03, 2014 41 \index{realize@\texttt{realize}}  Guillaume Melquiond committed Mar 23, 2012 42 43  \begin{verbatim}  Guillaume Melquiond committed Jun 03, 2014 44 45 why3 realize -D path/to/drivers/prover-realize.drv -T env_path.theory_name -o path/to/target/dir/  Guillaume Melquiond committed Mar 23, 2012 46 \end{verbatim}  Guillaume Melquiond committed Sep 19, 2012 47 48 \index{driver@\verb+--driver+} \index{theory@\verb+--theory+}  Guillaume Melquiond committed Sep 19, 2012 49   Guillaume Melquiond committed Jun 03, 2014 50 51 52 53 The theory is looked into the files from the environment, \eg the standard library. If the theory is stored in a different location, option \texttt{-L} should be used.  Guillaume Melquiond committed Mar 23, 2012 54 55 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 56 extracts all the parts that it assumes to be user-edited and merges them in  Guillaume Melquiond committed Mar 23, 2012 57 58 the generated file.  Guillaume Melquiond committed May 07, 2012 59 Note that \why does not track dependencies between realizations and  Jean-Christophe committed Jul 12, 2012 60 61 62 63 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 64   MARCHE Claude committed Feb 01, 2014 65 \subsection{Using realizations inside proofs}  Guillaume Melquiond committed Mar 23, 2012 66   Jean-Christophe committed Jul 12, 2012 67 68 69 70 71 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 72 73 \index{driver file}  Guillaume Melquiond committed Mar 23, 2012 74 75 \begin{verbatim} theory env_path.theory_name  Guillaume Melquiond committed Oct 30, 2012 76  meta "realized_theory" "env_path.theory_name", "optional_naming"  Guillaume Melquiond committed Mar 23, 2012 77 78 end \end{verbatim}  Guillaume Melquiond committed Sep 19, 2012 79   Guillaume Melquiond committed Sep 19, 2012 80 The first parameter is the theory name for \why. The second  Guillaume Melquiond committed Mar 23, 2012 81 82 83 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 84 \index{realized_theory@\verb+realized_theory+}  Guillaume Melquiond committed Mar 23, 2012 85   MARCHE Claude committed Feb 01, 2014 86 \subsection{Shipping libraries of realizations}  Guillaume Melquiond committed Mar 23, 2012 87 88 89  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 90 91 92 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 93 \verb+meta "realized_theory"+ declarations. The configuration file should be as  Guillaume Melquiond committed Sep 19, 2012 94 follows.  Guillaume Melquiond committed Sep 19, 2012 95 \index{configuration file}  Guillaume Melquiond committed Mar 23, 2012 96 97 98 99 100  \begin{verbatim} [main] loadpath="path/to/theories"  Guillaume Melquiond committed Sep 19, 2012 101 102 [prover_modifiers] name="Coq"  Guillaume Melquiond committed Mar 23, 2012 103 option="-R path/to/vo/files Logical_directory"  Guillaume Melquiond committed Sep 19, 2012 104 105 106 107 108 109 110 111 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 112 113 \end{verbatim}  Guillaume Melquiond committed Sep 19, 2012 114 115 This configuration file can be passed to \why thanks to the \verb+--extra-config+ option.  Guillaume Melquiond committed Sep 19, 2012 116 \index{extra-config@\verb+--extra-config+}  Guillaume Melquiond committed Sep 19, 2012 117 118 119 120 \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 121 122   MARCHE Claude committed Feb 01, 2014 123 124 125 126 127 128 129 \input{./coq.tex} \input{./isabelle.tex} \input{./pvs.tex}  MARCHE Claude committed Jul 19, 2012 130 131 132 133 134 %%% Local Variables: %%% mode: latex %%% TeX-PDF-mode: t %%% TeX-master: "manual" %%% End: