itp.tex 3.74 KB
Newer Older
1 2 3 4 5 6 7

\chapter{Interactive Proof Assistants}

\section{On using an interactive proof assistant from Why3}

\todo{expliquer les principes}

8 9
... We then provide specific information about some ITPs.

10 11
\section{Theory Realizations}
\label{sec:realizations}
12

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
16
axioms. This way, one can show the consistency of an axiomatized
17 18
theory and/or make a connection to an existing library (of the proof
assistant) to ease some proofs.
19
Currently, realizations are supported for the proof assistants Coq and PVS.
20

21
\subsection{Generating a realization}
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
25
the theories to realize, and a target directory.
26
\index{realize@\verb+--realize+}
27 28

\begin{verbatim}
29
why3 --realize -D path/to/drivers/prover-realize.drv
30 31
      -T env_path.theory_name -o path/to/target/dir/
\end{verbatim}
32 33
\index{driver@\verb+--driver+}
\index{theory@\verb+--theory+}
34

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
37
extracts all the parts that it assumes to be user-edited and merges them in
38 39
the generated file.

40
Note that \why does not track dependencies between realizations and
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}.
45

46
\subsection{Using realizations inside proofs}
47

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.
53 54
\index{driver file}

55 56
\begin{verbatim}
theory env_path.theory_name
57
  meta "realized_theory" "env_path.theory_name", "optional_naming"
58 59
end
\end{verbatim}
60

61
The first parameter is the theory name for \why. The second
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.
65
\index{realized_theory@\verb+realized_theory+}
66

67
\subsection{Shipping libraries of realizations}
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
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
74
\verb+meta "realized_theory"+ declarations. The configuration file should be as
75
follows.
76
\index{configuration file}
77 78 79 80 81

\begin{verbatim}
[main]
loadpath="path/to/theories"

82 83
[prover_modifiers]
name="Coq"
84
option="-R path/to/vo/files Logical_directory"
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))\""
93 94
\end{verbatim}

95 96
This configuration file can be passed to \why thanks to the
\verb+--extra-config+ option.
97
\index{extra-config@\verb+--extra-config+}
98 99 100 101
\index{prover_modifiers@\verb+prover_modifiers+}
\index{editor_modifiers@\verb+editor_modifiers+}
\index{option@\verb+option+}
\index{driver@\verb+driver+}
102 103


104 105
\input{./coq.tex}

106 107
\input{./coq_tactic.tex}

108 109 110 111 112
\input{./isabelle.tex}

\input{./pvs.tex}


113 114 115 116 117
%%% Local Variables:
%%% mode: latex
%%% TeX-PDF-mode: t
%%% TeX-master: "manual"
%%% End: