# Verification in Dafny (2020)

Goto the [Dafny homepage](https://dafny.org/) ... see also [here](https://www.microsoft.com/en-us/research/project/dafny-a-language-and-program-verifier-for-functional-correctness/).

Unfortunately, these notes were written referring to an online-in-the-browser version of Dafny that used to be at [here](https://rise4fun.com/Dafny) but is not available anymore.

It seems that there is a new and better version [here](https://github.com/dafny-lang/dafny/blob/master/docs/OnlineTutorial/guide.md) but the tutorial needs a bit more work to get through.

For the remainder of this note, I use the [version at the way-back-machine](https://web.archive.org/web/20210621232650/https://rise4fun.com/Dafny) to reconstruct what was here in 2020.

**Activity:** Let us work through the sample programs, see "samples" in the lower left of the [page](https://rise4fun.com/Dafny). (Last time I checked this page was down.)

Hello
Fibonacci
Ackermann

[^runtheprogram]

[^runtheprogram]: (This referred to the online version:) In case you do not only want to verify but also run the programs, here is a simple example that shows how to invoke a method and print the result.

	method Plus(x: int, y: int) returns (r: int)
	{
	  r := x+y;
	}
	
	method Main() {
	  var r := Plus(2,3);
	  print r;
	}

Next let us look at the Dafny program `Add`.

// The following program is intended to compute
// twice 'x' plus 'y' into the out-parameter 'r',
// given that 'x' and 'y' are non-negative integers.
// The precondition (keyword 'requires') states the
// non-negative assumption and the postcondition
// (keyword 'ensures') states the intended result.
// The loop invariant (keyword 'invariant') states
// a condition that is intended to hold at the top
// of every loop iteration, just before the loop
// guard is evaluated.
// Can you correct the program and get Dafny to verify it?

method Add(x: int, y: int) returns (r: int)
  requires 0 <= x && 0 <= y
  ensures r == 2*x + y
{
  r := x;
  var n := y;
  while n != 0
    invariant r == x+y-n && 0 <= n
  {
    r := r + 1;
    n := n - 1;
  }
}

**Exercise:** Correct the program `Add`. Write a method `Main` that invokes `Add` and prints the result.

**Activity:** Translate

while (x != 0 ) do z:=z+y; x:= x-1 done

into Dafny and verify it.

Answer [^example1].

## Homework

Go back to the examples of the [lecture](https://hackmd.io/Df57tnuCSGaW8wqqsl57FQ) and the [exercises](https://hackmd.io/@alexhkurz/rkhVZNzjH) and verify some of them in Dafny.

Read Section 2 (and possibly more) of [Using Dafny, an Automatic Program Verifier](https://www.microsoft.com/en-us/research/wp-content/uploads/2016/12/krml221.pdf).

## Lorem Ipsum

[Lorem ipsum](https://www.lipsum.com/) dolor sit amet, consectetur adipiscing elit, sed do eiusmod tempor incididunt ut labore et dolore magna aliqua. Ut enim ad minim veniam, quis nostrud exercitation ullamco laboris nisi ut aliquip ex ea commodo consequat. Duis aute irure dolor in reprehenderit in voluptate velit esse cillum dolore eu fugiat nulla pariatur. Excepteur sint occaecat cupidatat non proident, sunt in culpa qui officia deserunt mollit anim id est laborum.

(This was added to move the solution in the footnote out of sight.)

## References

- [Using Dafny, an Automatic Program Verifier](https://www.microsoft.com/en-us/research/wp-content/uploads/2016/12/krml221.pdf)
- Rustan Leino speaks on Microsoft projects on [Engineering Methods for Ensuring Program Correctness](https://www.microsoft.com/en-us/research/video/engineering-methods-for-ensuring-program-correctness/) in general and Dafny in particuar, 2012.

[^example1]:

	method Example1(n: int, m: int, k:int) returns (z: int)
	  requires 0 <= n 
	  ensures z == n*m + k
	{
	    var x := n;
	    z := k;
	    while x != 0 
	      invariant z == (n-x)*m+k
	    {
	        z := z+m;
	        x := x-1;
	    }
	}
	method Main() {
	  var r := Example1(2,3,1);
	  print r;
	}