Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
7
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Open sidebar
Why3
why3
Commits
e5cbb752
Commit
e5cbb752
authored
Jun 29, 2011
by
François Bobot
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
doc : typo, subsection -> section
parent
0c996fcf
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
with
6 additions
and
6 deletions
+6
-6
doc/whyml.tex
doc/whyml.tex
+6
-6
No files found.
doc/whyml.tex
View file @
e5cbb752
...
...
@@ -50,9 +50,9 @@ See Chapter~\ref{chap:manpages} for more details regarding command lines.
As an introduction to
\whyml
, we use the five problems from the VSTTE
2010 verification competition~
\cite
{
vstte10comp
}
.
The source code for all these examples is contained in
\why
's
distribution, in
d
ub-directory
\texttt
{
examples/programs/
}
.
distribution, in
s
ub-directory
\texttt
{
examples/programs/
}
.
\
sub
section
{
Problem 1: Sum and Maximum
}
\section
{
Problem 1: Sum and Maximum
}
The first problem is stated as follows:
\begin{quote}
...
...
@@ -192,7 +192,7 @@ unsolved goal, which reduces to proving the following sequent:
This is easily discharged using an interactive proof assistant such as
Coq, and thus completes the verification.
\
sub
section
{
Problem 2: Inverting an Injection
}
\section
{
Problem 2: Inverting an Injection
}
The second problem is stated as follows:
\begin{quote}
...
...
@@ -292,7 +292,7 @@ end
\label
{
fig:Inverting
}
\end{figure}
\
sub
section
{
Problem 3: Searching a Linked List
}
\section
{
Problem 3: Searching a Linked List
}
The third problem is stated as follows:
\begin{quote}
...
...
@@ -464,7 +464,7 @@ exactly as for a recursive function. Such a variant must strictly decrease at
each execution of the loop body. The reader is invited to figure out
the loop invariant.
\
sub
section
{
Problem 4: N-Queens
}
\section
{
Problem 4: N-Queens
}
The fourth problem is probably the most challenging one.
We have to verify the implementation of a program which solves the
...
...
@@ -719,7 +719,7 @@ end
\end{figure}
\
sub
section
{
Problem 5: Amortized Queue
}
\section
{
Problem 5: Amortized Queue
}
The last problem consists in verifying the implementation of a
well-known purely applicative data structure for queues.
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment