starting.tex 10 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1
\chapter{Getting Started}
MARCHE Claude's avatar
MARCHE Claude committed
2
\label{chap:starting}
MARCHE Claude's avatar
MARCHE Claude committed
3

MARCHE Claude's avatar
MARCHE Claude committed
4
5
\section{Hello Proofs}

6
The first and basic step in using \why\ is to write a suitable input
MARCHE Claude's avatar
MARCHE Claude committed
7
8
9
10
file. When one wants to learn a programming language, you start by
writing a basic program. Here we start by writing a file containing a
basic set of goals. 

11
Here is our first \why\ file, which is the file
MARCHE Claude's avatar
MARCHE Claude committed
12
\texttt{examples/hello\_proof.why} of the distribution.
13
14
15
\verbatiminput{../examples/hello_proof.why}

Any declaration must occur
MARCHE Claude's avatar
MARCHE Claude committed
16
17
18
19
inside a theory, which is in that example called TheoryProof and
labelled with a comment inside double quotes. It contains three goals
named $G_1,G_2,G_3$. The first two are basic propositional goals,
whereas the third involves some integer arithmetic, and thus it
20
requires to import the theory of integer arithmetic from the \why\
MARCHE Claude's avatar
MARCHE Claude committed
21
22
23
24
standard library, which is done by the \texttt{use} declaration above.

We don't give more details here about the syntax and refer to
Chapter~\ref{chap:syntax} for detailed explanations. In the following,
25
we show how this file is handled in the \why\ GUI
MARCHE Claude's avatar
MARCHE Claude committed
26
(Section~\ref{sec:gui}) then in batch mode using the \texttt{why3}
27
executable (Section~\ref{sec:batch}). 
MARCHE Claude's avatar
MARCHE Claude committed
28
29
30
31


\section{Getting Started with the GUI}
\label{sec:gui}
MARCHE Claude's avatar
MARCHE Claude committed
32
33
34
35
36
37

The graphical interface allows to browse into a file or a set of
files, and check the validity of goals with external provers, in a
friendly way. This section presents the basic use of this GUI. Please
refer to Section~\ref{sec:ideref} for a more complete description.

MARCHE Claude's avatar
MARCHE Claude committed
38
39
40
41
42
43
44
45
46
47
48
\begin{figure}[tbp]
  \includegraphics[width=\textwidth]{gui1.png}
  \caption{The GUI when started the very first time}
  \label{fig:gui1}
\end{figure}

The GUI is launched on the file above as follows.
\begin{verbatim}
why3ide hello_proof.why
\end{verbatim}
When the GUI is started for the first time, you should get a window
MARCHE Claude's avatar
MARCHE Claude committed
49
which looks like the screenshot of Figure~\ref{fig:gui1}. First of
50
all, the left column is a tool bar which provides different actions to
MARCHE Claude's avatar
MARCHE Claude committed
51
apply on goals. In this case, the section ``Provers'' is empty, which
52
means that you have not performed prover detection yet. You should do it
MARCHE Claude's avatar
MARCHE Claude committed
53
54
now using the menu \textsf{File/Detect provers}. Second, the middle
part is a tree view that allows to browse inside the
55
theories. Initially, the item of this tree are closed. We can
MARCHE Claude's avatar
MARCHE Claude committed
56
expand this view using the menu \textsf{View/Expand all} or its
57
shortcut \textsf{Ctrl-E}. This will result is something like the
MARCHE Claude's avatar
MARCHE Claude committed
58
screenshot of Figure~\ref{fig:gui2}.
MARCHE Claude's avatar
MARCHE Claude committed
59
60
61
62
63
64
65
66
67
68
69
70
71
72

\begin{figure}[tbp]
  \includegraphics[width=\textwidth]{gui2.png}
  \caption{The GUI with provers detected and tree view expanded}
  \label{fig:gui2}
\end{figure}

In the tree view, we have now a strctured view of the file: this file
contains one theory, itself containg three goals. In
Figure~\ref{fig:gui2}, we also clicked on the row corresponding to
goal $G_1$. The \emph{task} associated with this goal is then
displayed on the top right, and the corresponding part of the input
file is shown on the bottom right part.

73
74
Notice also that three provers were detected, and are now shown
in the ``provers'' section of the left toolbar. In this example,
MARCHE Claude's avatar
MARCHE Claude committed
75
76
77
detected provers are Alt-Ergo~\cite{ergo}, Coq~\cite{CoqArt} and
Simplify~\cite{simplify05}. 

78
79
\subsection{Calling provers on goals}

MARCHE Claude's avatar
MARCHE Claude committed
80
81
You are now ready to call these provers on the goals. Whenever you
click on a prover button, this prover is called on the goal selected
82
in the tree view. You can select several goals at a time, either
MARCHE Claude's avatar
MARCHE Claude committed
83
84
85
86
87
88
89
90
91
92
93
94
by using multi-selection (typically by clicking while pressing the
\textsf{Shift} or \textsf{Ctrl} key) or by selecting the parent theory
or the parent file. Let us now select the theory ``HelloProof'' and
click on the \textsf{Simplify} button. After a short time, you should
get the display of Figure~\ref{fig:gui3}.

\begin{figure}[tbp]
  \includegraphics[width=\textwidth]{gui3.png}
  \caption{The GUI after Simplify prover is run on each goal}
  \label{fig:gui3}
\end{figure}

95
96
97
The row corresponding to goal $G_1$ is now closed, and marked with
green ``checked'' icon in the status column. This means that the goal
is proved by the Simplify prover. On the contrary, the two other goals
MARCHE Claude's avatar
MARCHE Claude committed
98
are not proved, they are marked with an orange question mark.
99
100
101
102
103
104
105
106
107
108
109

You can immediately attempt to prove the remaining goals using another
prover, {\eg} Alt-Ergo, by clicking on the corresponding button. The
goal $G_3$ should be proved now, but not $G_2$. 

\subsection{Applying transformations}

Instead of calling a prover on a goal, you can apply a transformation
to it.  Since $G_2$ is a conjunction, a possibility is to split it
into subgoals. You can do that by clicking on the \textsf{Split}
button of section ``Transformations'' of the left toolbar. Now you
MARCHE Claude's avatar
MARCHE Claude committed
110
have two subgoals, and you can try again a prover on them, for example
111
112
113
114
115
116
117
118
119
120
121
Simplify. Assuming we expand everything again, you should see now what
is displayed on Figure~\ref{fig:gui4}.

\begin{figure}[tbp]
  \includegraphics[width=\textwidth]{gui4.png}
  \caption{The GUI after splitting goal $G_2$}
  \label{fig:gui4}
\end{figure}

The first part of goal $G_2$ is still unproved. As a last resort, we
can try to call the Coq proof assistant. The first step is to click on
MARCHE Claude's avatar
MARCHE Claude committed
122
the \textsf{Coq} button. A new sub-row appear for Coq, and
123
124
125
126
127
128
129
130
unsurprisingly the goal is not proved by Coq either. What can be done
now is editing the proof: select that row and then click on the
\textsf{Edit} button in section ``Tools'' of the toolbar. This should
launch the Coq proof editor, which is \texttt{coqide} by default (see
Section~\ref{sec:ideref} for details on how to configure this). You get
now a regular Coq file fo fill in, as shown on Figure~\ref{fig:coqide}.
Please take care of the comments of this file. Only the part between
the two last comments can be modified. Moreover, these comments
131
themselves should not be modified at all, they are used to mark the
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
part you modify, in order to regenerate the file if the goal is
changed. 

\begin{figure}[tbp]
  \includegraphics[width=\textwidth]{coqide.png}
  \caption{CoqIDE on subgoal 1 of $G_2$}
  \label{fig:coqide}
\end{figure}

Of course, in that particular case, the goal cannot be proved since it
is not valid. The only thing to do is to fix the input file, as
explained below.

\subsection{Modifying the input}

Currently, the GUI does not allow to modify the input file. You must
MARCHE Claude's avatar
MARCHE Claude committed
148
exit the GUI and modify the file 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
149
150
151
152
153
154
155
156
157
158
159
160
161
\begin{verbatim}
  goal G2 : (false -> false) and (true or false)
\end{verbatim}
Starting the IDE on the modified file and expanding everything with
\textsf{Ctrl-E}, we get the tree view shown on Figure~\ref{fig:gui5}.

\begin{figure}[tbp]
  \includegraphics[width=\textwidth]{gui5.png}
  \caption{The GUI restarted after modifying goal $G_2$}
  \label{fig:gui5}
\end{figure}

