/* A First Taste of Dafny

This is the first of many lecture note files that we will go over in
class and that will be made available right after.

The first topic is going to be Dafny itself, what it is and what it
brings to the table. Lecture notes will be compileable files in 
the programming language we are looking at (Dafny/Haskell) that 
you can edit or play around with at your leisure.

*/

/* Dafny: A Standard Imperative Programming Language */

/* At a first glance, Dafny programs can be viewed as standard 
imperative programs. While there are minor syntactic differences,
from keywords to assignment operators and so on, you are probably
able to _read_ plain Dafny code already. Let's try it!

What does the following function do?

*/

method Mystery(a: array<int>, x: int) returns (i: int)
  {
  i := 0;
  while i < a.Length
  {
    if a[i] == x
    { 
      return; 
    }
    i := i + 1;
  }
  i := -1;
}

/* In terms of concrete syntax, this code snippet defines a `method`,
the basic building block of imperative Dafny programs. The name 
of the method is Mystery, and it takes two arguments
- `a`, whose type is an array of integers (written in template syntax `array<int>`)
- `x`, whose type is an integer (written `int`)
This Mystery method also has an output, `i`, also of integer type.

This is the first rather untraditional feature of Dafny methods: not 
only are input parameters named, but so are output parameters. The return
value (or values as we will see!) is the value of the return parameter 
at the conclusion of the method's control flow.

The main body of the loop is rather straightforward:
- We start by initializing the output parameter to 0 (assignment in Dafny is 
written with the `:=` operator)
- We then perform a while loop: while the output parameter is less than 
the length of the array (`a.Length` accesses the length of the array `a`),
we check whether the i-th element of the array is equal to x. 
  + If it is, we `return`. Note again that we don't return a variable - the 
  value of the output parameter is equal to its value at this point.
  + If not we increment `i` by 1.
- At the end of the loop, if we have not returned, we assign the integer -1 
to `i` and return (let the control flow reach the end of the method).

So what does this function do? As you might have correctly guessed,
this function performs a linear search in the input array, looking for 
its integer input. If it finds this input, it returns its index; if not,
it returns -1. So let's rename our variables and method to more sensible
names, and, being sensible programmers, add comments about the method's
functionality:

*/

// Linear Search in an Array
// It returns the index of the key, if it finds it
// It returns -1, if the key is not in the array
method LinearSearch(a: array<int>, key: int) returns (index: int)
{
  index := 0;
  while index < a.Length
  {
    if a[index] == key 
    { 
      return; 
    }
    index := index + 1;
  }
  index := -1;
}

/* Great! But are we done? Well, is there anything that actually checks 
the correspondence between the comment and the method's implementation?
No! The connection is only in the programmers brain. Naturally,
we can write tests that exercise different behaviors. 

Dafny identifies a `Main` method in a program, which is the entry point
to the program. (If you are in VSCode, it can be invoked with `F5` or 
any other standard way of running/debugging your code).
*/

method Main() 
{
  var a := new int[3];
  a[0] := 0;
  a[1] := 42;
  a[2] := 17;
  var r1 : int := LinearSearch(a, 42);
  var r2;
  r2 := LinearSearch(a, 43);
  print "Result 1:  ", r1, "\nResult 2:", r2, "\n";
 }

 /* A few more new bits of syntax, but nothing surprising.
 Note that we can declare local variables with the `var` keyword. 
 These are strongly typed - but Dafny's type inference can naturally
 infer them for this simple program. We can also annotate a variable
 with its type (`var r1 : int`) or declare a variable and then 
 initialize it (`var r2; ... r2 := ..`). Finally, the `print` command
 takes a comma-separated sequences of things to print, and does so.

 If we run this program, we can check that the output is as expected:

  Result 1: 1
  Result 2:-1

 Of course, printing the result of a method call is a far cry from 
 ensuring its correctness. Normally, in another language we'd turn to
 testing techniques (unit tests, property-based tests, etc.) in order
 to establish confidence in our program. However, Dafny offers a much
 more powerful tool: _verification_.
*/

/** Dafny: A Verification Aware Programming Language */

/* Dafny offers a way to _prove_, mathematically, once and for all that 
your program does what it's supposed to do. But how does it know what 
it's supposed to do? That is the role of a _specification_. Every method 
can be annotated logical expressions that express what the method expects 
from its arguments, and what it guarantees about its output.

We will return to the LinearSearch example shortly, but let's start
by trying to verify an even simpler program: accessing an array element.\

The following method simply returns the i-th element of an array. 
*/
method Access(a:array<int>, i:int) returns (x:int)
{
  return a[i];
}
/* Alas, it's not that simple. If you are reading this file in VSCode,
Dafny will complain with an "index out of range" Error. That is, even
if we don't have _any_ specification, Dafny will try to verify that 
all your memory accesses are in-bounds.

At this point, we could simply change the program to check 
whether the access is in bounds---but we have to do something about 
the case when it doesn't, otherwise Dafny will complain that the 
output value might be uninitialized (try it! remove the assignment 
outside the `if` and see what happens!)
 */
method SafeAccess(a:array<int>, i:int) returns (x:int)
{
  if 0 <= i < a.Length 
  {
    return a[i]; // This is equivalent to {x := a[i]; return;}
  }
  x := -1; // This is equivalent to return -1;
}
/* Great! Dafny doesn't complain anymore, which means all our 
array accesses are _provably_ safe---we will see what that means
in future lectures. But safe array access is not the only
thing we care about: we can ensure that the return value is 
the result of the array access with an `ensures` annotation:
*/
method SafeAccessSpec(a:array<int>, i:int) returns (x:int)
  ensures 0 <= i < a.Length ==> x == a[i]
{
  if 0 <= i < a.Length 
  {
    return a[i]; // This is equivalent to {x := a[i]; return;}
  }
  x := -1; // This is equivalent to return -1;
}
/* This `ensures` annotation is comprised by two boolean expressions
(which are valid Dafny code) separated by a boolean connector that 
denotes implication `==>`. It states that when i is in range, then
the output parameter of the function is equal to the i-th element
of the array. Dafny can _verify_ this specification, proving that 
this is always the case (again, try it! any changes to the method
that invalidate this specification will trigger a failure).

Another option to specify the original unsafe `Access` method
is to state that the method _only_ works for indices in ranges. 
After all, a lot of the time software expects complicated invariants
to hold on their inputs that are not checked over and over. To that
end Dafny provides a `requires` keyword that specifies what should
hold when this method is invoked.
*/
method SafeAccessPrec(a:array<int>, i:int) returns (x:int)
  requires 0 <= i < a.Length
  ensures x == a[i]
{
    return a[i]; 
}

/* Dafny once again is satisfied with our specification---but if you 
try to invoke it with an index out of range it will complain then 
(try it!). */

/** Back to our Linear Search example, what is a good specification for 
it? A good source of inspiration is to look at the comments we wrote!

// Linear Search in an Array
// It returns the index of the key, if it finds it
// It returns -1, if the key is not in the array

The first one is easy to translate to a Dafny spec, just like 
in our Access example, we would like to prove that `a[index] == key`.
When does that hold? when the index return is within the range of the 
array. The resulting spec could be:

  ensures 0 <= index < a.Length ==> a[index] == key

The second one is trickier, how do we encode "the key is not in the array".
Dafny provides quantifiers, `forall` and `exists` that allow us to encode
such properties: If the index returned is `-1`, no elements of the 
array are equal to the key. In Dafny code:

  ensures index < 0 ==> forall k :: 0 <= k < a.Length ==> a[k] != key

Note the syntax: `forall k :: e` states that `e` holds for all `k` 
(which are inferred to be integers).

Putting these two together, we can write a first spec for LinearSearch
(we could combined them with a conjunction, but Dafny allows for multiple
requires and ensures statemetns to be interpreted as such). 
*/

method LinearSearch2(a: array<int>, key: int) returns (index: int) 
  ensures 0 <= index < a.Length ==> a[index] == key
  ensures index < 0 ==> forall k :: 0 <= k < a.Length ==> a[k] != key
{
  index := 0;
  while index < a.Length
  {
    if a[index] == key 
    { 
      return; 
    }
    index := index + 1;
  }
  index := -1;
}
/* Oh no, Dafny complains: "a postcondition could not be proved on this return path"!

What does that mean? It means it couldn't automatically prove that our program
conforms to the required specification. That is, however, to be expected. Verifying 
an arbitrary program automatically is an utterly undecidable endeavor! So what can we do?
In Dafny we can write invariants to help the prover. Invariants will be a core topic in 
future lectures, as that is one of the main obstacles users face. For now, you can 
think of them as predicates that remain invariant (as in, their truth remains unchanged)
across different loop iterations. 

In our particular example, there are two things we need to know
to verify that our search is correct: 
1. That we have checked all elements up to the current index and
 the `key` is not among them. 

  invariant forall k :: 0 <= k < index ==> a[k] != key

2. That the index remains less than or equal to the array's Length.

  invariant index <= a.Length
  
Why these two? Well, the first one is the core "logic" of the loop.
If it holds before a loop iteration, that is all elements up
to `index` are not equal to the key, then the next iteration checks 
the `index` and increments it by one. The second one is needed to 
ensure that the array accesses (including the one in the invariant!)
are in range. We will demystify how invariants, and the verification 
process in general, work throughout the semester.

For now, let's put everything together:
*/
method LinearSearchVerified(a: array<int>, key: int) returns (index: int)
  ensures 0 <= index < a.Length ==> a[index] == key
  ensures index < 0 ==> forall k :: 0 <= k < a.Length ==> a[k] != key
{
  index := 0;
  while index < a.Length
    invariant index <= a.Length
    invariant forall k :: 0 <= k < index ==> a[k] != key
  {
    if a[index] == key 
    { 
      return; 
    }
    index := index + 1;
  }
  index := -1;
}

/* For one last time, try it! Changing anything about the program in a way that breaks
its correctness will immediately trigger errors in the verifier. You can be
absolutely certain that this linear search is correct (with respect to its specification).
Dafny (and verification in general) is a very powerful tool, which is used in
safety-critical systems around the world. */

/** Side note: Expressions, Commands, and Specifications. 

At this point you might be wondering about all the different 
syntactic constructs that we have introduced and when/where 
they can be used. At a first approximation, we have three 
languages:
- A language of expressions. This is a standard core language
of expressions like the one you encounter in most languages,
imperative or functional. This includes 
  + Booleans: Constants (true, false),  Negation (!b), 
  Conjunction (b1 && b2), Disjunction (b1 || b2), 
  Implication (b1 ==> b2), Equivalence (b1 <==> b2), etc.
  + Integers: Numbers (0,1,42,..), Negation (-n),
  Binary operations (+,-,*,/,%), Comparisons(==,!=,<=,<,..), etc.
  + Characters ('a'), Reals (42.42),...
  + Tuples (42,true,'a') and Projections (t.1)
  + If-Expressions (if b then e1 else e2)
  And more.

- A language of imperative commands. These include standard 
imperative constructs that we have seen to implement methods 
such as:
  + while b { c }
  + if b { c1 } else { c2 }
  + x := e
A key distinction in Dafny is that: 
  
  Expressions can appear inside commands (as guards in conditionals,
  as expressions to be assigned, etc.), but commands can never appear
  inside expressions!

- A language of specifications. This includes all expressions 
with a boolean type, as well as quantifiers:
  + forall k : T :: b
  + exists k : T :: b
  These act as binders for k, as in they introduce it as a new
  variable, and encode universal or existential quantification.
  These can appear in specs (requires, ensures, invariants), but 
  not inside commands. (After all, how would you run a program
  that needs to check such a quantifier?)

We will see in the next few lectures that the language of expressions
is actually a fully-fledged but pure functional language, and the idea
is that this language can be used to specify the behavior of imperative,
state-manipulating programs.
*/