Commit 87a315ab authored by Guillaume Melquiond's avatar Guillaume Melquiond

Inline most footnotes and listings in the HTML manual.

parent 3f1a2e2c
......@@ -38,6 +38,8 @@
\setcounter{bottomnumber}{4}
\setcounter{totalnumber}{8}
\newstyle{table.lstframe}{width:100\%;border-width:1px;}
% \usepackage[toc,nonumberlist]{glossaries}
% \makeglossaries
......
......@@ -45,13 +45,18 @@ The GUI is launched on the file above as follows.
why3ide hello_proof.why
\end{verbatim}
When the GUI is started for the first time, you should get a window
which looks like the screenshot of Figure~\ref{fig:gui1}.
that looks like the screenshot of Figure~\ref{fig:gui1}.
The left column is a tool bar which provides different actions to
apply on goals. The section ``Provers'' displays the provers that were
detected as installed on your computer\footnote{If not done yet, you
detected as installed on your computer.%
%BEGIN LATEX
\footnote{If not done yet, you
must perform prover autodetection using \texttt{why3config
--detect-provers}}. Three provers were detected, in this case
--detect-provers}}
%END LATEX
%HEVEA {} (If not done yet, you must perform prover autodetection using \texttt{why3config --detect-provers}.)
Three provers were detected, in this case,
these are Alt-Ergo~\cite{ergo}, Coq~\cite{CoqArt} and
Simplify~\cite{simplify05}.
......
......@@ -13,19 +13,16 @@ logic with polymorphic types.
\section{Example 1: lists}
The Figure~\ref{fig:tutorial1} contains an example of \why input
text, containing three theories. The first theory, \texttt{List},
declares a new algebraic type for polymorphic lists, \texttt{list 'a}.
As in ML, \texttt{'a} stands for a type variable.
The type \texttt{list 'a} has two constructors, \texttt{Nil} and
\texttt{Cons}. Both constructors can be used as usual function
symbols, respectively of type \texttt{list 'a} and \texttt{'a
$\times$ list 'a $\rightarrow$ list 'a}.
We deliberately make this theory that short, for reasons which will be
discussed later.
%BEGIN LATEX
Figure~\ref{fig:tutorial1} contains an example of \why input
text, containing three theories.
%END LATEX
%HEVEA The code below is an example of \why input text, containing three theories.
%BEGIN LATEX
\begin{figure}
\centering
%END LATEX
\begin{whycode}
theory List
type list 'a = Nil | Cons 'a (list 'a)
......@@ -58,9 +55,21 @@ theory Sorted
x <= y -> sorted (Cons y l) -> sorted (Cons x (Cons y l))
end
\end{whycode}
%BEGIN LATEX
\caption{Example of Why3 text.}
\label{fig:tutorial1}
\end{figure}
%END LATEX
The first theory, \texttt{List},
declares a new algebraic type for polymorphic lists, \texttt{list 'a}.
As in ML, \texttt{'a} stands for a type variable.
The type \texttt{list 'a} has two constructors, \texttt{Nil} and
\texttt{Cons}. Both constructors can be used as usual function
symbols, respectively of type \texttt{list 'a} and \texttt{'a
$\times$ list 'a $\rightarrow$ list 'a}.
We deliberately make this theory that short, for reasons which will be
discussed later.
The next theory, \texttt{Length}, introduces the notion of list
length. The \texttt{use import List} command indicates that this new
......@@ -118,8 +127,20 @@ by ``cloning''. A \texttt{clone} declaration constructs a local
copy of the cloned theory, possibly instantiating some of its
abstract (\emph{i.e.}~declared but not defined) symbols.
%BEGIN LATEX
Consider the continued example in Figure~\ref{fig:tutorial2}.
%END LATEX
%HEVEA Consider the continued example below.
We write an abstract theory of partial orders, declaring an
abstract type \texttt{t} and an abstract binary predicate
\texttt{<=}. Notice that an infix operation must be enclosed
in parentheses when used outside a term. We also specify
three axioms of a partial order.
%BEGIN LATEX
\begin{figure}
\centering
%END LATEX
\begin{whycode}
theory Order
type t
......@@ -149,16 +170,11 @@ theory SortedIntList
clone SortedGen with type O.t = int, predicate O.(<=) = (<=)
end
\end{whycode}
%BEGIN LATEX
\caption{Example of Why3 text (continued).}
\label{fig:tutorial2}
\end{figure}
Consider the continued example in Figure~\ref{fig:tutorial2}.
We write an abstract theory of partial orders, declaring an
abstract type \texttt{t} and an abstract binary predicate
\texttt{<=}. Notice that an infix operation must be enclosed
in parentheses when used outside a term. We also specify
three axioms of a partial order.
%END LATEX
There is little value in \texttt{use}'ing such a theory: this
would constrain us to stay with the type \texttt{t}. However,
......@@ -299,7 +315,11 @@ this feature is rarely used.
We now consider another, slightly more complex example: how to use \why
to solve a little puzzle known as ``Einstein's logic
problem''\footnote{This \why example was contributed by St\'ephane Lescuyer.}.
problem''.%
%BEGIN LATEX
\footnote{This \why example was contributed by St\'ephane Lescuyer.}
%END LATEX
%HEVEA {} (This \why example was contributed by St\'ephane Lescuyer.)
The problem is stated as follows. Five persons, of five
different nationalities, live in five houses in a row, all
painted with different colors.
......
......@@ -161,9 +161,12 @@ keyword \texttt{invariant}, immediately after the keyword \texttt{do}.
There is no need to introduce a variant, as the termination of a
\texttt{for} loop is automatically guaranteed.
This completes module \texttt{MaxAndSum}.
%BEGIN LATEX
Figure~\ref{fig:MaxAndSum} shows the whole code.
\begin{figure}
\centering
%END LATEX
%HEVEA The whole code is shown below.
\begin{whycode}
module MaxAndSum
......@@ -186,10 +189,12 @@ module MaxAndSum
end
\end{whycode}
%BEGIN LATEX
\vspace*{-1em}%\hrulefill
\caption{Solution for VSTTE'10 competition problem 1.}
\label{fig:MaxAndSum}
\end{figure}
%END LATEX
We can now proceed to its verification.
Running \texttt{why3}, or better \texttt{why3ide}, on file
\verb|max_sum.mlw| will show a single verification condition with name
......@@ -267,11 +272,16 @@ which simply expresses the values assigned to array \texttt{b} so far:
\end{whycode}
Here we chose to have array \texttt{b} as argument; returning a
freshly allocated array would be equally simple.
%BEGIN LATEX
The whole module is given in Figure~\ref{fig:Inverting}.
%END LATEX
%HEVEA The whole module is given below.
The verification conditions for function \texttt{inverting} are easily
discharged automatically, thanks to the lemma.
%BEGIN LATEX
\begin{figure}
\centering
%END LATEX
\begin{whycode}
module InvertingAnInjection
......@@ -302,10 +312,12 @@ module InvertingAnInjection
end
\end{whycode}
%BEGIN LATEX
\vspace*{-1em}%\hrulefill
\caption{Solution for VSTTE'10 competition problem 2.}
\label{fig:Inverting}
\end{figure}
%END LATEX
\section{Problem 3: Searching a Linked List}
......@@ -388,10 +400,15 @@ or no zero value was found, and thus the returned value is exactly
\end{whycode}
Solving the problem is simply a matter of calling \texttt{search} with
0 as first argument.
The code is given Figure~\ref{fig:LinkedList}. The verification
conditions are all discharged automatically.
%BEGIN LATEX
The code is given Figure~\ref{fig:LinkedList}.
%END LATEX
%HEVEA The code is given below.
The verification conditions are all discharged automatically.
%BEGIN LATEX
\begin{figure}
\centering
%END LATEX
\begin{whycode}
module SearchingALinkedList
......@@ -421,10 +438,12 @@ module SearchingALinkedList
end
\end{whycode}
%BEGIN LATEX
\vspace*{-1em}%\hrulefill
\caption{Solution for VSTTE'10 competition problem 3.}
\label{fig:LinkedList}
\end{figure}
%END LATEX
Alternatively, we can implement the search with a \texttt{while} loop.
To do this, we need to import references from the standard library,
......@@ -548,9 +567,14 @@ the loop is reached, \texttt{True} is returned.
end
\end{whycode}
The assertion in the exception handler is a cut for SMT solvers.
%BEGIN LATEX
This first part of the solution is given in Figure~\ref{fig:NQueens1}.
%END LATEX
%HEVEA This first part of the solution is given below.
%BEGIN LATEX
\begin{figure}
\centering
%END LATEX
\begin{whycode}
module NQueens
use import int.Int
......@@ -586,10 +610,12 @@ module NQueens
False
end
\end{whycode}
%BEGIN LATEX
\vspace*{-1em}%\hrulefill
\caption{Solution for VSTTE'10 competition problem 4 (1/2).}
\label{fig:NQueens1}
\end{figure}
%END LATEX
We now proceed with the verification of the backtracking algorithm.
The specification requires us to define the notion of solution, which
......@@ -686,12 +712,17 @@ search on row 0. The postcondition is also twofold, as for
raises { Solution -> solution board n }
= bt_queens board n 0
\end{whycode}
%BEGIN LATEX
This second part of the solution is given Figure~\ref{fig:NQueens2}.
%END LATEX
%HEVEA This second part of the solution is given below.
With the help of a few auxiliary lemmas --- not given here but available
from \why's sources --- the verification conditions are all discharged
automatically, including the verification of the lemmas themselves.
%BEGIN LATEX
\begin{figure}
\centering
%END LATEX
\begin{whycode}
predicate is_board (board: array int) (pos: int) =
forall q:int. 0 <= q < pos -> 0 <= board[q] < length board
......@@ -732,11 +763,12 @@ automatically, including the verification of the lemmas themselves.
end
\end{whycode}
%BEGIN LATEX
\vspace*{-1em}%\hrulefill
\caption{Solution for VSTTE'10 competition problem 4 (2/2).}
\label{fig:NQueens2}
\end{figure}
%END LATEX
\section{Problem 5: Amortized Queue}
......@@ -858,10 +890,15 @@ a one line code.
ensures { sequence result = sequence q ++ Cons x Nil }
= create q.front q.lenf (Cons x q.rear) (q.lenr + 1)
\end{whycode}
The code is given Figure~\ref{fig:AQueue}. The verification conditions
are all discharged automatically.
%BEGIN LATEX
The code is given Figure~\ref{fig:AQueue}.
%END LATEX
%HEVEA The code is given below.
The verification conditions are all discharged automatically.
%BEGIN LATEX
\begin{figure}[p]
\centering
%END LATEX
\begin{whycode}
module AmortizedQueue
use import int.Int
......@@ -907,10 +944,12 @@ module AmortizedQueue
= create q.front q.lenf (Cons x q.rear) (q.lenr + 1)
end
\end{whycode}
%BEGIN LATEX
\vspace*{-1em}%\hrulefill
\caption{Solution for VSTTE'10 competition problem 5.}
\label{fig:AQueue}
\end{figure}
%END LATEX
% other examples: same fringe ?
......
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