Mentions légales du service

Skip to content
Snippets Groups Projects
Commit 4de24d90 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

doc: manual now uses LaTeX package listings

parent 5ca4a174
No related branches found
No related tags found
No related merge requests found
...@@ -33,6 +33,57 @@ ...@@ -33,6 +33,57 @@
\newcommand{\emptystring}{$\epsilon$} \newcommand{\emptystring}{$\epsilon$}
\newcommand{\below}{See\; below} \newcommand{\below}{See\; below}
%%% listings for Why3 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\RequirePackage{listings}
\RequirePackage{amssymb}
\lstset{basicstyle={\ttfamily},framesep=2pt,frame=single}
\lstdefinelanguage{why3}
{
morekeywords=[1]{namespace,predicate,function,inductive,type,use,clone,%
import,export,theory,end,in,with,%
goal,axiom,lemma,forall},%
keywordstyle=[1]{\color{blue}},%
otherkeywords={},%
string=[b]",%
showstringspaces=false,%
stringstyle=\itshape,%
commentstyle=\itshape,%
columns=[l]fullflexible,%
sensitive=true,%
morecomment=[s]{(*}{*)},%
escapeinside={*?}{?*},%
keepspaces=true,
literate=%
%{'a}{$\alpha$}{1}%
%{'b}{$\beta$}{1}%
%{<}{$<$}{1}%
%{>}{$>$}{1}%
%{<=}{$\le$}{1}%
%{>=}{$\ge$}{1}%
% {<>}{$\ne$}{1}%
% {/\\}{$\land$}{1}%
% {\\/}{ $\lor$ }{3}%
% {\ or(}{ $\lor$(}{3}%
% {not\ }{$\lnot$ }{1}%
% {not(}{$\lnot$(}{1}%
% {+->}{\texttt{+->}}{2}%
% % {+->}{$\mapsto$}{2}%
% {-->}{\texttt{-\relax->}}{2}%
% %{-->}{$\longrightarrow$}{2}%
% {->}{$\rightarrow$}{2}%
% {<->}{$\leftrightarrow$}{2}%
%
%
}
% default language is Why3
\lstset{language=why3}
\lstnewenvironment{why3}{\lstset{language=why3}}{}
%%% Local Variables: %%% Local Variables:
%%% mode: latex %%% mode: latex
%%% TeX-master: "manual" %%% TeX-master: "manual"
......
...@@ -10,6 +10,7 @@ ...@@ -10,6 +10,7 @@
%\usepackage{url} %\usepackage{url}
\usepackage[a4paper,pdftex,colorlinks=true,urlcolor=blue,pdfstartview=FitH]{hyperref} \usepackage[a4paper,pdftex,colorlinks=true,urlcolor=blue,pdfstartview=FitH]{hyperref}
\usepackage{graphicx} \usepackage{graphicx}
\usepackage{listings}
\usepackage{xspace} \usepackage{xspace}
\setulmarginsandblock{30mm}{30mm}{*} \setulmarginsandblock{30mm}{30mm}{*}
......
...@@ -10,7 +10,7 @@ basic set of goals. ...@@ -10,7 +10,7 @@ basic set of goals.
Here is our first \why file, which is the file Here is our first \why file, which is the file
\texttt{examples/hello\_proof.why} of the distribution. \texttt{examples/hello\_proof.why} of the distribution.
\verbatiminput{../examples/hello_proof.why} \lstinputlisting[language=why3]{../examples/hello_proof.why}
Any declaration must occur Any declaration must occur
inside a theory, which is in that example called TheoryProof and inside a theory, which is in that example called TheoryProof and
...@@ -150,9 +150,9 @@ Currently, the GUI does not allow to modify the input file. You must ...@@ -150,9 +150,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 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 change the goal $G_2$ by replacing the first occurrence of true by
false, \eg false, \eg
\begin{verbatim} \begin{why3}
goal G2 : (false -> false) /\ (true \/ false) goal G2 : (false -> false) /\ (true \/ false)
\end{verbatim} \end{why3}
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}. 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] \begin{figure}[tbp]
...@@ -182,8 +182,8 @@ tool bar. ...@@ -182,8 +182,8 @@ tool bar.
Notice that replaying can be done in batch mode, using the Notice that replaying can be done in batch mode, using the
\texttt{why3replayer} tool (see Section~\ref{sec:why3replayer}) For \texttt{why3replayer} tool (see Section~\ref{sec:why3replayer}) For
example, running the replayer on the \texttt{hello\_proof} example is example, running the replayer on the \texttt{hello\_proof} example is
as follows (assuming $G_2$ still is \texttt{(true -> false) /\ (true as follows (assuming $G_2$ still is
\/ false)}). \lstinline{(true -> false) /\ (true \/ false)}).
\begin{verbatim} \begin{verbatim}
$ why3replayer hello_proof $ why3replayer hello_proof
Info: found directory 'hello_proof' for the project Info: found directory 'hello_proof' for the project
......
...@@ -26,7 +26,7 @@ discussed later. ...@@ -26,7 +26,7 @@ discussed later.
\begin{figure} \begin{figure}
\centering \centering
\begin{verbatim} \begin{why3}
theory List theory List
type list 'a = Nil | Cons 'a (list 'a) type list 'a = Nil | Cons 'a (list 'a)
end end
...@@ -57,7 +57,7 @@ theory Sorted ...@@ -57,7 +57,7 @@ theory Sorted
forall x y : int, l : list int. forall x y : int, l : list int.
x <= y -> sorted (Cons y l) -> sorted (Cons x (Cons y l)) x <= y -> sorted (Cons y l) -> sorted (Cons x (Cons y l))
end end
\end{verbatim} \end{why3}
\caption{Example of Why3 text.} \caption{Example of Why3 text.}
\label{fig:tutorial1} \label{fig:tutorial1}
\end{figure} \end{figure}
...@@ -97,15 +97,15 @@ an inductive predicate. Every such definition is a list of clauses: ...@@ -97,15 +97,15 @@ an inductive predicate. Every such definition is a list of clauses:
universally closed implications where the consequent is an instance universally closed implications where the consequent is an instance
of the defined predicate. Moreover, the defined predicate may only of the defined predicate. Moreover, the defined predicate may only
occur in positive positions in the antecedent. For example, a clause: occur in positive positions in the antecedent. For example, a clause:
\begin{verbatim} \begin{why3}
| Sorted_Bad : | Sorted_Bad :
forall x y : int, l : list int. forall x y : int, l : list int.
(sorted (Cons y l) -> y > x) -> sorted (Cons x (Cons y l)) (sorted (Cons y l) -> y > x) -> sorted (Cons x (Cons y l))
\end{verbatim} \end{why3}
would not be allowed. This positivity condition assures the logical would not be allowed. This positivity condition assures the logical
soundness of an inductive definition. soundness of an inductive definition.
Note that the type signature of \texttt{sorted} predicate does not Note that the type signature of \lstinline{sorted} predicate does not
include the name of a parameter (see \texttt{l} in the definition include the name of a parameter (see \texttt{l} in the definition
of \texttt{length}): it is unused and therefore optional. of \texttt{length}): it is unused and therefore optional.
...@@ -120,7 +120,7 @@ abstract (\emph{i.e.}~declared but not defined) symbols. ...@@ -120,7 +120,7 @@ abstract (\emph{i.e.}~declared but not defined) symbols.
\begin{figure} \begin{figure}
\centering \centering
\begin{verbatim} \begin{why3}
theory Order theory Order
type t type t
predicate (<=) t t predicate (<=) t t
...@@ -148,7 +148,7 @@ theory SortedIntList ...@@ -148,7 +148,7 @@ theory SortedIntList
use import int.Int use import int.Int
clone SortedGen with type O.t = int, predicate O.(<=) = (<=) clone SortedGen with type O.t = int, predicate O.(<=) = (<=)
end end
\end{verbatim} \end{why3}
\caption{Example of Why3 text (continued).} \caption{Example of Why3 text (continued).}
\label{fig:tutorial2} \label{fig:tutorial2}
\end{figure} \end{figure}
...@@ -228,7 +228,7 @@ we can launch the following command: ...@@ -228,7 +228,7 @@ we can launch the following command:
> why3 lists.why -T SortedIntList > why3 lists.why -T SortedIntList
\end{verbatim} \end{verbatim}
to see the resulting theory \texttt{SortedIntList}: to see the resulting theory \texttt{SortedIntList}:
\begin{verbatim} \begin{why3}
theory SortedIntList theory SortedIntList
(* use BuiltIn *) (* use BuiltIn *)
(* use Int *) (* use Int *)
...@@ -255,7 +255,7 @@ theory SortedIntList ...@@ -255,7 +255,7 @@ theory SortedIntList
prop Le_trans2 = Le_trans, prop Le_asym2 = Le_asym, prop Le_trans2 = Le_trans, prop Le_asym2 = Le_asym,
prop Le_refl2 = Le_refl *) prop Le_refl2 = Le_refl *)
end end
\end{verbatim} \end{why3}
In conclusion, let us briefly explain the concept of namespaces In conclusion, let us briefly explain the concept of namespaces
in \why. Both \texttt{use} and \texttt{clone} instructions can in \why. Both \texttt{use} and \texttt{clone} instructions can
...@@ -286,11 +286,11 @@ would be \texttt{T.$s$}. ...@@ -286,11 +286,11 @@ would be \texttt{T.$s$}.
\why allows to open new namespaces explicitly in the text. In particular, \why allows to open new namespaces explicitly in the text. In particular,
the instruction ``\texttt{clone import Order as O}'' can be equivalently the instruction ``\texttt{clone import Order as O}'' can be equivalently
written as: written as:
\begin{verbatim} \begin{why3}
namespace import O namespace import O
clone export Order clone export Order
end end
\end{verbatim} \end{why3}
However, since \why favours short theories over long and complex ones, However, since \why favours short theories over long and complex ones,
this feature is rarely used. this feature is rarely used.
...@@ -343,7 +343,7 @@ We start by introducing a general-purpose theory defining the notion ...@@ -343,7 +343,7 @@ We start by introducing a general-purpose theory defining the notion
of \emph{bijection}, as two abstract types together with two functions from of \emph{bijection}, as two abstract types together with two functions from
one to the other and two axioms stating that these functions are one to the other and two axioms stating that these functions are
inverse of each other. inverse of each other.
\begin{verbatim} \begin{why3}
theory Bijection theory Bijection
type t type t
type u type u
...@@ -354,45 +354,45 @@ theory Bijection ...@@ -354,45 +354,45 @@ theory Bijection
axiom To_of : forall x : t. to (of x) = x axiom To_of : forall x : t. to (of x) = x
axiom Of_to : forall y : u. of (to y) = y axiom Of_to : forall y : u. of (to y) = y
end end
\end{verbatim} \end{why3}
We now start a new theory, \texttt{Einstein}, which will contain all We now start a new theory, \texttt{Einstein}, which will contain all
the individuals of the problem. the individuals of the problem.
\begin{verbatim} \begin{why3}
theory Einstein "Einstein's problem" theory Einstein "Einstein's problem"
\end{verbatim} \end{why3}
First we introduce enumeration types for houses, colors, persons, First we introduce enumeration types for houses, colors, persons,
drinks, cigars and pets. drinks, cigars and pets.
\begin{verbatim} \begin{why3}
type house = H1 | H2 | H3 | H4 | H5 type house = H1 | H2 | H3 | H4 | H5
type color = Blue | Green | Red | White | Yellow type color = Blue | Green | Red | White | Yellow
type person = Dane | Englishman | German | Norwegian | Swede type person = Dane | Englishman | German | Norwegian | Swede
type drink = Beer | Coffee | Milk | Tea | Water type drink = Beer | Coffee | Milk | Tea | Water
type cigar = Blend | BlueMaster | Dunhill | PallMall | Prince type cigar = Blend | BlueMaster | Dunhill | PallMall | Prince
type pet = Birds | Cats | Dogs | Fish | Horse type pet = Birds | Cats | Dogs | Fish | Horse
\end{verbatim} \end{why3}
We now express that each house is associated bijectively to a color, We now express that each house is associated bijectively to a color,
by cloning the \texttt{Bijection} theory appropriately. by cloning the \texttt{Bijection} theory appropriately.
\begin{verbatim} \begin{why3}
clone Bijection as Color with type t = house, type u = color clone Bijection as Color with type t = house, type u = color
\end{verbatim} \end{why3}
It introduces two functions, namely \texttt{Color.of} and It introduces two functions, namely \texttt{Color.of} and
\texttt{Color.to}, from houses to colors and colors to houses, \texttt{Color.to}, from houses to colors and colors to houses,
respectively, and the two axioms relating them. respectively, and the two axioms relating them.
Similarly, we express that each house is associated bijectively to a Similarly, we express that each house is associated bijectively to a
person person
\begin{verbatim} \begin{why3}
clone Bijection as Owner with type t = house, type u = person clone Bijection as Owner with type t = house, type u = person
\end{verbatim} \end{why3}
and that drinks, cigars and pets are all associated bijectively to persons: and that drinks, cigars and pets are all associated bijectively to persons:
\begin{verbatim} \begin{why3}
clone Bijection as Drink with type t = person, type u = drink 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 Cigar with type t = person, type u = cigar
clone Bijection as Pet with type t = person, type u = pet clone Bijection as Pet with type t = person, type u = pet
\end{verbatim} \end{why3}
Next we need a way to state that a person lives next to another. We Next we need a way to state that a person lives next to another. We
first define a predicate \texttt{leftof} over two houses. first define a predicate \texttt{leftof} over two houses.
\begin{verbatim} \begin{why3}
predicate leftof (h1 h2 : house) = predicate leftof (h1 h2 : house) =
match h1, h2 with match h1, h2 with
| H1, H2 | H1, H2
...@@ -401,49 +401,49 @@ first define a predicate \texttt{leftof} over two houses. ...@@ -401,49 +401,49 @@ first define a predicate \texttt{leftof} over two houses.
| H4, H5 -> true | H4, H5 -> true
| _ -> false | _ -> false
end end
\end{verbatim} \end{why3}
Note how we advantageously used pattern matching, with an or-pattern Note how we advantageously used pattern matching, with an or-pattern
for the four positive cases and a universal pattern for the remaining for the four positive cases and a universal pattern for the remaining
21 cases. It is then immediate to define a \texttt{neighbour} 21 cases. It is then immediate to define a \texttt{neighbour}
predicate over two houses, which completes theory \texttt{Einstein}. predicate over two houses, which completes theory \texttt{Einstein}.
\begin{verbatim} \begin{why3}
predicate rightof (h1 h2 : house) = predicate rightof (h1 h2 : house) =
leftof h2 h1 leftof h2 h1
predicate neighbour (h1 h2 : house) = predicate neighbour (h1 h2 : house) =
leftof h1 h2 \/ rightof h1 h2 leftof h1 h2 \/ rightof h1 h2
end end
\end{verbatim} \end{why3}
The next theory contains the 15 hypotheses. It starts by importing The next theory contains the 15 hypotheses. It starts by importing
theory \texttt{Einstein}. theory \texttt{Einstein}.
\begin{verbatim} \begin{why3}
theory EinsteinHints "Hints" theory EinsteinHints "Hints"
use import Einstein use import Einstein
\end{verbatim} \end{why3}
Then each hypothesis is stated in terms of \texttt{to} and \texttt{of} Then each hypothesis is stated in terms of \texttt{to} and \texttt{of}
functions. For instance, the hypothesis ``The Englishman lives in a functions. For instance, the hypothesis ``The Englishman lives in a
red house'' is declared as the following axiom. red house'' is declared as the following axiom.
\begin{verbatim} \begin{why3}
axiom Hint1: Color.of (Owner.to Englishman) = Red axiom Hint1: Color.of (Owner.to Englishman) = Red
\end{verbatim} \end{why3}
And so on for all other hypotheses, up to And so on for all other hypotheses, up to
``The man who smokes Blends has a neighbour who drinks water'', which completes ``The man who smokes Blends has a neighbour who drinks water'', which completes
this theory. this theory.
\begin{verbatim} \begin{why3}
... ...
axiom Hint15: axiom Hint15:
neighbour (Owner.to (Cigar.to Blend)) (Owner.to (Drink.to Water)) neighbour (Owner.to (Cigar.to Blend)) (Owner.to (Drink.to Water))
end end
\end{verbatim} \end{why3}
Finally, we declare the goal in the fourth theory: Finally, we declare the goal in the fourth theory:
\begin{verbatim} \begin{why3}
theory Problem "Goal of Einstein's problem" theory Problem "Goal of Einstein's problem"
use import Einstein use import Einstein
use import EinsteinHints use import EinsteinHints
goal G: Pet.to Fish = German goal G: Pet.to Fish = German
end end
\end{verbatim} \end{why3}
and we are ready to use \why to discharge this goal with any prover and we are ready to use \why to discharge this goal with any prover
of our choice. of our choice.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment