starting.tex 11.9 KB
 MARCHE Claude committed Dec 14, 2010 1 \chapter{Getting Started}  MARCHE Claude committed Dec 15, 2010 2 \label{chap:starting}  MARCHE Claude committed Dec 14, 2010 3   MARCHE Claude committed Dec 15, 2010 4 5 \section{Hello Proofs}  Guillaume Melquiond committed Jul 18, 2012 6 7 8 The first step in using \why is to write a suitable input file. When one wants to learn a programming language, one starts by writing a basic program. Here is our first \why file, which is the file  Andrei Paskevich committed Jan 30, 2013 9 10 11 \texttt{examples/logic/hello\_proof.why} of the distribution. It contains a small set of goals. \lstinputlisting[language=why3]{../examples/logic/hello_proof.why}  Andrei Paskevich committed Dec 20, 2010 12 13  Any declaration must occur  Guillaume Melquiond committed Jul 18, 2012 14 inside a theory, which is in that example called HelloProof and  Guillaume Melquiond committed Oct 11, 2012 15 labeled with a comment inside double quotes. It contains three goals  MARCHE Claude committed Dec 15, 2010 16 17 named $G_1,G_2,G_3$. The first two are basic propositional goals, whereas the third involves some integer arithmetic, and thus it  MARCHE Claude committed Jul 02, 2011 18 requires to import the theory of integer arithmetic from the \why  MARCHE Claude committed Dec 15, 2010 19 20 21 22 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,  MARCHE Claude committed Jul 02, 2011 23 we show how this file is handled in the \why GUI  MARCHE Claude committed Dec 15, 2010 24 (Section~\ref{sec:gui}) then in batch mode using the \texttt{why3}  Andrei Paskevich committed Jun 30, 2011 25 executable (Section~\ref{sec:batch}).  MARCHE Claude committed Dec 15, 2010 26 27 28 29  \section{Getting Started with the GUI} \label{sec:gui}  MARCHE Claude committed Dec 14, 2010 30 31 32 33 34 35  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 committed Dec 15, 2010 36 \begin{figure}[tbp]  Guillaume Melquiond committed Oct 11, 2012 37 %HEVEA\centering  MARCHE Claude committed Jul 03, 2011 38  \includegraphics[width=\textwidth]{gui-0-70-1.png}  MARCHE Claude committed Dec 15, 2010 39 40 41 42 43 44 45 46 47  \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 committed Jul 04, 2011 48 which looks like the screenshot of Figure~\ref{fig:gui1}.  MARCHE Claude committed Jul 03, 2011 49 50 51 52 53 54 55 56 57 58  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 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}. The middle part is a tree view that  MARCHE Claude committed Jul 04, 2011 59 allows to browse inside the theories.  MARCHE Claude committed Jul 03, 2011 60 61 62 63 64 % Initially, the item of this tree % are closed. We can expand this view using the menu \textsf{View/Expand % all} or its shortcut \textsf{Ctrl-E}. This will result is something % like the screenshot of Figure~\ref{fig:gui2}. In this tree view, we have a structured view of the file: this file  Guillaume Melquiond committed Oct 11, 2012 65 contains one theory, itself containing three goals.  MARCHE Claude committed Jul 03, 2011 66   MARCHE Claude committed Dec 15, 2010 67 68  \begin{figure}[tbp]  Guillaume Melquiond committed Oct 11, 2012 69 %HEVEA\centering  MARCHE Claude committed Jul 03, 2011 70 71  \includegraphics[width=\textwidth]{gui-0-70-2.png} \caption{The GUI with goal G1 selected}  MARCHE Claude committed Dec 15, 2010 72 73  \label{fig:gui2} \end{figure}  MARCHE Claude committed Jul 03, 2011 74 In Figure~\ref{fig:gui2}, we clicked on the row corresponding to  MARCHE Claude committed Dec 15, 2010 75 76 77 78 79 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.  MARCHE Claude committed Dec 15, 2010 80 81 \subsection{Calling provers on goals}  MARCHE Claude committed Dec 15, 2010 82 83 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  Andrei Paskevich committed Dec 20, 2010 84 in the tree view. You can select several goals at a time, either  MARCHE Claude committed Dec 15, 2010 85 86 87 88 89 90 91 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]  Guillaume Melquiond committed Oct 11, 2012 92 %HEVEA\centering  MARCHE Claude committed Jul 03, 2011 93 \includegraphics[width=\textwidth]{gui-0-70-3.png}  MARCHE Claude committed Dec 15, 2010 94 95 96 97  \caption{The GUI after Simplify prover is run on each goal} \label{fig:gui3} \end{figure}  MARCHE Claude committed Jul 03, 2011 98 99 100 101 The goal $G_1$ is now marked with a 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 are not proved, they remain marked with an orange question mark.  MARCHE Claude committed Dec 15, 2010 102 103 104  You can immediately attempt to prove the remaining goals using another prover, {\eg} Alt-Ergo, by clicking on the corresponding button. The  Andrei Paskevich committed Jun 30, 2011 105 goal $G_3$ should be proved now, but not $G_2$.  MARCHE Claude committed Dec 15, 2010 106 107 108 109 110 111 112  \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 committed Dec 15, 2010 113 have two subgoals, and you can try again a prover on them, for example  MARCHE Claude committed Jul 03, 2011 114 115 Simplify. We already have a lot of goals and proof attempts, so it is a good idea to close the sub-trees which are already proved: this can be done by the menu \textsf{View/Collapse proved goals}, or even better by its shortcut Ctrl-C''. You should see now what is displayed on Figure~\ref{fig:gui4}.  MARCHE Claude committed Dec 15, 2010 116 117  \begin{figure}[tbp]  Guillaume Melquiond committed Oct 11, 2012 118 %HEVEA\centering  MARCHE Claude committed Jul 03, 2011 119 120  \includegraphics[width=\textwidth]{gui-0-70-4.png} \caption{The GUI after splitting goal $G_2$ and collapsing proved goals}  MARCHE Claude committed Dec 15, 2010 121 122 123 124 125  \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 committed Dec 15, 2010 126 the \textsf{Coq} button. A new sub-row appear for Coq, and  MARCHE Claude committed Dec 15, 2010 127 128 129 130 131 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  MARCHE Claude committed Jul 03, 2011 132 now a regular Coq file to fill in, as shown on Figure~\ref{fig:coqide}.  MARCHE Claude committed Dec 15, 2010 133 134 Please take care of the comments of this file. Only the part between the two last comments can be modified. Moreover, these comments  Jean-Christophe Filliâtre committed Feb 17, 2011 135 themselves should not be modified at all, they are used to mark the  MARCHE Claude committed Dec 15, 2010 136 part you modify, in order to regenerate the file if the goal is  Andrei Paskevich committed Jun 30, 2011 137 changed.  MARCHE Claude committed Dec 15, 2010 138 139  \begin{figure}[tbp]  Guillaume Melquiond committed Oct 11, 2012 140 %HEVEA\centering  MARCHE Claude committed Jul 03, 2011 141  \includegraphics[width=\textwidth]{coqide-0-70.png}  MARCHE Claude committed Dec 15, 2010 142 143 144 145 146 147 148 149 150 151 152  \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 committed Jul 03, 2011 153 154 155 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  156 \begin{whycode}  Andrei Paskevich committed Jun 30, 2011 157  goal G2 : (false -> false) /\ (true \/ false)  158 \end{whycode}  MARCHE Claude committed Jul 03, 2011 159 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}.  MARCHE Claude committed Dec 15, 2010 160 161  \begin{figure}[tbp]  Guillaume Melquiond committed Oct 11, 2012 162 %HEVEA\centering  MARCHE Claude committed Jul 03, 2011 163 164  \includegraphics[width=\textwidth]{gui-0-70-5.png} \caption{File reloaded after modifying goal $G_2$}  MARCHE Claude committed Dec 15, 2010 165 166 167 168  \label{fig:gui5} \end{figure} The important feature to notice first is that all the previous proof  MARCHE Claude committed Jul 03, 2011 169 170 171 172 attempts and transformations were saved in a database --- an XML file created when the \why file was opened in the GUI for the first time. Then, for all the goals that remain unchanged, the previous proofs are shown again. For the parts that changed, the previous  Guillaume Melquiond committed Oct 30, 2012 173 proofs attempts are shown but marked with (obsolete)''\index{obsolete!proof attempt}  174 so that you  MARCHE Claude committed Jul 03, 2011 175 know the results are not accurate. You can now retry to prove all what  MARCHE Claude committed Jul 04, 2011 176 177 178 179 180 remains unproved using any of the provers. \subsection{Replaying obsolete proofs} Instead of pushing a prover's button to rerun its proofs, you can  MARCHE Claude committed Aug 24, 2012 181 \emph{replay} the existing but obsolete  182 proof attempts, by clicking on  MARCHE Claude committed Jul 04, 2011 183 184 185 186 187 188 189 190 the \textsf{Replay} button. By default, \textsf{Replay} only replays proofs that were successful before. If you want to replay all of them, you must select the context \textsf{all goals} at the top of the left tool bar. Notice that replaying can be done in batch mode, using the \texttt{why3replayer} tool (see Section~\ref{sec:why3replayer}) For example, running the replayer on the \texttt{hello\_proof} example is  Jean-Christophe Filliâtre committed Apr 20, 2012 191 as follows (assuming $G_2$ still is  Guillaume Melquiond committed Oct 11, 2012 192 \lstinline|(true -> false) /\ (true \/ false)|).  MARCHE Claude committed Jul 04, 2011 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 \begin{verbatim} $why3replayer hello_proof Info: found directory 'hello_proof' for the project Opening session...[Xml warning] prolog ignored [Reload] file '../hello_proof.why' [Reload] theory 'HelloProof' [Reload] transformation split_goal for goal G2 done Progress: 9/9 2/3 +--file ../hello_proof.why: 2/3 +--theory HelloProof: 2/3 +--goal G2 not proved Everything OK. \end{verbatim} The last line tells us that no difference was detected between the current run and the informations in the XML file. The tree above reminds us that the G2 is not proved.  MARCHE Claude committed Jul 03, 2011 211 212 213  \subsection{Cleaning}  MARCHE Claude committed Jul 04, 2011 214 215 216 217 218 219 You may want to clean some the proof attempts, \eg removing the unsuccessful ones when a project is finally fully proved. A proof or a transformation can be removed by selecting it and clicking on button \textsf{Remove}. You must confirm the removal. Beware that there is no way to undo such a removal.  MARCHE Claude committed Jul 03, 2011 220   MARCHE Claude committed Jul 04, 2011 221 222 223 The \textsf{Clean} button performs an automatic removal of all proofs attempts that are unsuccessful, while there exists a successful proof attempt for the same goal.  MARCHE Claude committed Dec 15, 2010 224   MARCHE Claude committed Jul 02, 2011 225 \section{Getting Started with the \why Command}  MARCHE Claude committed Dec 15, 2010 226 227 228 229 230 \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 committed Dec 15, 2010 231 232 233 description of this tool and all its command-line options. The very first time you want to use Why, you should proceed with  Andrei Paskevich committed Dec 20, 2010 234 autodetection of external provers. We have already seen how to do  MARCHE Claude committed Jul 02, 2011 235 it in the \why GUI. On the command line, this is done as follows  Andrei Paskevich committed Dec 20, 2010 236 (here \texttt{>}'' is the prompt):  MARCHE Claude committed Dec 15, 2010 237 \begin{verbatim}  Jean-Christophe Filliâtre committed Feb 15, 2011 238 > why3config --detect  MARCHE Claude committed Dec 15, 2010 239 240 \end{verbatim} This prints some information messages on what detections are attempted. To know which  Andrei Paskevich committed Dec 20, 2010 241 provers have been successfully detected, you can do as follows.  MARCHE Claude committed Dec 15, 2010 242 243 244 245 246 247 248 249 250 \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  Andrei Paskevich committed Jun 30, 2011 251 Simplify~\cite{simplify05}.  MARCHE Claude committed Dec 15, 2010 252 253 254  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  Andrei Paskevich committed Dec 20, 2010 255 256 \verb|-P| option is followed by the unique prover identifier (as shown by \texttt{--list-provers} option).  MARCHE Claude committed Dec 15, 2010 257 258 259 260 261 262 \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}  Andrei Paskevich committed Dec 20, 2010 263 264 Unlike \why GUI, the command-line tool does not save the proof attempts or applied transformations in a database.  MARCHE Claude committed Dec 15, 2010 265   Andrei Paskevich committed Dec 20, 2010 266 We can also specify which goal or goals to prove. This is done by giving  MARCHE Claude committed Dec 15, 2010 267 first a theory identifier, then goal identifier(s). Here is the way to  MARCHE Claude committed Dec 16, 2010 268 call Alt-Ergo on goals$G_2$and$G_3$.  MARCHE Claude committed Dec 15, 2010 269 270 271 272 273 \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 committed Dec 15, 2010 274   MARCHE Claude committed Dec 15, 2010 275 Finally, a transformation to apply to goals before proving them can be  MARCHE Claude committed Dec 16, 2010 276 specified. To know the unique identifier associated to  Andrei Paskevich committed Dec 20, 2010 277 a transformation, do as follows.  MARCHE Claude committed Dec 15, 2010 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 \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 committed Dec 15, 2010 297   MARCHE Claude committed Dec 14, 2010 298 299 300 301 302 %%% Local Variables: %%% mode: latex %%% TeX-PDF-mode: t %%% TeX-master: "manual" %%% End: