Automatic Program Verification using Dafny
Tags: programming, dafny, verification
Published: 2021-04-16 14:13:41

##Program Verification
>Program Verification is the process of proving that the program does exactly what the developer intended it to do and noting more.

basically it can help prevent us from creating something like 
![HAL](https://dev-to-uploads.s3.amazonaws.com/uploads/articles/podgy06c3wxcao7tf8e4.png)
not exactly but close enough.
## Why testing is not enough

>“Testing shows the **presence**, not the **absence** of bugs”          

-Edsgar W. Dijkstra

For this post HAL is not a super smart AI but a simple program that performs arithmetic operations.
if we were to test HAL he is smart enough to give us correct output for our questions 
```
Hal what is 2 + 2?
HAL: 4
HAL what is 2*2 ?
HAL: 4
```
HAL gives correct answers to our questions in our test does this mean HAL works as we intended it to work.

Spoiler alert 
No

HAL can be returning 2 every time we run it and we wound not notice it with such test. In real life no one will use such small test for their program but even with exhaustive testing we cannot say with 100% confidence that program will work.

##So what is the solution?

>Formal Methods 

Formal methods is just a fancy way of using mathematics in the verification of your program. 

![mathematics meme](https://dev-to-uploads.s3.amazonaws.com/uploads/articles/sw4jm7lg2dyhjm3p3x4a.jpg)

Formal methods are really difficult to do and this article is not exactly about them so I'll get straight to the point. but remember that a program that does formal verification for us will take the code we write and what the code is supposed to do from us in order to verify it.
##Dafny

>Dafny is programming language that helps us in doing formal verification

dafny is close to C# so a lot of thing are similar in dafny.

The most cool thing about Dafny is it can show we are making a mistake while we are writing the code.

Eg:
```cs
method Double(x: int) returns (r: int)
   requires  x > 0
   ensures r==2*x
{
   r := x + x;
}
```
the above code has a method Double which returns the double value of the int it takes in.
The keywords **ensures** and **requires** give us a way to specify what the code is supposed to do.
If we make some silly mistake and instead of + we write - dafny will show the error to us

![Dafny example ](https://dev-to-uploads.s3.amazonaws.com/uploads/articles/160vkzagydfy6q3jthzk.png)

Dafny has a really good guide for learning all of this stuff which you can check out [Best Guide](https://rise4fun.com/dafny/tutorialcontent/guide) and below I will be summarizing what I learned from it.

##Summary from what I learnt
###Advantages
1. Can detect bugs while writing code.
2. Similar to C# and can be installed with [VS code extension](https://marketplace.visualstudio.com/items?itemName=correctnessLab.dafny-vscode#:~:text=This%20extension%20adds%20Dafny%203.0,requires%20the%20Dafny%20language%20server.)
3. Provides a great learning opportunity.

###Disadvantages
1. Dafny uses the Boogie Intermediate language and Z3 SMT solver so is limited by what they both can do.
2. Dafny cannot be used for existing code we need to write new code to use dafny.

###Different parts of Dafny
####Method
A method is function which takes zero or more arguments and returns zero or more  values. it is differnt than functions present inside dafny. The main method in dafny is Main()
it is not necessary for verification but we need it for getting a .net executable from our code as the execution of code will begins here.
```c
 method Main()
 {
  
   print "Hello World";
   print "\n";
 }
```
####Function
the keyword function is used for pure functions in dafny. they cannot change the state of program and are ghost by default menas they do not appear in the compiled code. They are used to define mathematical logic.
eg: 
```cs 
function fib(n: nat): nat
{
	if n < 2 then  n
    else
		fib(n - 1) + fib(n - 2)
}
``` 
####Pre and Post Conditions
They help in specifying the specifications of the program a precondition must be true before the execution of method and a post condition must be true after the execution of the program.
#### loop invariants 
They specify the range of loop condition  suppose for a loop i goes from 0 to n then we can specify loop invariants as 
```cs
while i<n
   invariant 1 <= i <=n
   {
      i := i + 1;
   }
   assert i == n; 
```
They help in dafny in understanding how many times the loop occurs.
#### Termination
Dafny can automatically determine if a loop will terminate or not 
```cs
while i<n
       invariant 1 <= i <=n
   {
      i := i + 1; 
       if i<n  {i:= 1;}
       if i==1 {break;}
   }
```
When we run this code we see dafny knows the code terminates.
### Fiboncacci verification using dafny
```cs
function fib(n: nat): nat
decreases n
{
	if n < 2 then  n
    else
		fib(n - 1) + fib(n - 2)
}


method ComputeFib(n: nat) returns (b: nat)
	ensures b == fib(n)  
{
	if n == 0 { return 0; }
	var i: int := 1;
	var c := 1;
		b := 1 ;
	while i < n
		invariant  0< i <= n
		invariant b == fib(i)
		invariant c == fib(i + 1)
	{
		b, c := c, b + c;
		i := i + 1;
	}
}

 
 method Main()
 {
   var result:int := ComputeFib(6);
   print "fib(6):= ";
   print result;
   print "\n";
 }
```