realizations.tex 3.68 KB
Newer Older
1 2 3 4 5 6 7 8 9 10
\chapter{Theory realizations}
\label{chap:realizations}

\section{Generating a realization}

Generating the skeleton for a theory is done by passing to \why the
\verb+--realize+ option, a driver suitable for realizations, the names of
the theories to realize, and the target directory.

\begin{verbatim}
11
why3 --realize -D path/to/drivers/coq-realize.drv
12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93
      -T env_path.theory_name -o path/to/target/dir/
\end{verbatim}

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
extracts all the parts that it assumes to be user-made and prints them in
the generated file.

\section{Using realizations inside proofs}

If a theory has been realized, a \why printer for an interactive prover
will no longer output assumptions from the theory but instead simply put
a directive to load the realization. In order to indicate to the printer
that a given theory is realized, one has to add a meta declaration to the
corresponding theory section.

\begin{verbatim}
theory env_path.theory_name
  meta "realized" "env_path.theory_name", "optional_naming"
end
\end{verbatim}

The first parameter is the theory name for \why, while the second
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.

\section{Coq scripts}

This section describes the content of the Coq files generated by \why for
both proof obligations and theory realizations. When reading a Coq
script, \why is guided by the presence of empty lines to split the
script, so the user should refrain from removing empty lines around
generated parts or adding empty lines inside them.

\begin{enumerate}
\item	The header of the file contains all the library inclusions
	required by the driver file. Any user-made changes to this part
	will be lost when the file is regenerated by \why. This part ends
	at the first empty line.
\item	Abstract logic symbols are assumed with the vernacular directive
	\verb+Paramater+. Axioms are assumed with the \verb+Axiom+
	directive. When regenerating a script, \why assumes that all such
	symbols have been generated by a previous run. As a consequence,
	the user should not introduce new symbols with these two
	directives, as they would be lost.
\item	Definitions of functions and inductive types in theories are
	printed in a block that starts with \verb+(* Why3 assumption *)+.
	This comment should not be removed; otherwise \why will assume
	that the definition is user-made.
\item	Finally, proof obligations and symbols to be realized are
	introduced by \verb+(* Why3 goal *)+. The user is supposed to
	fill the script after the statement. \why assumes that the
	user-made part extends up to \verb+Qed+, \verb+Admitted+,
	\verb+Save+, or \verb+Defined+, whichever comes first. In the
	case of definitions, the original statement can be replaced by
	a \verb+Notation+ directive, in order to ease the usage of
	already defined symbols.
\end{enumerate}

Currently, the parser for Coq scripts is rather naive and does not know
much about comments. For instance, \why can easily be confused by
some terminating directive like \verb+Qed+ that would be present in a
comment.

\section{Shipping libraries of realizations}

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
other users. Instead, an additional configuration file should be created.

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

[prover coq]
option="-R path/to/vo/files Logical_directory"
driver="path/to/extra_coq.drv"
\end{verbatim}

This file can be passed to \why thanks to the \verb+--extra-config+
option.