Commit 7ad702fd authored by Guillaume Melquiond's avatar Guillaume Melquiond

Modify the manual slightly so that it can at least go through hevea without crashing.

parent 10950a1d
......@@ -64,6 +64,7 @@ DEPFLAGS += -native
endif
RUBBER = @RUBBER@
HEVEA = @HEVEA@
#PSVIEWER = @PSVIEWER@
#PDFVIEWER = @PDFVIEWER@
......@@ -1233,8 +1234,9 @@ DOCTEX = $(addprefix doc/, $(addsuffix .tex, $(DOC)))
doc/manual.pdf: $(BNFTEX) $(DOCTEX) doc/manual.bib
cd doc; $(RUBBER) --warn all --pdf manual.tex
# doc/manual.html: doc/manual.tex doc/version.tex
# $(MAKE) -C doc manual.html
# the dependency on the pdf ensures the bbl was built
doc/manual.html: doc/manual.pdf
cd doc; $(HEVEA) -fix fix.hva makeidx.hva manual.tex
clean::
cd doc; $(RUBBER) --pdf --clean manual.tex
......
......@@ -299,6 +299,9 @@ if test "$RUBBER" = no ; then
fi
fi
# checking for hevea
AC_CHECK_PROG(HEVEA,hevea,hevea,no)
# checking for lablgtk2
if test "$enable_ide" = yes ; then
if test "$USEOCAMLFIND" = yes; then
......
\usepackage{book}
\newcommand{\fontsize}[2]{}
......@@ -80,10 +80,7 @@ literate=%
%
}
% default language is Why3
\lstset{language=why3}
\lstnewenvironment{why3}{\lstset{language=why3}}{}
\lstnewenvironment{whycode}{\lstset{language=why3}}{}
%%% Local Variables:
%%% mode: latex
......
......@@ -777,7 +777,7 @@ output.
\begin{center}
\input{HelloProof.tex}
\end{center}
\verbatiminput{./replayer_macros.tex}
\lstinputlisting{./replayer_macros.tex}
\caption{Sample macros for the LaTeX command}
\label{fig:latex}
\end{figure}
......
......@@ -12,6 +12,7 @@
\usepackage{graphicx}
\usepackage{listings}
\usepackage{xspace}
\usepackage{hevea}
\setulmarginsandblock{30mm}{30mm}{*}
\setlrmarginsandblock{30mm}{30mm}{*}
......@@ -35,8 +36,8 @@
% for ocamldoc generated pages
%\usepackage{ocamldoc}
\let\tt\ttfamily
\let\bf\bfseries
%\let\tt\ttfamily
%\let\bf\bfseries
\usepackage{ifthen}
\input{./macros.tex}
......@@ -58,7 +59,8 @@
\vfill
{\fontsize{40}{40pt}\selectfont\bfseries\sffamily The Why3 platform}
{\Huge\fontsize{40}{40pt}
\selectfont\bfseries\sffamily The Why3 platform}
\vfill
......
......@@ -148,9 +148,9 @@ Currently, the GUI does not allow to modify the input file. You must
edit the file external by some editor of your choice. Let's assume we
change the goal $G_2$ by replacing the first occurrence of true by
false, \eg
\begin{why3}
\begin{whycode}
goal G2 : (false -> false) /\ (true \/ false)
\end{why3}
\end{whycode}
We can reload the modified file in the IDE using menu \textsf{File/Reload}, or the shortcut ``Ctrl-R''. We get the tree view shown on Figure~\ref{fig:gui5}.
\begin{figure}[tbp]
......
......@@ -26,7 +26,7 @@ discussed later.
\begin{figure}
\centering
\begin{why3}
\begin{whycode}
theory List
type list 'a = Nil | Cons 'a (list 'a)
end
......@@ -57,7 +57,7 @@ theory Sorted
forall x y : int, l : list int.
x <= y -> sorted (Cons y l) -> sorted (Cons x (Cons y l))
end
\end{why3}
\end{whycode}
\caption{Example of Why3 text.}
\label{fig:tutorial1}
\end{figure}
......@@ -97,11 +97,11 @@ an inductive predicate. Every such definition is a list of clauses:
universally closed implications where the consequent is an instance
of the defined predicate. Moreover, the defined predicate may only
occur in positive positions in the antecedent. For example, a clause:
\begin{why3}
\begin{whycode}
| Sorted_Bad :
forall x y : int, l : list int.
(sorted (Cons y l) -> y > x) -> sorted (Cons x (Cons y l))
\end{why3}
\end{whycode}
would not be allowed. This positivity condition assures the logical
soundness of an inductive definition.
......@@ -120,7 +120,7 @@ abstract (\emph{i.e.}~declared but not defined) symbols.
\begin{figure}
\centering
\begin{why3}
\begin{whycode}
theory Order
type t
predicate (<=) t t
......@@ -148,7 +148,7 @@ theory SortedIntList
use import int.Int
clone SortedGen with type O.t = int, predicate O.(<=) = (<=)
end
\end{why3}
\end{whycode}
\caption{Example of Why3 text (continued).}
\label{fig:tutorial2}
\end{figure}
......@@ -228,7 +228,9 @@ we can launch the following command:
> why3 lists.why -T SortedIntList
\end{verbatim}
to see the resulting theory \texttt{SortedIntList}:
\begin{why3}
\ifhevea
\else
\begin{whycode}
theory SortedIntList
(* use BuiltIn *)
(* use Int *)
......@@ -255,7 +257,8 @@ theory SortedIntList
prop Le_trans2 = Le_trans, prop Le_asym2 = Le_asym,
prop Le_refl2 = Le_refl *)
end
\end{why3}
\end{whycode}
\fi
In conclusion, let us briefly explain the concept of namespaces
in \why. Both \texttt{use} and \texttt{clone} instructions can
......@@ -286,11 +289,11 @@ would be \texttt{T.$s$}.
\why allows to open new namespaces explicitly in the text. In particular,
the instruction ``\texttt{clone import Order as O}'' can be equivalently
written as:
\begin{why3}
namespace import O
clone export Order
end
\end{why3}
\begin{whycode}
namespace import O
clone export Order
end
\end{whycode}
However, since \why favours short theories over long and complex ones,
this feature is rarely used.
......@@ -343,7 +346,7 @@ We start by introducing a general-purpose theory defining the notion
of \emph{bijection}, as two abstract types together with two functions from
one to the other and two axioms stating that these functions are
inverse of each other.
\begin{why3}
\begin{whycode}
theory Bijection
type t
type u
......@@ -354,45 +357,45 @@ theory Bijection
axiom To_of : forall x : t. to (of x) = x
axiom Of_to : forall y : u. of (to y) = y
end
\end{why3}
\end{whycode}
We now start a new theory, \texttt{Einstein}, which will contain all
the individuals of the problem.
\begin{why3}
\begin{whycode}
theory Einstein "Einstein's problem"
\end{why3}
\end{whycode}
First we introduce enumeration types for houses, colors, persons,
drinks, cigars and pets.
\begin{why3}
\begin{whycode}
type house = H1 | H2 | H3 | H4 | H5
type color = Blue | Green | Red | White | Yellow
type person = Dane | Englishman | German | Norwegian | Swede
type drink = Beer | Coffee | Milk | Tea | Water
type cigar = Blend | BlueMaster | Dunhill | PallMall | Prince
type pet = Birds | Cats | Dogs | Fish | Horse
\end{why3}
\end{whycode}
We now express that each house is associated bijectively to a color,
by cloning the \texttt{Bijection} theory appropriately.
\begin{why3}
\begin{whycode}
clone Bijection as Color with type t = house, type u = color
\end{why3}
\end{whycode}
It introduces two functions, namely \texttt{Color.of} and
\texttt{Color.to}, from houses to colors and colors to houses,
respectively, and the two axioms relating them.
Similarly, we express that each house is associated bijectively to a
person
\begin{why3}
\begin{whycode}
clone Bijection as Owner with type t = house, type u = person
\end{why3}
\end{whycode}
and that drinks, cigars and pets are all associated bijectively to persons:
\begin{why3}
\begin{whycode}
clone Bijection as Drink with type t = person, type u = drink
clone Bijection as Cigar with type t = person, type u = cigar
clone Bijection as Pet with type t = person, type u = pet
\end{why3}
\end{whycode}
Next we need a way to state that a person lives next to another. We
first define a predicate \texttt{leftof} over two houses.
\begin{why3}
\begin{whycode}
predicate leftof (h1 h2 : house) =
match h1, h2 with
| H1, H2
......@@ -401,49 +404,49 @@ first define a predicate \texttt{leftof} over two houses.
| H4, H5 -> true
| _ -> false
end
\end{why3}
\end{whycode}
Note how we advantageously used pattern matching, with an or-pattern
for the four positive cases and a universal pattern for the remaining
21 cases. It is then immediate to define a \texttt{neighbour}
predicate over two houses, which completes theory \texttt{Einstein}.
\begin{why3}
\begin{whycode}
predicate rightof (h1 h2 : house) =
leftof h2 h1
predicate neighbour (h1 h2 : house) =
leftof h1 h2 \/ rightof h1 h2
end
\end{why3}
\end{whycode}
The next theory contains the 15 hypotheses. It starts by importing
theory \texttt{Einstein}.
\begin{why3}
\begin{whycode}
theory EinsteinHints "Hints"
use import Einstein
\end{why3}
\end{whycode}
Then each hypothesis is stated in terms of \texttt{to} and \texttt{of}
functions. For instance, the hypothesis ``The Englishman lives in a
red house'' is declared as the following axiom.
\begin{why3}
\begin{whycode}
axiom Hint1: Color.of (Owner.to Englishman) = Red
\end{why3}
\end{whycode}
And so on for all other hypotheses, up to
``The man who smokes Blends has a neighbour who drinks water'', which completes
this theory.
\begin{why3}
\begin{whycode}
...
axiom Hint15:
neighbour (Owner.to (Cigar.to Blend)) (Owner.to (Drink.to Water))
end
\end{why3}
\end{whycode}
Finally, we declare the goal in the fourth theory:
\begin{why3}
\begin{whycode}
theory Problem "Goal of Einstein's problem"
use import Einstein
use import EinsteinHints
goal G: Pet.to Fish = German
end
\end{why3}
\end{whycode}
and we are ready to use \why to discharge this goal with any prover
of our choice.
......
......@@ -7,7 +7,7 @@ The proof session state is stored in an XML file named
\texttt{\textsl{<dir>}/why3session.xml}, where \texttt{\textsl{<dir>}}
is the directory of the project.
The XML file follows the DTD given in \texttt{share/why3session.dtd} and reproduced below.
\verbatiminput{../share/why3session.dtd}
\lstinputlisting{../share/why3session.dtd}
\section{Provers detection data}
......@@ -18,7 +18,7 @@ installed provers is stored in the file
\texttt{provers-detection-data.conf} typically located in directory
\verb|/usr/local/share/why3| after installation. The contents of this
file is reproduced below.
{\footnotesize\verbatiminput{../share/provers-detection-data.conf}}
{\footnotesize\lstinputlisting{../share/provers-detection-data.conf}}
\section{The \texttt{why3.conf} configuration file}
\label{sec:whyconffile}
......
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