The important feature to notice first is that all the previous proof
162
163
164
attempts and transformations were saved in a database --- an SQLite3
file created when the \why\ file was opened in the GUI for the first
time. Then, for
165
166
167
168
all the goals that remain unchanged, the previous proofs are shown
again. For the parts that changed, the previous proofs attempts are
shown but marked with "(obsolete)" so that you know the results are
not accurate. You can now retry to prove all what remains unproved
169
using any of the provers, using the button ``Replay''.
170

171
\section{Getting Started with the \why\ Command}
MARCHE Claude's avatar
MARCHE Claude committed
172
173
174
175
176
\label{sec:batch}

The why3 command allows to check the validity of goals with external
provers, in batch mode. This section presents the basic use of this
tool. Refer to Section~\ref{sec:why3ref} for a more complete
MARCHE Claude's avatar
MARCHE Claude committed
177
178
179
description of this tool and all its command-line options.

The very first time you want to use Why, you should proceed with
180
181
182
autodetection of external provers. We have already seen how to do
it in the \why\ GUI. On the command line, this is done as follows
(here ``\texttt{>}'' is the prompt):
MARCHE Claude's avatar
MARCHE Claude committed
183
\begin{verbatim}
184
> why3config --detect
MARCHE Claude's avatar
MARCHE Claude committed
185
186
\end{verbatim}
This prints some information messages on what detections are attempted. To know which
187
provers have been successfully detected, you can do as follows.
MARCHE Claude's avatar
MARCHE Claude committed
188
189
190
191
192
193
194
195
196
197
198
199
200
\begin{verbatim}
> why3 --list-provers
Known provers:
  alt-ergo (Alt-Ergo)
  coq (Coq)
  simplify (Simplify)
\end{verbatim}
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}. 

Let's assume now we want to run Simplify on the HelloProof
example. The command to type and its output are as follows, where the
201
202
\verb|-P| option is followed by the unique prover identifier (as shown
by \texttt{--list-provers} option).
MARCHE Claude's avatar
MARCHE Claude committed
203
204
205
206
207
208
\begin{verbatim}
> why3 -P simplify hello_proof.why
hello_proof.why HelloProof G1 : Valid (0.10s)
hello_proof.why HelloProof G2 : Unknown: Unknown (0.01s)
hello_proof.why HelloProof G3 : Unknown: Unknown (0.00s)
\end{verbatim}
209
210
Unlike \why GUI, the command-line tool does not save the proof attempts
or applied transformations in a database.
MARCHE Claude's avatar
MARCHE Claude committed
211

212
We can also specify which goal or goals to prove. This is done by giving
MARCHE Claude's avatar
MARCHE Claude committed
213
first a theory identifier, then goal identifier(s). Here is the way to
MARCHE Claude's avatar
MARCHE Claude committed
214
call Alt-Ergo on goals $G_2$ and $G_3$.
MARCHE Claude's avatar
MARCHE Claude committed
215
216
217
218
219
\begin{verbatim}
> why3 -P alt-ergo hello_proof.why -T HelloProof -G G2 -G G3
hello_proof.why HelloProof G2 : Unknown: Unknown (0.01s)
hello_proof.why HelloProof G3 : Valid (0.01s)
\end{verbatim}
MARCHE Claude's avatar
MARCHE Claude committed
220

MARCHE Claude's avatar
MARCHE Claude committed
221
Finally, a transformation to apply to goals before proving them can be
222
specified. To know the unique identifier associated to
223
a transformation, do as follows.
MARCHE Claude's avatar
MARCHE Claude committed
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
\begin{verbatim}
> why3 --list-transforms
Known non-splitting transformations:
  [...]

Known splitting transformations:
  [...]
  split_goal
  split_intro
\end{verbatim}
Here is how you can split the goal $G_2$ before calling
Simplify on resulting subgoals.
\begin{verbatim}
> why3 -P simplify hello_proof.why -a split_goal -T HelloProof -G G2
hello_proof.why HelloProof G2 : Unknown: Unknown (0.00s)
hello_proof.why HelloProof G2 : Valid (0.00s)
\end{verbatim}
Section~\ref{sec:transformations} gives the description of the various
transformations available.
MARCHE Claude's avatar
MARCHE Claude committed
243

MARCHE Claude's avatar
MARCHE Claude committed
244
245
246
247
248
%%% Local Variables:
%%% mode: latex
%%% TeX-PDF-mode: t
%%% TeX-master: "manual"
%%% End: