## Introduction to Dafny
The goal of today's session is to consolidate what we have
been learning about Dafny.
**First**, ensure that you have Dafny working in your PC.
You can also run [Dafny
online](https://rise4fun.com/Dafny), but the experience is not as good.
*In these labs, I recommend you to use the IDE VS Code.*
### 0. Before you continue
Start by revising the slides of [Lecture 6](06-dafny.html).
Make sure that you do all the exercises (if you haven't
done so already).
1. From manual to automated verification
Use Dafny to verify the following triples that we proved by hand
in Lab 1.
Define methods
for each of the exercises. For some of
them, defining functions to be used in the specification is
the most challening aspect.
1.1. Integer division
$$
\scriptsize
\begin{array}{l}
\{ A\gt 0 \wedge B\gt 0 \}\\
q := 0; \\
r := A; \\
\texttt{while}\,\,r\ge B\,\,\texttt{do \{} \\
~~~ q := q+1; \\
~~~ r := r-B \\
\texttt{\}}\\
\{ A = q\times B + r \,\,\wedge\,\, 0\le r \,\,\wedge\,\, r\lt B \}
\end{array}
$$
1.2. Factorial
$$
\scriptsize
\begin{array}{l}
\{ x \ge 0 \}\\
y := 1; \\
z := 0; \\
\texttt{while}\,\,z\neq x\,\,\texttt{do \{} \\
~~~ z := z+1; \\
~~~ y := y*z \\
\texttt{\}}\\
\{ z = x \,\wedge\, y=x! \}
\end{array}
$$
1.3. Euclid's algorithm
$$
\scriptsize
\begin{array}{l}
\{ 0\lt M \,\wedge\, 0\lt N\}\\
x:=M;\,\,y:=N;\\
\texttt{while}\,\,x\neq y\,\,\texttt{do \{} \\
~~~ \texttt{if}\,\,\,x\lt y\,\,\,\texttt{then} \\
~~~~~~~~~ y := y-x \\
~~~ \texttt{else} \\
~~~~~~~~~ x := x-y \\
\texttt{\}}\\
\{ x = y = GCD(M,N) \}
\end{array}
$$
1.4. Exponentiation
$$
\scriptsize
\begin{array}{l}
\{ A\ge 0 \,\wedge\, B\ge 0\}\\
r:=1;\,\,x:=0;\\
\texttt{while}\,\,x\neq B\,\,\texttt{do \{} \\
~~~~~~ r := r*A; \\
~~~~~~ x := x+1 \\
\texttt{\}}\\
\{ r = A^B \}
\end{array}
$$
2. Square Root
Write a verified method that given a natural number returns its
square root, rounded down.
To give an example, we should have $sqrt(x) = 2$ for
$4\le x \lt 9$.
3. The n-th odd number
Annotate the following code so that Dafny can verify it.
method nth_odd (n: nat) returns (j: int)
ensures j == 1 + 2*n
{
var k := 0;
j := 1;
while k < n
{
k := k + 1;
j := j + 2;
}
}
4. The n-th even number
Define a verified method similar to nth_odd but that returns the $n^{th}$ even number.
5. Mysterious Loop (I)
What does the following method do, assuming that $x$ is a
positive integer? Add a specification and loop invariant for
the method.
method loop(x: int) returns (ret:int)
{
var y := x;
var z := 0;
while (y > 0)
{
z := z + x;
y := y - 1;
}
return z;
}
6. Mysterious Loop (II)
What does the following method do? Add a specification and loop invariant for
the method.
method loop2 (n: nat) returns (j : nat)
{
var k := 0;
j := 1;
while k < n
{
k := k + 1;
j := 2 * j ;
}
}