starting.tex 9.96 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}  MARCHE Claude committed Jul 02, 2011 6 The first and basic step in using \why is to write a suitable input  MARCHE Claude committed Dec 15, 2010 7 8 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  Andrei Paskevich committed Jun 30, 2011 9 basic set of goals.  MARCHE Claude committed Dec 15, 2010 10   MARCHE Claude committed Jul 02, 2011 11 Here is our first \why file, which is the file  MARCHE Claude committed Dec 15, 2010 12 \texttt{examples/hello\_proof.why} of the distribution.  Andrei Paskevich committed Dec 20, 2010 13 14 15 \verbatiminput{../examples/hello_proof.why} Any declaration must occur  MARCHE Claude committed Dec 15, 2010 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  MARCHE Claude committed Jul 02, 2011 20 requires to import the theory of integer arithmetic from the \why  MARCHE Claude committed Dec 15, 2010 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,  MARCHE Claude committed Jul 02, 2011 25 we show how this file is handled in the \why GUI  MARCHE Claude committed Dec 15, 2010 26 (Section~\ref{sec:gui}) then in batch mode using the \texttt{why3}  Andrei Paskevich committed Jun 30, 2011 27 executable (Section~\ref{sec:batch}).  MARCHE Claude committed Dec 15, 2010 28 29 30 31  \section{Getting Started with the GUI} \label{sec:gui}  MARCHE Claude committed Dec 14, 2010 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 committed Dec 15, 2010 38 \begin{figure}[tbp]  MARCHE Claude committed Jul 03, 2011 39 \includegraphics[width=\textwidth]{gui-0-70-1.png}  MARCHE Claude committed Dec 15, 2010 40 41 42 43 44 45 46 47 48  \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 03, 2011 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 which 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 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 allows to browse inside the theories. % 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 contains one theory, itself containg three goals.  MARCHE Claude committed Dec 15, 2010 68 69  \begin{figure}[tbp]  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]  MARCHE Claude committed Jul 03, 2011 92 \todo{update \includegraphics[width=\textwidth]{gui3.png}}  MARCHE Claude committed Dec 15, 2010 93 94 95 96  \caption{The GUI after Simplify prover is run on each goal} \label{fig:gui3} \end{figure}  MARCHE Claude committed Dec 15, 2010 97 98 99 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 committed Dec 15, 2010 100 are not proved, they are marked with an orange question mark.  MARCHE Claude committed Dec 15, 2010 101 102 103  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 104 goal $G_3$ should be proved now, but not $G_2$.  MARCHE Claude committed Dec 15, 2010 105 106 107 108 109 110 111  \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 112 have two subgoals, and you can try again a prover on them, for example  MARCHE Claude committed Dec 15, 2010 113 114 115 116 Simplify. Assuming we expand everything again, you should see now what is displayed on Figure~\ref{fig:gui4}. \begin{figure}[tbp]  MARCHE Claude committed Jul 03, 2011 117 \todo{update \includegraphics[width=\textwidth]{gui4.png}}  MARCHE Claude committed Dec 15, 2010 118 119 120 121 122 123  \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 committed Dec 15, 2010 124 the \textsf{Coq} button. A new sub-row appear for Coq, and  MARCHE Claude committed Dec 15, 2010 125 126 127 128 129 130 131 132 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  Jean-Christophe Filliâtre committed Feb 17, 2011 133 themselves should not be modified at all, they are used to mark the  MARCHE Claude committed Dec 15, 2010 134 part you modify, in order to regenerate the file if the goal is  Andrei Paskevich committed Jun 30, 2011 135 changed.  MARCHE Claude committed Dec 15, 2010 136 137  \begin{figure}[tbp]  MARCHE Claude committed Jul 03, 2011 138 \todo{update \includegraphics[width=\textwidth]{coqide.png}}  MARCHE Claude committed Dec 15, 2010 139 140 141 142 143 144 145 146 147 148 149  \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 Dec 15, 2010 150 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  MARCHE Claude committed Dec 15, 2010 151 \begin{verbatim}  Andrei Paskevich committed Jun 30, 2011 152  goal G2 : (false -> false) /\ (true \/ false)  MARCHE Claude committed Dec 15, 2010 153 154 155 156 157 \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]  MARCHE Claude committed Jul 03, 2011 158 \todo{update \includegraphics[width=\textwidth]{gui5.png}}  MARCHE Claude committed Dec 15, 2010 159 160 161 162 163  \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  Andrei Paskevich committed Dec 20, 2010 164 attempts and transformations were saved in a database --- an SQLite3  MARCHE Claude committed Jul 02, 2011 165 file created when the \why file was opened in the GUI for the first  Andrei Paskevich committed Dec 20, 2010 166 time. Then, for  MARCHE Claude committed Dec 15, 2010 167 168 169 170 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  Andrei Paskevich committed Dec 20, 2010 171 using any of the provers, using the button Replay''.  MARCHE Claude committed Dec 15, 2010 172   MARCHE Claude committed Jul 02, 2011 173 \section{Getting Started with the \why Command}  MARCHE Claude committed Dec 15, 2010 174 175 176 177 178 \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 179 180 181 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 182 autodetection of external provers. We have already seen how to do  MARCHE Claude committed Jul 02, 2011 183 it in the \why GUI. On the command line, this is done as follows  Andrei Paskevich committed Dec 20, 2010 184 (here \texttt{>}'' is the prompt):  MARCHE Claude committed Dec 15, 2010 185 \begin{verbatim}  Jean-Christophe Filliâtre committed Feb 15, 2011 186 > why3config --detect  MARCHE Claude committed Dec 15, 2010 187 188 \end{verbatim} This prints some information messages on what detections are attempted. To know which  Andrei Paskevich committed Dec 20, 2010 189 provers have been successfully detected, you can do as follows.  MARCHE Claude committed Dec 15, 2010 190 191 192 193 194 195 196 197 198 \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 199 Simplify~\cite{simplify05}.  MARCHE Claude committed Dec 15, 2010 200 201 202  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 203 204 \verb|-P| option is followed by the unique prover identifier (as shown by \texttt{--list-provers} option).  MARCHE Claude committed Dec 15, 2010 205 206 207 208 209 210 \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 211 212 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 213   Andrei Paskevich committed Dec 20, 2010 214 We can also specify which goal or goals to prove. This is done by giving  MARCHE Claude committed Dec 15, 2010 215 first a theory identifier, then goal identifier(s). Here is the way to  MARCHE Claude committed Dec 16, 2010 216 call Alt-Ergo on goals $G_2$ and $G_3$.  MARCHE Claude committed Dec 15, 2010 217 218 219 220 221 \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 222   MARCHE Claude committed Dec 15, 2010 223 Finally, a transformation to apply to goals before proving them can be  MARCHE Claude committed Dec 16, 2010 224 specified. To know the unique identifier associated to  Andrei Paskevich committed Dec 20, 2010 225 a transformation, do as follows.  MARCHE Claude committed Dec 15, 2010 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 \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 245   MARCHE Claude committed Dec 14, 2010 246 247 248 249 250 %%% Local Variables: %%% mode: latex %%% TeX-PDF-mode: t %%% TeX-master: "manual" %%% End: