Commit ef2899d2 by Guillaume Melquiond

### Improve documentation a bit.

parent b484b2b1
 ... ... @@ -360,13 +360,13 @@ be done by a sequence of calls: \item closing the theory under construction, obtaining something of type \verb|Theory.theory|. \end{itemize} Creation of a theory named \verb|My_theory| is done by: Creation of a theory named \verb|My_theory| is done by \begin{ocamlcode} let my_theory : Theory.theory_uc = Theory.create_theory (Ident.id_fresh "My_theory") \end{ocamlcode} First let us add the formula 1 above as a goal: First let us add formula 1 above as a goal: \begin{ocamlcode} let decl_goal1 : Decl.decl = Decl.create_prop_decl Decl.Pgoal goal_id1 fmla1 ... ... @@ -424,7 +424,7 @@ Finally, we close our theory under construction as follows. let my_theory : Theory.theory = Theory.close_theory my_theory \end{ocamlcode} We can inspect what we did for example by printing that theory: We can inspect what we did by printing that theory: \begin{ocamlcode} let () = printf "@[theory is:@\n%a@]@." Pretty.print_theory my_theory \end{ocamlcode} ... ... @@ -472,21 +472,21 @@ let () = One can run provers on those tasks exactly as we did above. \section{Applying transformations} \section{Applying Transformations} [TO BE COMPLETED] \section{Writing new functions on term} \section{Writing New Functions on Terms} [TO BE COMPLETED] % pattern-matching on terms, opening a quantifier \section{Proof sessions} \section{Proof Sessions} 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. \section{ML programs} \section{ML Programs} There are two ways for building \whyml programs from OCaml. The first is to build untyped syntax trees for such \whyml programs, and then ... ...
 ... ... @@ -14,7 +14,7 @@ The Coq tactic is installed in where \textit{why3-lib-dir} is \why's library directory, as reported by \verb+why3 --print-libdir+. This directory is automatically added to Coq's load path if you are calling Coq via \why (from \texttt{why3ide}, \texttt{why3replay}, calling Coq via \why (from \texttt{why3 ide}, \texttt{why3 replay}, etc.). If you are calling Coq by yourself, you need to add this directory to Coq's load path, either using Coq's command line option \texttt{-I} or by adding ... ... @@ -33,6 +33,7 @@ The Coq tactic is called \texttt{why3} and is used as follows: The string \textit{prover-name} identifies one of the automated theorem provers supported by \why, as reported by \verb+why3 --list-provers+ (interactive provers excluded). \index{list-provers@\verb+--list-provers+} The current goal is then translated to \why's logic and the prover is called. If it reports the goal to be valid, then Coq's \texttt{admit} tactic is used to assume the goal. The prover is called with a time ... ...
 ... ... @@ -34,7 +34,8 @@ It is also installable from sources, downloadable from the site \noindent For some of the \why tools, additional OCaml libraries are needed: \begin{itemize} \item For the graphical interface: the Lablgtk2 library for OCaml \item For the graphical interface, the Lablgtk2 library is needed. It provides OCaml bindings of the gtk2 graphical library. For Debian-based Linux distributions, you can install the packages \begin{verbatim} ... ... @@ -43,7 +44,8 @@ liblablgtk2-ocaml-dev liblablgtksourceview2-ocaml-dev It is also installable from sources, available from the site \url{http://wwwfun.kurims.kyoto-u.ac.jp/soft/olabl/lablgtk.html} \item For \texttt{why3 bench}: The OCaml bindings of the sqlite3 library. \item For \texttt{why3 bench}, the OCaml bindings of the sqlite3 library are needed. For Debian-based Linux distributions, you can install the package \begin{verbatim} libsqlite3-ocaml-dev ... ... @@ -91,7 +93,7 @@ Everything OK. \end{verbatim} \end{enumerate} \section{Local use, without installation} \section{Local Use, Without Installation} It is not mandatory to install \why into system directories. \why can be configured and compiled for local use as follows: ... ... @@ -127,7 +129,7 @@ Section~\ref{sec:why3config}. \section{Multiple Versions of the Same Prover} Since version 0.72, \why is able to use several versions of the same \why is able to use several versions of the same prover, \eg it can use both CVC3 2.2 and CVC3 2.4.1 at the same time. The automatic detection of provers looks for typical names for their executable command, \eg \texttt{cvc3} for CVC3. However, if you ... ... @@ -136,6 +138,7 @@ use specialized executable names, such as \texttt{cvc3-2.2} or \texttt{cvc3-2.4.1}. To allow the \why detection process to recognize these, you can use the option \verb|--add-prover| with the \texttt{config} command, \eg \index{add-prover@\verb+--add-prover+} \begin{verbatim} why3 config --detect --add-prover cvc3-2.4 /usr/local/bin/cvc3-2.4.1 \end{verbatim} ... ...
 ... ... @@ -87,7 +87,7 @@ tracking system.) The result of provers detection is stored in the user's configuration file (\verb+~/.why3.conf+ or, in the case of local installation, \verb+why3.conf+ in Why3 sources top directory). This file installation, \verb+why3.conf+ in \why sources top directory). This file is also human-readable, and advanced users may modify it in order to experiment with different ways of calling provers, \eg different versions of the same prover, or with different options. ... ... @@ -143,15 +143,16 @@ The \texttt{prove} command executes the following steps: \item Parse and typecheck the given files using the correct parser in order to obtain a set of \why theories for each file. It uses the filename extension or the \verb|--format| option to choose among the available parsers. The \verb|--list-format| option gives the list of registered parsers. among the available parsers. \verb|why3 --list-formats| lists the registered parsers. \index{list-formats@\verb+--list-formats+} \whyml modules are turned into theories containing verification conditions as goals. \item Extract the selected goals inside each of the selected theories into tasks. The goals and theories are selected using options \verb|-G/--goal| and \verb|-T/--theory|. Option \verb|-T/--theory| applies to the last file appearing on the command line, the option \verb|-G/--goal| applies to the last theory \verb|-T/--theory| applies to the previous file appearing on the command line. Option \verb|-G/--goal| applies to the previous theory appearing on the command line. If no theories are selected in a file, then every theory is considered as selected. If no goals are selected in a theory, then every goal is considered as selected. ... ... @@ -159,21 +160,22 @@ The \texttt{prove} command executes the following steps: \index{goal@\verb+--goal+} \index{T@\verb+-T+|see{\texttt{-{}-theory}}} \index{theory@\verb+--theory+} \item Apply the transformation requested \item Apply the transformations requested with \verb|-a/--apply-transform| in their order of appearance on the command line. \verb|--list-transforms| lists the known transformations, plugins can add more of them. command line. \verb|why3 --list-transforms| lists the known transformations; plugins can add more of them. \index{a@\verb+-a+|see{\texttt{-{}-apply-transform}}} \index{apply-transform@\verb+--apply-transform+} \index{list-transforms@\verb+--list-transforms+} \item Apply the driver selected with the \verb|-D/--driver| option, or the driver of the prover selected with the \verb|-P/--prover| option. \verb|--list-provers| lists the known provers, \ie the ones option. \verb|why3 --list-provers| lists the known provers, \ie the ones that appear in the configuration file. \index{D@\verb+-D+|see{\texttt{-{}-driver}}} \index{driver@\verb+--driver+} \index{P@\verb+-P+|see{\texttt{-{}-prover}}} \index{prover@\verb+--prover+} \index{list-provers@\verb+--list-provers+} \item If option \verb|-P/--prover| is given, call the selected prover on each generated task and print the results. If option \verb|-D/--driver| is given, print each generated task using ... ... @@ -509,7 +511,6 @@ of the definitions is irrelevant. Notice that one can use axiomatizations. One can run all the bench given in one bench configuration file with \texttt{why3bench}: \begin{verbatim} why3 bench -B path_to_my_bench.rc \end{verbatim} ... ... @@ -989,7 +990,7 @@ add the option \verb|-F| to force this behavior. \section{The \texttt{doc} command} \section{The \texttt{doc} Command} \label{sec:why3doc} This tool can produce HTML pages from \why source code. ... ...
 ... ... @@ -250,6 +250,7 @@ Known provers: coq (Coq) simplify (Simplify) \end{verbatim} \index{list-provers@\verb+--list-provers+} The first word of each line is a unique identifier for the associated prover. We thus have now the three provers Alt-Ergo~\cite{ergo}, Coq~\cite{CoqArt} and Simplify~\cite{simplify05}. ... ...
 ... ... @@ -11,7 +11,7 @@ These declarations can be directly written in the theory or taken from existing theories. The base logic of \why is first-order logic with polymorphic types. \section{Example 1: lists} \section{Example 1: Lists} %BEGIN LATEX Figure~\ref{fig:tutorial1} contains an example of \why input ... ... @@ -56,7 +56,8 @@ theory Sorted end \end{whycode} %BEGIN LATEX \caption{Example of Why3 text.} \vspace*{-1em}%\hrulefill \caption{Example of \why text} \label{fig:tutorial1} \end{figure} %END LATEX ... ... @@ -118,7 +119,7 @@ Note that the type signature of \lstinline{sorted} predicate does not include the name of a parameter (see \texttt{l} in the definition of \texttt{length}): it is unused and therefore optional. \section{Example 1 (continued): lists and abstract orderings} \section{Example 1 (continued): Lists and Abstract Orderings} In the previous section we have seen how a theory can reuse the declarations of another theory, coming either from the same input ... ... @@ -171,7 +172,8 @@ theory SortedIntList end \end{whycode} %BEGIN LATEX \caption{Example of Why3 text (continued).} \vspace*{-1em}%\hrulefill \caption{Example of \why text (continued)} \label{fig:tutorial2} \end{figure} %END LATEX ... ... @@ -307,10 +309,10 @@ namespace import O clone export Order end \end{whycode} However, since \why favours short theories over long and complex ones, However, since \why favors short theories over long and complex ones, this feature is rarely used. \section{Example 2: Einstein's problem} \section{Example 2: Einstein's Problem} \index{Einstein's logic problem} We now consider another, slightly more complex example: how to use \why ... ... @@ -323,7 +325,7 @@ problem''.% The problem is stated as follows. Five persons, of five different nationalities, live in five houses in a row, all painted with different colors. These five persones own different pets, drink different beverages and These five persons own different pets, drink different beverages and smoke different brands of cigars. We are given the following information: \begin{itemize} ... ...
 ... ... @@ -10,7 +10,7 @@ The XML file follows the DTD given in \texttt{share/why3session.dtd} and reprodu \lstinputlisting{../share/why3session.dtd} \section{Provers detection data} \section{Prover Detection} \label{sec:proverdetecttiondata} All the necessary data configuration for the automatic detection of ... ... @@ -26,12 +26,31 @@ file is reproduced below. } %END LATEX \section{The \texttt{why3.conf} configuration file} \section{The \texttt{why3.conf} Configuration File} \label{sec:whyconffile} \index{why3.conf@\texttt{why3.conf}}\index{configuration file} \begin{figure}[p] One can use a custom configuration file. The \why tools look for it in the following order: \begin{enumerate} \item the file specified by the \texttt{-C} or \texttt{-{}-config} options, \item the file specified by the environment variable \texttt{WHY3CONFIG} if set, \item the file \texttt{\$HOME/.why3.conf} (\texttt{\$USERPROFILE/.why3.conf} under Windows) or, in the case of local installation, \texttt{why3.conf} in the top directory of \why sources. \end{enumerate} If none of these files exist, a built-in default configuration is used. The configuration file is a human-readable text file, which consists of association pairs arranged in sections. %BEGIN LATEX Figure~\ref{fig:why3conf} shows an example of configuration file. %END LATEX %HEVEA Below is an example of configuration file. %BEGIN LATEX \begin{figure}[p] {\footnotesize %END LATEX \begin{verbatim} ... ... @@ -90,28 +109,10 @@ name = "CoqIDE" \end{verbatim} %BEGIN LATEX } %END LATEX \caption{Sample why3.conf file} \caption{Sample \texttt{why3.conf} file} \label{fig:why3conf} \end{figure} One can use a custom configuration file. \texttt{why3config} and other \texttt{why3} tools look for it in the following order: \begin{enumerate} \item the file specified by the \texttt{-C} or \texttt{-{}-config} options, \item the file specified by the environment variable \texttt{WHY3CONFIG} if set, \item the file \texttt{\$HOME/.why3.conf} (\texttt{\$USERPROFILE/.why3.conf} under Windows) or, in the case of local installation, \texttt{why3.conf} in the top directory of \why sources. \end{enumerate} If none of these files exists, a built-in default configuration is used. The configuration file is a human-readable text file, which consists of association pairs arranged in sections. Figure~\ref{fig:why3conf} shows an example of configuration file. %END LATEX A section begins with a header inside square brackets and ends at the beginning of the next section. The header of a ... ... @@ -121,15 +122,16 @@ argument, \texttt{prover} is one family name, \texttt{coq} and \texttt{alt-ergo} are the family argument. Sections contain associations \texttt{key=value}. A value is either an integer (\eg{} -555), a boolean (true, false), or a string (\eg "emacs"). Some specific keys can be attributed multiple values and are an integer (\eg \texttt{-555}), a boolean (\texttt{true}, \texttt{false}), or a string (\eg \texttt{"emacs"}). Some specific keys can be attributed multiple values and are thus allowed to occur several times inside a given section. In that case, the relative order of these associations matter. \section{Drivers of External Provers} \section{Drivers for External Provers} \label{sec:drivers} Drivers of external provers are readable files from directory Drivers for external provers are readable files from directory \texttt{drivers}. Experimented users can modify them to change the way the external provers are called, in particular which transformations are applied to goals. ... ... @@ -148,6 +150,7 @@ installation is given by \begin{verbatim} why3 --list-transforms \end{verbatim} \index{list-transforms@\verb+--list-transforms+} \subsection{Non-splitting transformations} ... ... @@ -220,7 +223,6 @@ definitions~\cite{paskevich09rr}. \item[inline\_trivial] removes definitions of the form \begin{whycode} function f x_1 ... x_n = (g e_1 ... e_k) predicate p x_1 ... x_n = (q e_1 ... e_k) ... ...
 ... ... @@ -129,7 +129,7 @@ pattern matching immediately: We are now left with the function body itself, that is a code computing the sum and the maximum of all elements in \texttt{a}. With no surpise, it is as simple as introducing two local references no surprise, it is as simple as introducing two local references \begin{whycode} let sum = ref 0 in let max = ref 0 in ... ... @@ -192,7 +192,7 @@ end \end{whycode} %BEGIN LATEX \vspace*{-1em}%\hrulefill \caption{Solution for VSTTE'10 competition problem 1.} \caption{Solution for VSTTE'10 competition problem 1} \label{fig:MaxAndSum} \end{figure} %END LATEX ... ... @@ -315,7 +315,7 @@ end \end{whycode} %BEGIN LATEX \vspace*{-1em}%\hrulefill \caption{Solution for VSTTE'10 competition problem 2.} \caption{Solution for VSTTE'10 competition problem 2} \label{fig:Inverting} \end{figure} %END LATEX ... ... @@ -441,7 +441,7 @@ end \end{whycode} %BEGIN LATEX \vspace*{-1em}%\hrulefill \caption{Solution for VSTTE'10 competition problem 3.} \caption{Solution for VSTTE'10 competition problem 3} \label{fig:LinkedList} \end{figure} %END LATEX ... ... @@ -613,7 +613,7 @@ module NQueens \end{whycode} %BEGIN LATEX \vspace*{-1em}%\hrulefill \caption{Solution for VSTTE'10 competition problem 4 (1/2).} \caption{Solution for VSTTE'10 competition problem 4 (1/2)} \label{fig:NQueens1} \end{figure} %END LATEX ... ... @@ -766,7 +766,7 @@ end \end{whycode} %BEGIN LATEX \vspace*{-1em}%\hrulefill \caption{Solution for VSTTE'10 competition problem 4 (2/2).} \caption{Solution for VSTTE'10 competition problem 4 (2/2)} \label{fig:NQueens2} \end{figure} %END LATEX ... ... @@ -947,7 +947,7 @@ end \end{whycode} %BEGIN LATEX \vspace*{-1em}%\hrulefill \caption{Solution for VSTTE'10 competition problem 5.} \caption{Solution for VSTTE'10 competition problem 5} \label{fig:AQueue} \end{figure} %END LATEX ... ...
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
{"extraction_info": {"found_math": true, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 1, "mathjax_display_tex": 0, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0, "katex": 0, "math-container": 0, "wp-katex-eq": 0, "align": 0, "equation": 0, "x-ck12": 0, "texerror": 0, "math_score": 0.9993669390678406, "perplexity": 12256.024673469472}, "config": {"markdown_headings": true, "markdown_code": true, "boilerplate_config": {"ratio_threshold": 0.18, "absolute_threshold": 10, "end_threshold": 15, "enable": true}, "remove_buttons": true, "remove_image_figures": true, "remove_link_clusters": true, "table_config": {"min_rows": 2, "min_cols": 3, "format": "plain"}, "remove_chinese": true, "remove_edit_buttons": true, "extract_latex": true}, "warc_path": "s3://commoncrawl/crawl-data/CC-MAIN-2022-33/segments/1659882573760.75/warc/CC-MAIN-20220819191655-20220819221655-00166.warc.gz"}