Commit 014b5455 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Fix documentation.

parent 28fcb939
......@@ -356,7 +356,7 @@ We illustrate now how one can build theories. Building a theory must
be done by a sequence of calls:
\begin{itemize}
\item creating a theory ``under construction'', of type \verb|Theory.theory_uc|;
\item adding declarations, one at a time ;
\item adding declarations, one at a time;
\item closing the theory under construction, obtaining something of type \verb|Theory.theory|.
\end{itemize}
......@@ -488,20 +488,20 @@ an illustration on how to manipulate proof sessions from an OCaml program.
\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
call the Why3 typing procedure to build typed declarations. The second
There are two ways for building \whyml programs from OCaml. The first
is to build untyped syntax trees for such \whyml programs, and then
call the \why typing procedure to build typed declarations. The second
way is to directly build typed programs using smart constructors that
check well-typedness at each step.
The first approach, building untyped trees and then typed them, is
The first approach, building untyped trees and then typing them, is
examplified in file \verb|examples/use_api/mlw_tree.ml| of the
distribution. The second approach is
examplified in file \verb|examples/use_api/mlw.ml|. The first approach
is significantly simpler to do since the internal typing mechanism
using regions remains implicit, whereas when one uses the second
approach one should care about such typing. On the other hand, the
second approach is more `''efficient'' in the sense that no
second approach is more ``efficient'' in the sense that no
intermediate form needs to be built in memory.
......
\subsection{Coq Tactic}
\label{sec:coqtactic}
\why\ provides a Coq tactic to call external theorem provers as oracles.
\why provides a Coq tactic to call external theorem provers as oracles.
\subsubsection{Installation}
......@@ -37,7 +37,7 @@ 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
limit in seconds as given by \why's configuration file
(see page~\pageref{sec:whyconffile}). A different value may be given
(see Section~\ref{sec:whyconffile}). A different value may be given
using the \texttt{timelimit} keyword.
\subsubsection{Error messages.} The following errors may be reported by
......
......@@ -5,9 +5,15 @@
This chapter show how \whyml code can be executed, either by being
interpreted or compiled to some existing programming language.
Let us consider the program in Fig.~\ref{fig:MaxAndSum}
\begin{latexonly}
Let us consider the program in Figure~\ref{fig:MaxAndSum}
on page~\pageref{fig:MaxAndSum} that computes the maximum and the sum
of an array of integers.
\end{latexonly}
\begin{htmlonly}
Let us consider the program of Section~\ref{sec:MaxAndSum} that computes
the maximum and the sum of an array of integers.
\end{htmlonly}
Let us assume it is contained in a file \texttt{maxsum.mlw}.
\section{Interpreting \whyml Code}
......@@ -27,7 +33,7 @@ in module \texttt{MaxAndSum}
and then we use option \verb+--exec+ to interpret this function,
as follows:
\begin{verbatim}
> why3 maxsum.mlw --exec MaxAndSum.test
> why3 maxsum.mlw --exec MaxAndSum.test
Execution of MaxAndSum.test ():
type: (int, int)
result: Tuple2(45, 10)
......@@ -76,7 +82,7 @@ OCaml code extracted from \why must be linked with the library
stored in subdirectory \texttt{why3} of the OCaml standard library.
Depending on the way \why was installed, it depends either on library
\texttt{nums.cmxa} or \texttt{zarith.cmxa} for big integers. Above we
assumed the latter. it is likely that additional options \texttt{-I}
assumed the latter. It is likely that additional options \texttt{-I}
must be passed to the OCaml compiler for libraries
\texttt{zarith.cmxa} and \texttt{why3extract.cmxa} to be found.
......
\chapter{Interactive Proof Assistants}
\section{On using an interactive proof assistant from Why3}
\section{Using an Interactive Proof Assistant from \why}
\todo{expliquer les principes}
......
......@@ -10,9 +10,9 @@ provided by the \why environment. These are as follows:
provers, on the command-line.
\item[\texttt{why3ide}] graphical interface to display goals, run
provers and transformations on them.
\item[\texttt{why3bench}] produces benchmarks.
\item[\texttt{why3replayer}] replays the proofs stored in a session,
for regression test purposes.
\item[\texttt{why3bench}] produces benchmarks.
\item[\texttt{why3session}] dumps various informations from a proof
session, and possibly modifies the session.
\item[\texttt{why3doc}] produces HTML versions of \why source codes.
......@@ -46,7 +46,7 @@ particular, option \verb|-help| displays the usage and options.
sets all debug flags (except flags which change the behavior).
\index{debug-all@\verb+--debug-all+}
\item[\texttt{-{}-debug \textsl{<flag>}}]
set a specific debug flag.
sets a specific debug flag.
\index{debug@\verb+--debug+}
\item[\texttt{-v}]
prints version information.
......@@ -54,7 +54,7 @@ particular, option \verb|-help| displays the usage and options.
displays the usage and the exact list of options for the given tool.
\end{description}
\section{The \texttt{why3config} command-line tool}
\section{\texttt{why3config}}
\label{sec:why3config}
\why must be configured to access external provers. Typically, this is done
......@@ -66,8 +66,8 @@ the command line tool \texttt{why3config}.
%%File/Detect provers
%%\end{verbatim}
%%of the IDE.
This must be redone each time a new prover is installed.
\index{why3config@\texttt{why3config}}
This must be redone each time a new prover is installed.%
\index{why3config@\texttt{why3config}}%
\index{configuration file}
The provers which \why attempts to detect are described in
......@@ -115,7 +115,7 @@ can be obtained by the option \verb|--list-prover-ids|.
\index{add-prover@\verb+--add-prover+}
\index{list-prover-ids@\verb+--list-prover-ids+}
\section{The \texttt{why3} command-line tool}
\section{\texttt{why3}}
\label{sec:why3ref}
\why is primarily used to call provers on goals contained in an
......@@ -203,7 +203,7 @@ multiple times with reduced context. The minimal set of declarations is
then written in the prover syntax into a file located in the directory
given to the \verb|-o/--output| option.
\section{The \texttt{why3ide} GUI}
\section{\texttt{why3ide}}
\label{sec:ideref}
The basic usage of the GUI is described by the tutorial of
......@@ -414,10 +414,10 @@ are grouped together under several tabs.
\begin{itemize}
\item The default editor to use when the \textsf{Edit} button is
pressed.
\urldef{\urlprfgen}{\url}{http://proofgeneral.inf.ed.ac.uk/}
\item For each installed prover, a specific editor can be selected to
override the default. Typically if you install the Coq prover, then
the editor to use will be set to ``CoqIDE'' by default, and this
\urldef{\urlprfgen}{\url}{http://proofgeneral.inf.ed.ac.uk/}
dialog allows you to select the Emacs editor and its
\ahref{\urlprfgen}{Proof General} mode instead%
\begin{latexonly} (\urlprfgen)\end{latexonly}.
......@@ -432,7 +432,7 @@ are grouped together under several tabs.
\end{description}
\section{The \texttt{why3bench} tool}
\section{\texttt{why3bench}}
The \texttt{why3bench} tool adds a scheduler on top of the \why
library. \texttt{why3bench} is designed to compare various components
......@@ -453,7 +453,7 @@ comparison in various formats:
\end{itemize}
The compared components can be defined in an \emph{rc-file};
\texttt{examples/programs/\ prgbench.rc} is such an example. More
\texttt{examples/misc/prgbench.rc} is an example of such a file. More
generally, a bench configuration file looks like
\begin{verbatim}
[probs "myprobs"]
......@@ -509,7 +509,7 @@ One can run all the bench given in one bench configuration file with
why3bench -B path_to_my_bench.rc
\end{verbatim}
\section{The \texttt{why3replayer} tool}
\section{\texttt{why3replayer}}
\label{sec:why3replayer}
The purpose of the \texttt{why3replayer} tool is to execute the proofs
......@@ -615,7 +615,7 @@ if the smoke detector has been triggered, or \texttt{No smoke
\section{The \texttt{why3session} tool}
\section{\texttt{why3session}}
\label{sec:why3session}
The program \texttt{why3session} allows to extract informations from
......@@ -995,18 +995,19 @@ add the option \verb|-F| to force this behavior.
\section{The \texttt{why3doc} tool}
\section{\texttt{why3doc}}
\label{sec:why3doc}
This tool can produce HTML pages from \why source code. A source file
is scanned, \why code for theories or modules is output in
This tool can produce HTML pages from \why source code.
\why code for theories or modules is output in
preformatted HTML code. Comments are interpreted in three different ways.
\begin{itemize}
\item Comments starting with at least three stars are completed
ignored.
\item Comments starting with two stars are interpreted as textual
documentation. Special constructs are interpreted as described
below.
below. When the previous line is not empty, the comment is indented to
the right, so as to be displayed as a description of that line.
\item Comments starting with one star only are interpreted as code
comments, and are typeset as the code
\end{itemize}
......@@ -1021,10 +1022,10 @@ identifier use to its definition.
\item[\texttt{-o \textsl{<dir>}}] defines the directory where to
output the HTML files.
\item[\texttt{-{}-output \textsl{<dir>}}] is the same as \verb|-o|.
\item[\texttt{-{}-index}] (resp. \verb|--no-index|) generates
(resp. does not generate) an index file \texttt{index.html}.
The default behavior is to generate an index if more than one file
\item[\texttt{-{}-index}] generates an index file \texttt{index.html}.
This is the default behavior if more than one file
is passed on the command line.
\item[\texttt{-{}-no-index}] prevents the generation of an index file.
\item[\texttt{-{}-title \textsl{<title>}}] sets title of the
index page.
\item[\texttt{-{}-stdlib-url \textsl{<url>}}] sets a URL for files
......@@ -1036,20 +1037,18 @@ identifier use to its definition.
Some constructs are interpreted:
\begin{itemize}
\item \texttt{\{\textsl{c text}\}} interprets character \textsl{c} as
some typesetting command, detailed below
some typesetting command:
\begin{description}
\item[1-6] a heading of level 1 to 6 respectively
\item[h] raw HTML
\end{description}
\item \texttt{[\textsl{code}]} is a code escape: the text
\textsl{code} is typeset as \why code.
\end{itemize}
The typesetting commands are
\begin{description}
\item[1-6] a heading of level 1 to 6 respectively
\item[h] raw HTML
\end{description}
The HTML rendering is controlled via a CSS file \verb|style.css|
generated in the same directory as output files. This CSS style can be
modified manually: regenerating the doc will not overwrite an existing
A CSS file \verb|style.css| suitable for rendering is generated in the
same directory as output files. This CSS style can be modified manually,
since regenerating the HTML documentation will not overwrite an existing
\verb|style.css| file.
......
......@@ -3,30 +3,34 @@
This chapter gives the grammar and semantics for \why and \whyml input files.
\section{Lexical conventions}
\section{Lexical Conventions}
Lexical conventions are common to \why and \whyml.
% TODO: blanks
\paragraph{Comments.}
\subsection{Comments}
Comments are enclosed by \texttt{(*} and \texttt{*)} and can be nested.
\paragraph{Strings.}
\subsection{Strings}
Strings are enclosed in double quotes (\verb!"!). Double quotes can be
inserted in strings using the backslash character (\verb!\!).
escaped in strings using the backslash character (\verb!\!).
The other special sequences are \verb!\n! for line feed and \verb!\t!
for horizontal tab.
In the following, strings are referred to with the non-terminal
\nonterm{string}{}.
% TODO: escape sequences for strings
\subsection{Identifiers}
\paragraph{Identifiers.} The syntax distinguishes lowercase and
The syntax distinguishes lowercase and
uppercase identifiers and, similarly, lowercase and uppercase
qualified identifiers.
\begin{center}\framebox{\input{./qualid_bnf.tex}}\end{center}
\paragraph{Constants.}
\subsection{Constants}
The syntax for constants is given in Figure~\ref{fig:bnf:constant}.
Integer and real constants have arbitrary precision.
Integer constants may be given in base 16, 10, 8 or 2.
......@@ -38,7 +42,8 @@ Real constants may be given in base 16 or 10.
\label{fig:bnf:constant}
\end{figure}
\paragraph{Operators.}
\subsection{Operators}
Prefix and infix operators are built from characters organized in four
categories (\textsl{op-char-1} to \textsl{op-char-4}).
\begin{center}\framebox{\input{./operator_bnf.tex}}\end{center}
......@@ -55,7 +60,9 @@ characters they are built from:
\item level 1: all other operators (non-terminal \textit{infix-op-1}).
\end{itemize}
\paragraph{Labels.} Identifiers, terms, formulas, program expressions
\subsection{Labels}
Identifiers, terms, formulas, program expressions
can all be labeled, either with a string, or with a location tag.
\begin{center}\framebox{\input{./label_bnf.tex}}\end{center}
A location tag consists of a file name, a line number, and starting
......@@ -63,9 +70,10 @@ and ending characters.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Why3 Language}
\section{The Why3 Language}
\subsection{Terms}
\paragraph{Terms.}
The syntax for terms is given in Figure~\ref{fig:bnf:term}.
The various constructs have the following priorities and
associativities, from lowest to greatest priority:
......@@ -98,14 +106,17 @@ application is not allowed (rejected at typing).
\label{fig:bnf:term}
\end{figure}
\paragraph{Type Expressions.} The syntax for type expressions is the following:
\subsection{Type Expressions}
The syntax for type expressions is the following:
\begin{center}\framebox{\input{./type_bnf.tex}}\end{center}
Built-in types are \texttt{int}, \texttt{real}, and tuple types.
Note that the syntax for type
expressions notably differs from the usual ML syntax (\eg the
type of polymorphic lists is written \texttt{list 'a}, not \texttt{'a list}).
\paragraph{Formulas.}
\subsection{Formulas}
The syntax for formulas is given Figure~\ref{fig:bnf:formula}.
The various constructs have the following priorities and
associativities, from lowest to greatest priority:
......@@ -146,7 +157,8 @@ transformations. For instance, \texttt{split} transforms the goal
transforms \verb!not (A || B)! into subgoals \verb|not A| and
\verb|not ((not A) /\ B)|.
\paragraph{Theories.}
\subsection{Theories}
The syntax for theories is given on Figure~\ref{fig:bnf:theorya} and~\ref{fig:bnf:theoryb}.
\begin{figure}
......@@ -161,18 +173,19 @@ The syntax for theories is given on Figure~\ref{fig:bnf:theorya} and~\ref{fig:bn
\label{fig:bnf:theoryb}
\end{figure}
\paragraph{Files.}
\subsection{Files}
A \why input file is a (possibly empty) list of theories.
\begin{center}\framebox{\input{./why_file_bnf.tex}}\end{center}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\clearpage
\section{WhyML Language}\label{sec:syntax:whyml}
\section{The \whyml Language}\label{sec:syntax:whyml}
\subsection{Specification}
The syntax for specification clauses in programs
The syntax for specification clauses in programs
is given in Figure~\ref{fig:bnf:spec}.
\begin{figure}
\begin{center}\framebox{\input{./spec_bnf.tex}}\end{center}
......@@ -363,9 +376,9 @@ variables, functions, exceptions).
A \whyml input file is a (possibly empty) list of theories and modules.
\begin{center}\framebox{\input{./whyml_file_bnf.tex}}\end{center}
A theory defined in a \whyml\ file can only be used within that
A theory defined in a \whyml file can only be used within that
file. If a theory is supposed to be reused from other files, be they
\why\ or \whyml\ files, it should be defined in a \why\ file.
\why or \whyml files, it should be defined in a \why file.
\section{The \why Standard Library}
......
\chapter{The WhyML Programming Language}
\chapter{The \whyml Programming Language}
\label{chap:whyml}
This chapter describes the \whyml programming language.
A \whyml input text contains a list of theories (see
chapter~\ref{chap:syntax}) and/or modules.
Chapter~\ref{chap:syntax}) and/or modules.
Modules extend theories with \emph{programs}.
Programs can use all types, symbols, and constructs from the logic.
They also provide extra features:
......@@ -56,6 +56,7 @@ The source code for all these examples is contained in \why's
distribution, in sub-directory \texttt{examples/}.
\section{Problem 1: Sum and Maximum}
\label{sec:MaxAndSum}
The first problem is stated as follows:
\begin{quote}
......@@ -86,7 +87,7 @@ declaration:
\end{whycode}
Modules \texttt{Ref} and \texttt{Array} respectively provide a type
\texttt{ref 'a} for references and a type \texttt{array 'a} for
arrays (see Section~\ref{sec:mllibrary}), together with useful
arrays, together with useful
operations and traditional syntax. They are loaded from the \whyml
files \texttt{ref.mlw} and \texttt{array.mlw} in the standard library.
\why reports an error when it finds a theory and a module with
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment