pvs.tex 1.9 KB
 MARCHE Claude committed Feb 01, 2014 1 2 3 4 5 6 7 8 9 10 \section{PVS} \label{sec:pvs} \index{PVS proof assistant} \subsection{Installation} You need version 6.0. \subsection{Usage}  MARCHE Claude committed Jul 19, 2012 11 12 13 14 15 16 17 18 19 20 21 22 23 24  When a PVS file is regenerated, the old version is split into chunks, according to blank lines. Chunks corresponding to \why declarations are identified with a comment starting with \verb+% Why3+, \eg \begin{verbatim} % Why3 f f(x: int) : int \end{verbatim} Other chunks are considered to be user PVS declarations. Thus a comment such as \verb+% Why3 f+ must not be removed; otherwise, there will be two declarations for \texttt{f} in the next version of the file (one being regenerated and another one considered to be a user-edited chunk).  MARCHE Claude committed Feb 01, 2014 25 26 \subsection{Realization}  MARCHE Claude committed Jul 19, 2012 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 The user is allowed to perform the following actions on a PVS realization: \begin{itemize} \item give a definition to an uninterpreted symbol (type, function, or predicate symbol), by adding an equal sign (\texttt{=}) and a right-hand side to the definition. When the declaration is regenerated, the left-hand side is updated and the right-hand side is reprinted as is. In particular, the names of a function or predicate arguments should not be modified. In addition, the \texttt{MACRO} keyword may be inserted and it will be kept in further generations. \item turn an axiom into a lemma, that is to replace the PVS keyword \texttt{AXIOM} with either \texttt{LEMMA} or \texttt{THEOREM}. \item insert anything between generated declarations, such as a lemma,  Jean-Christophe Filliâtre committed Dec 11, 2013 43 44 45  an extra definition for the purpose of a proof, an extra \texttt{IMPORTING} command, etc. Do not forget to surround these extra declarations with blank lines.  MARCHE Claude committed Jul 19, 2012 46 \end{itemize}  Jean-Christophe Filliâtre committed Dec 11, 2013 47 48 \why makes some effort to merge new declarations with old ones and with user chunks. If it happens that some chunks could not be  MARCHE Claude committed Jul 19, 2012 49 merged, they are appended at the end of the file, in comments.  MARCHE Claude committed Feb 01, 2014 50 51 52 53 54 55 56  %%% Local Variables: %%% mode: latex %%% TeX-PDF-mode: t %%% TeX-master: "manual" %%% End: