Commit 6673640c authored by MARCHE Claude's avatar MARCHE Claude

doc: done a few todos

parent 51a377d3
......@@ -1397,8 +1397,10 @@ NAME = why3-$(VERSION)
DISTRIB_DIR = distrib/$(NAME)
DISTRIB_TAR = $(DISTRIB_DIR).tar.gz
DISTRIB_FILES = Version Makefile.in configure.in configure AUTHORS \
README CHANGES INSTALL OCAML-LICENSE LICENSE src/config.sh.in \
DISTRIB_FILES = Version Makefile.in configure.in configure \
src/jessie/Makefile.in \
AUTHORS README CHANGES INSTALL OCAML-LICENSE LICENSE \
src/config.sh.in \
src/*.ml* src/*.dep src/*/*.ml* src/*/*.dep src/*/*.c \
plugins/printer/.keepme plugins/*/*.ml* plugins/*/*.dep \
lib/why3/META.in lib/why3/why3.ml \
......
......@@ -144,7 +144,7 @@ Provers support:
Misc:
o improved output of "why3session latex"
(incompatible changes in LaTeX macos)
(incompatible changes in LaTeX macros)
o [replayer] new option -q for running quietly
o a warning is emitted for unused bound logic variables in "forall",
"exists" and "let"
......
......@@ -7,7 +7,7 @@
\cline{2-4}
\quad\transformation{split\_goal} & \multicolumn{3}{|c|}{}\\
\cline{2-4}
\quad\subgoal{G2.1}{1} & \unknown{0.00} & \unknown{0.49} & \unknown{0.00} \\
\quad\subgoal{G2.1}{1} & \unknown{0.00} & \unknown{0.43} & \unknown{0.00} \\
\cline{2-4}
\quad\subgoal{G2.2}{2} & \valid{0.00} & \noresult& \valid{0.00} \\
\hline
......
......@@ -5,7 +5,7 @@
\hline
\explanation{G2} & & \unknown{0.00} & \noresult& \unknown{0.00} \\
\cline{2-4}
& \explanation{G2.1} & \unknown{0.00} & \unknown{0.49} & \unknown{0.00} \\
& \explanation{G2.1} & \unknown{0.00} & \unknown{0.43} & \unknown{0.00} \\
\cline{2-5}
& \explanation{G2.2} & \valid{0.00} & \noresult& \valid{0.00} \\
\hline
......
doc/hello_proof.png

21.8 KB | W: | H:

doc/hello_proof.png

21.4 KB | W: | H:

doc/hello_proof.png
doc/hello_proof.png
doc/hello_proof.png
doc/hello_proof.png
  • 2-up
  • Swipe
  • Onion skin
......@@ -183,7 +183,7 @@ Section~\ref{sec:why3session}.
% pour l'instant on ne documente pas
% \todo{que devient l'option -to-known-prover de why3session ?
% {que devient l'option -to-known-prover de why3session ?
% (d'ailleurs documenté en tant que --convert-unknown ??) Pourrait-on
% permettre à why3session d'appliquer les choix d'association
% vieux-prover/nouveau-prouveur stockés par l'IDE ?}
......
......@@ -260,11 +260,11 @@ session. If you modify the original file (.why, .mlw) or if the
transformations have changed (new version of why3) why3 will detect
that. The provers will perhaps answer differently on this new
problems. So the proof attempts that corresponds to a goal that
changed are marked obsolete.
changed are marked obsolete.
% non
% non
% We say that a session is obsolete if new
% goals are made obsolete by this method during start-up.
% goals are made obsolete by this method during start-up.
% Claude: Alors la je ne vois pas pourquoi
% A session can
......@@ -348,7 +348,7 @@ A copy of the tools already available in the left toolbar, plus:
transformations, as listed in Section~\ref{sec:transformations}
\item[Apply non-splitting transformation]. Same as above, but for
splitting transformations, \emph{i.e.} those that can generated
several sub-goals.
several sub-goals.
\end{description}
\item[Menu \textsf{Help}]
......@@ -531,7 +531,7 @@ file is fully proved, the subtree is not shown.
When some proof attempts stored in the session file are
obsolete\index{obsolete!proof attempt},
the replay is run anyway, as with the replay button in the IDE. Then, the session
file will be updated if both
file will be updated if both
\begin{itemize}
\item all the replayed proof attempts give the same result as what
is stored in the session
......@@ -695,15 +695,15 @@ For example, here are the session tree produced on the ``hello
proof'' example of Section~\ref{chap:starting}.
{\scriptsize
\begin{verbatim}
hello_proof---../hello_proof.why?---HelloProof?-+-G3-+-Alt-Ergo (0.93)
| `-Simplify (1.5.4)?
|-G2?-+-split_goal?-+-G2.1-+-Alt-Ergo (0.93)
| | | `-Simplify (1.5.4)
| | `-G2.0?-+-Alt-Ergo (0.93)?
hello_proof---../hello_proof.why?---HelloProof?-+-G3-+-Simplify (1.5.4)?
| `-Alt-Ergo (0.94)
|-G2?-+-split_goal?-+-G2.2-+-Simplify (1.5.4)
| | | `-Alt-Ergo (0.94)
| | `-G2.1?-+-Coq (8.3pl4)?
| | |-Simplify (1.5.4)?
| | `-Coq (8.3pl3)?
| |-Alt-Ergo (0.93)?
| `-Simplify (1.5.4)?
| | `-Alt-Ergo (0.94)?
| |-Simplify (1.5.4)?
| `-Alt-Ergo (0.94)?
`-G1---Simplify (1.5.4)
\end{verbatim}
}
......@@ -740,17 +740,18 @@ proof'' example of Section~\ref{chap:starting}.
+-- theory HelloProof
+-- goal G2
+-- transformation split_goal
+-- goal G2.0
+-- goal G2.1
== Goals proved by only one prover ==
+-- file ../hello_proof.why
+-- theory HelloProof
+-- goal G1: Simplify (1.5.4) (0.01)
+-- goal G3: Alt-Ergo (0.93) (0.02)
+-- goal G1: Simplify (1.5.4) (0.00)
+-- goal G3: Alt-Ergo (0.94) (0.00)
== Statistics per prover: number of proofs, time (minimum/maximum/average) in seconds ==
Alt-Ergo (0.93) : 2 0.02 0.02 0.02
Simplify (1.5.4) : 2 0.01 0.01 0.01
Alt-Ergo (0.94) : 2 0.00 0.00 0.00
Simplify (1.5.4) : 2 0.00 0.00 0.00
\end{verbatim}
}
......@@ -801,8 +802,6 @@ output.
\label{fig:custom-latex}
\end{figure}
\todo{rejouer HelloProofs, pour eviter tout ces 0.00, et qu'en plus
cela soit coherent avec la sortie HTML ci-dessous}
\begin{figure}[t]
\begin{center}
%HEVEA\begin{toimage}
......@@ -837,23 +836,25 @@ There are three styles of output: `table', `simpletree', and
`jstree'. The default is `table'.
\begin{figure}[t]
\begin{center}
%BEGIN LATEX
\begin{center}
\fbox{\includegraphics[width=0.9\textwidth]{hello_proof.png}}
\end{center}
%END LATEX
\begin{htmlonly}
\begin{rawhtml}
<h1>Why3 Proof Results for Project "hello_proof"</h1>
<h2><font color="#FF0000">Theory "HelloProof": not fully verified</font></h2>
<table border="1"><tr><td colspan="2">Obligations</td><td text-rotation="90">Alt-Ergo (0.94)</td><td text-rotation="90">Coq (8.3pl4)</td><td text-rotation="90">Simplify (1.5.4)</td></td></tr>
<td bgcolor="#C0FFC0" colspan="2">G1</td><td bgcolor="#E0E0E0">---</td><td bgcolor="#E0E0E0">---</td><td bgcolor="#C0FFC0">0.00</td></tr>
<td bgcolor="#FF0000" colspan="2">G2</td><td bgcolor="#FF8000">0.00</td><td bgcolor="#E0E0E0">---</td><td bgcolor="#FF8000">0.00</td></tr>
<tr><td bgcolor="#FF0000" colspan="2">split_goal</td><td bgcolor="#E0E0E0"></td><td bgcolor="#E0E0E0"></td><td bgcolor="#E0E0E0"></td></tr>
<td rowspan="2">&nbsp;&nbsp;</td><td bgcolor="#FF0000" colspan="1">G2.1</td><td bgcolor="#FF8000">0.00</td><td bgcolor="#FF8000">0.49</td><td bgcolor="#FF8000">0.00</td></tr>
<td rowspan="2">&nbsp;&nbsp;</td><td bgcolor="#FF0000" colspan="1">G2.1</td><td bgcolor="#FF8000">0.00</td><td bgcolor="#FF8000">0.43</td><td bgcolor="#FF8000">0.00</td></tr>
<tr><td bgcolor="#C0FFC0" colspan="1">G2.2</td><td bgcolor="#C0FFC0">0.00</td><td bgcolor="#E0E0E0">---</td><td bgcolor="#C0FFC0">0.00</td></tr>
<td bgcolor="#C0FFC0" colspan="2">G3</td><td bgcolor="#C0FFC0">0.00</td><td bgcolor="#E0E0E0">---</td><td bgcolor="#FF8000">0.00</td></tr>
</table>
\end{rawhtml}
\end{htmlonly}
\end{center}
\caption{HTML table produced for the HelloProof example}
\label{fig:html}
\end{figure}
......
......@@ -196,7 +196,9 @@ We gratefully thank the people who contributed to \why, directly or
indirectly: Romain Bardou, Simon Cruanes, Leon Gondelman, Johannes Kanig,
St\'ephane Lescuyer, Sim\~ao Melo de Sousa, Benjamin Monate, Asma Tafat.
\subsection*{Release Notes for version 0.80: syntax changes w.r.t. 0.73}
\section{Release Notes}
\subsection{Release Notes for version 0.80: syntax changes w.r.t. 0.73}
The syntax of \whyml programs changed in release 0.80.
The table in Figure~\ref{fig:syntax080} summarizes the changes.
......@@ -217,11 +219,11 @@ type t = \{ field~:~int \} \\
\\
\hline
\begin{minipage}[t]{0.45\textwidth}\ttfamily
\hspace*{3ex} \{| field = 5 |\} \\
\{| field = 5 |\} \\
\end{minipage}
&
\begin{minipage}[t]{0.45\textwidth}\ttfamily
\hspace*{3ex} \{ field = 5 \} \\
\{ field = 5 \} \\
\end{minipage}
\\
\hline
......@@ -309,7 +311,7 @@ abstract e ensures \{ Q \} \\
\label{fig:syntax080}
\end{figure}
\subsection*{Summary of Changes w.r.t. Why 2}
\subsection{Summary of Changes w.r.t. Why 2}
The main new features with respect to Why 2.xx
are the following.
......
......@@ -196,16 +196,16 @@ Figure~\ref{fig:bnf:expra} and~Figure~\ref{fig:bnf:exprb}.
\label{fig:bnf:exprb}
\end{figure}
In the following we describe the informal semantics of each constructs, and provide the corresponding rule for computing the weakest precondition.
In the following we describe the informal semantics of each
constructs, and provide the corresponding rule for computing the
weakest precondition.
\subsubsection{Constant expressions}
\subsubsection{Constant Expressions, Unary and Binary Operators}
\todo{Integer and real constants are as in the logic language}
\subsubsection{Unary and Binary Operators}
Integer and real constants are as in the logic language, as weel as the unary and binary operators.
\todo{}
\subsubsection{Array accesses and updates, fields access and updates}
......@@ -231,9 +231,51 @@ In the following we describe the informal semantics of each constructs, and prov
\todo{if then else. Discuss standard WP versus fast WP}
\subsubsection{Loops}
\subsubsection{Iteration Expressions}
There are three kind of expressions for iterating: bounded, unbounded and infinite.
\begin{itemize}
\item A bounded iteration has the form
\begin{flushleft}\ttfamily
for $i$=$a$ to $b$ do invariant \{ $I$ \} $e$ done
\end{flushleft}
Expressions $a$ and $b$ are evaluated first and only once, then expression $e$ si evaluated successively for $i$ from $a$ to $b$ included. Nothing is executed if $a > b$. The invariant $I$ must hold at each iteration including before entering the loop and when leaving it. The rule for computing WP is as follows:
\begin{eqnarray*}
WP(\texttt{for} \ldots, Q) &=& I(a) \land \\
&& \forall \vec{w} (\forall i, a \leq i \leq b \land I(i) \rightarrow WP(e,I(i+1))) \land (I(b+1) \rightarrow Q)
\end{eqnarray*}
where $\vec{w}$ is the set of references modified by $e$.
\todo{while, loop, for}
A downward bounded iteration is also available, under the form
\begin{flushleft}\ttfamily
for $i$=$a$ downto $b$ do invariant \{ $I$ \} $e$ done
\end{flushleft}
\item An unbounded iteration has the form
\begin{flushleft}\ttfamily
while $c$ do invariant \{ $I$ \} $e$ done
\end{flushleft}
it iterates the loop body $e$ until the condition $c$ becomes false.
\begin{eqnarray*}
WP(\texttt{while} \ldots, Q) &=& I \land \\
&& \forall \vec{w} (c \land I \rightarrow WP(e,I)) \land (\neg c \land I \rightarrow Q)
\end{eqnarray*}
where $\vec{w}$ is the set of references modified by $e$.
Additionally, such a loop can be given a variant $v$, a quantity that must decreases ar each iteration, so as to prove its termination.
\item An infinite iteration has the form
\begin{flushleft}\ttfamily
loop invariant \{ $I$ \} $e$ end
\end{flushleft}
it iterates the loop forever, hence the only way to exit such a loop is to raise an exception.
\begin{eqnarray*}
WP(\texttt{loop} \ldots, Q \mid Exc \Rightarrow R) &=& I \land \\
&& \forall \vec{w} (I \rightarrow WP(e,I)) \land (I \rightarrow WP(e,Exc \Rightarrow R))
\end{eqnarray*}
\end{itemize}
\subsubsection{Assertions, Code Contracts}
......@@ -268,8 +310,6 @@ The other forms of code contracts allow to abstract a piece of code by specifica
in the sense that it does not check whether there exists any program
that can effectively establish the post-condition (similarly as the
introduction of a \texttt{val} at the global level).
\item $\texttt{contract}~e~\{ Q \}$ evaluates the expression $e$ and
ensures that the post-condition $Q$ holds afterwards.
\item $\texttt{abstract}~e~\{ Q \}$ makes sure that the evaluation of
expression $e$ establishes the post-condition $Q$, and then abstract
away the program state by the post-condition $Q$ (similarly to the
......@@ -282,9 +322,6 @@ The corresponding rules for computing WP are as follows:
Q' exn_i \Rightarrow R'_i) = \\
\qquad\qquad P \mathop{\&\&} \forall result, \epsilon.
(Q \rightarrow Q') \land (R_i \rightarrow R'_i) \\
WP(\texttt{contract}~e~\{ Q \mid exn_i \Rightarrow R_i \} ,
Q' \mid exn_i \Rightarrow R'_i) = \\
\qquad\qquad WP(e,Q \land Q' \mid exn_i \Rightarrow R_i \land R'_i) \\
WP(\texttt{abstract}~e~\{ Q \mid exn_i \Rightarrow R_i \} ,
Q' \mid exn_i \Rightarrow R'_i) = \\
\qquad\qquad WP(e,Q \mid exn_i \Rightarrow R_i) \land
......@@ -292,12 +329,6 @@ The corresponding rules for computing WP are as follows:
\end{array}
\]
\todo{? sandbox:}
\[
WP(\texttt{sandbox}~e, Q) = WP(e,true) \land Q
\]
(side-effects in $e$ are "forgotten"...)
\subsubsection{Labels, old, at}
\todo{}
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment