Automatic Program Verification using Dafny

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

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.

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:

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 has a really good guide for learning all of this stuff which you can check out Best 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
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.

 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:

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

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

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

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";
 }