/** Verification with Dafny */

/* Verification in Dafny is all about specifications. 
   In this lecture, our goal will be to specify and verify
   a sequence of increasingly more complex functions, to 
   get a feeling about what we can/can't prove automatically,
   as well as a first taste of coming up with invariants. 
   
   Meanwhile, we will be introducing more syntax and intricacies
   of the Dafny language.
   */

/* To begin with, consider the following `Min` function. It 
   takes two integers, a and b, and returns two integers, x and y.
   This is the first, perhaps surprising, feature of Dafny: methods
   can have multiple outputs! This goes hand in hand with the slightly
   unconvential way that Dafny handles method returns---the return
   value is whatever is assigned to a return variable at the end of 
   the control flow. But that can easily scale to multiple outputs! */
method Min(a : int, b: int) returns (x : int, y : int)
{
    if a <= b 
    {
        x := a;
        y := b;
    }
    else
    {
        x := b;
        y := a;
    }
}

/* As it stands, Dafny accepts this definition. There is no specification 
to check, no array accesses, nothing that can really go wrong. Or is there?
Try deleting an assignment or a branch: Dafny will immediately complain that
an "out-parameter which is subject to definite-assignment rules might be uninitialized".
What that means is that, by default, Dafny will check that every output parameter
(and every variable that is used) will be initialized.

But we haven't actually specified what it means for `Min` to actually compute
the minimum of two numbers. What are possible specifications? 

The natural one is that it ensures `x <= y`. */

method MinSpec(a : int, b: int) returns (x : int, y : int)
    ensures x <= y
{
    if a <= b 
    {
        x := a;
        y := b;
    }
    else
    {
        x := b;
        y := a;
    }
}

/* 
Dafny does verify that ordering, but is that enough? What does "enough" even mean?
Is there a method other than this one which satisfied `x <= y` but is not 
the "minimum" method? */
method OtherMin(a : int, b: int) returns (x : int, y : int)
    ensures x <= y
{
    x := 0;
    y := 42;    
}
/* We don't have any links between the inputs and outputs to the method! A fully
   specified Minimum function therefore looks like the following (as we saw in the
   introduction, multiple "ensures" or "requires" clauses are joined via conjunction):
*/
method Minimum(a : int, b: int) returns (x : int, y : int)
    ensures x <= y
    ensures x == a || x == b
    ensures y == a || y == b
{
    if a <= b 
    {
        x := a;
        y := b;
    }
    else
    {
        x := b;
        y := a;
    }
}

/** Test yourself: Fill in, specify, and verify the absolute value function: */
method Abs (x : int) returns (y : int)
    // Specification goes here
{
    y := 42; // Replace with your implementation here
}

/* Let's do another loop-free example: evaluating 2-nd degree polynomials:
How do we evaluate something like a*x^2 + b*x + c? We could just evaluate
this expression - but that's inefficient: we perform too many multiplications!
Here's the standard more efficient way:
*/
method Poly2(a:int,b:int,c:int,x:int) returns (out:int)
  ensures out == a*x*x+b*x+c
{
  var o1 := a * x;
  var o2 := (o1 + b) * x;
  return o2 + c;
}
/* For most straight-line code, Dafny can prove the correctness of your 
code with respect to its specification automatically. But there is a 
limit to what we can program without any kind of loop or recursion. */

/** Dafny verification and Loops */

/* Sticking to the "minimum" theme, let's look at a method for 
   finding the minimum element of an array. We start by initializing
   the return value to the first element of the array; then, we iterate
   through the rest of the array updating the result when appropriate.
   */
method FindMinBase (a : array<int>) returns (m : int)
{
  m := a[0];
  var i:= 1;
  while (i < a.Length)
  {
    if a[i] < m
      { m := a[i]; }
    i := i+1;
  }
}

/* Immediately, Dafny complains - the array access a[0] could be out 
of bounds. To fix this, we must _require_ that the length of the 
input array is greater than 0. Let's also specify the function:
the result m should be smaller than all elements in the array; we 
will use a `forall` quantifier to encode that fact: */
method FindMinSpec (a : array<int>) returns (m : int)
  requires a.Length > 0
  ensures forall j:int :: 0 <= j < a.Length ==> m <= a[j]
{
  m := a[0];
  var i:= 1;
  while (i < a.Length)
  {
    if a[i] < m
      { m := a[i]; }
    i := i+1;
  }
}
/* Dafny no longer complains about array accesses, but it can't 
verify the postcondition. It needs a loop invariant. Again, we 
will focus on loop invariants in future lectures, but for now
we can try to come up with them by focusing on "whats true at
every iteration of the loop". In this particular case, we know 
that m is the minimum element from all the ones we have checked 
so far! 

Adding only that invariant, however, is not enough. Our invariant
accesses a[j], so we need to ensure that that is within range as well.
*/

method FindMin (a : array<int>) returns (m : int)
  requires a.Length > 0
  ensures forall j:int :: 0 <= j < a.Length ==> m <= a[j]
{
  m := a[0];
  var i:= 1;
  while (i < a.Length)
    invariant i <= a.Length
    invariant forall j:int :: 0 <= j < i ==> m <= a[j]
  {
    if a[i] < m
      { m := a[i]; }
    i := i+1;
  }
}

/* Test yourself! Implement and verify the following square root method: */
method SquareRoot(N: int) returns (r: int)
  requires N >= 0
  ensures r * r <= N < (r + 1) * (r + 1)
{
  r := 0;
  while (r + 1) * (r + 1) <= N
    invariant r * r <= N
  {
    r := r + 1;
  }
}

/* A nice feature of verification is that we can verify more complicated
and more efficient ways of performing the same computation. Why does
the following function verify? */

method MoreEfficientSquareRoot(N: int) returns (r: int)
  requires N >= 0
  ensures r * r <= N < (r + 1) * (r + 1)
{
  r := 0;
  var s := 1;
  while s <= N
    invariant r * r <= N
    invariant s == (r + 1) * (r + 1)
  {
    s := s + 2*r + 3;
    r := r + 1;
  }
}

/** Functional specifications in Dafny.

As discussed in the introduction, Dafny consists of a 
language of expressions which is extended via commands to a language
for implementing imperative methods, and via quantifiers to a 
language for specifications. Dafny includes another layer: a full functional 
language. Let's see that in practice with our favorite example: Fibonnacci numbers.
*/

function fib(n:int) : int {
  if n < 2 then n else fib(n - 2) + fib(n - 1)
}

/* The syntax for functions in Dafny is straightforward: we declare
them with the `function` keyword, followed by the name of the function,
any arguments, and the return type of the expression. The body of the 
function consists of a single expression - what the function is expected 
to return. 

What can we do with this definition? For the most part, we will be using
such functions as specifications:
*/
method Fib(n:int) returns (x : int) 
    requires n >= 0
    ensures x == fib(n)
{
  x := 0;
  var y := 1;
  var i := 0;
  while i != n
    invariant x == fib(i) && y == fib(i + 1)
  {
    x, y := y, x + y; // NEW SYNTAX: Simultaneous assignment!
    i := i + 1;
  }
}
/* That is, the imperative, efficient implementation that mutates
two variables in place to keep track of the last two values of 
the Fibonacci sequence, correctly implements the trivial but 
inefficient functional implementation. */

/* For another example, let's implement a functional and imperative version
of the factorial function, and verify that they correspond! */
function fact (n : int) : int
{
    if (n <= 0) then 1 else n * fact(n-1)
}

/* A note on termination:

By default, Dafny checks that any recursive function terminates using
heuristics. In particular, try changing the `n <= 0` check to an equality.
Dafny will complain that "decreases must be bounded below by 0". Termination
checking works by finding some quantity that decreases at every iteration
while being bounded from below. In this particular case, Dafny would correctly
complain that if the integer n is negative, fact would loop forever.
*/

method Fact(n : int) returns (x : int)
  requires n >= 0
  ensures x == fact(n)
{
  var i := n; // NOTE: n is not a variable that can be assigned to! 
  x := 1;
  while (i > 0)
    invariant fact(i) * x == fact (n)
  {
    x := x * i;
    i := i - 1;
  }
}

/* Test yourself! Write an imperative version of factorial that counts
up to n rather than down to 0! */

/** Now, time for a larger example. Let's revisit our search example
from last lecture, but now let's require that the input array is sorted.
That enables binary search for the key. 

First, how do we specify sortedness? The answer is double quantification! 

  forall i, j :: 0 <= i < j < a.Length ==> a[i] <= a[j]

What should binary search return? It should return the smallest index n in the 
array, such that all elements before n are strictly smaller, and all elements 
after (and including) n are greater or equal.

*/

method BinarySearch(a: array<int>, key: int) returns (n: int)
  requires forall i, j :: 0 <= i < j < a.Length ==> a[i] <= a[j]
  ensures 0 <= n <= a.Length
  ensures forall i :: 0 <= i < n ==> a[i] < key
  ensures forall i :: n <= i < a.Length ==> key <= a[i]
{
  var lo, hi := 0, a.Length;
  while lo < hi
    invariant 0 <= lo <= hi <= a.Length
    invariant forall i :: 0 <= i < lo ==> a[i] < key
    invariant forall i :: hi <= i < a.Length ==> key <= a[i]
  {
    var mid := (lo + hi) / 2;
    if a[mid] < key {
      lo := mid + 1;
    } else {
      hi := mid;
    }
  }
  n := lo;
}

/* As for invariants, what do we know at every point? We start with 
lo at 0 and hi at a.Length - bounds to the array for which one part 
of the postcondition holds trivially. And we just keep shortening 
the range until lo and hi coincide! 

Now we can wrap the call to BinarySearch inside a convenient Contains function. */

method Contains(a: array<int>, key: int) returns (present: bool)
  requires forall i, j :: 0 <= i < j < a.Length ==> a[i] <= a[j]
  ensures present == exists i :: 0 <= i < a.Length && key == a[i]
{
  var n := BinarySearch(a, key);
  present := n < a.Length && a[n] == key;
}