// Recapitulare

// Dafny: implementare (imperativ), specificare (funcțional)

// implementare (method)
method fibo1(n : nat) returns (r : nat)
  ensures r == fibo(n)
{
  if (n <= 1) {
    return n;
  } else {
    var a := fibo1(n - 1);
    var b := fibo1(n - 2);
    return a + b;
  }
}

// implementare 2
method fibo2(n : nat) returns (r : nat)
  ensures r == fibo(n)
{
  var a := 0; // a si b sunt doua numere fibonacci de pe poz consecutive
  var b := 1;
  var i := 0;
  while (i < n)
    invariant 0 <= i <= n // <- invariantul despre index
    invariant a == fibo(i)
    invariant b == fibo(i + 1)
  {
    var temp := a + b;
    a := b;
    b := temp;
    i := i + 1;
  }
  assert i == n;
  return a;
}

// specificare (function, ca la matematică)
// ghost = șters la momentul execuției (compilării), folosit doar pentru verificare
ghost function fibo(n : nat) : nat
{
  if (n <= 1) then
    n
  else
    fibo(n - 1) + fibo(n - 2)
}

/*
   0 1 2 3 4 5 6  7 ...
   0 1 1 2 3 5 8 13
   
   */

// daca specificatia si implementarea sunt sintactic similare,
// nu este nevoie sa scriu ambele, ci scriu o functie care nu e ghost
function fibo_spec_impl(n : nat) : nat
{
  if (n <= 1) then
    n
  else
    fibo_spec_impl(n - 1) + fibo_spec_impl(n - 2)
}

/*
   Ce face sistemul in spate pentru o functie care nu e ghost?

   Genereaza o functie ghost:
ghost function fibo_spec_impl(n : nat) : nat
{
  if (n <= 1) then
    n
  else
    fibo_spec_impl(n - 1) + fibo_spec_impl(n - 2)
}

   Si o metoda care implementeaza functia ghost
method fibo_spec_impl(n : nat) return (result : nat)
  ensures fibo_spec_impl(n) == result   
{
  if (n <= 1) {
   return n;
  } else {
   var temp1 := fibo_spec_impl(n - 1);
   var temp2 := fibo_spec_impl(n - 2);
   return temp1 + temp2;
 }
}

   */

method use_fibo()
{
  var x := fibo_spec_impl(10);
}

method double(x : int) returns (r : int)
  requires x > 0
  ensures r > 0
{
  return x * 2;
}

method use_double(x : int) returns (r : int)
  requires x > 0
  // ensures r == x * 2 // FAILS!
{
  var temp := double(x);
  //assert temp == 2 * x; // doar fiindca e adevarat, nu inseamna ca sistemul "stie" sa demonstreze
                     // problema de verificare e nedecidabila
  return temp;
}

// ideea fundamentala care face verificarea tractabila este o abstractizare

// method use_double(x : int) returns (r : int)
//   requires x > 0
//   ensures r == x * 2 ---> obligatie de verificare (verification obligation, verification condition)
//                           pe care o trimite la un SMT solver                             
/*
   Ce stiu?
   x : int
   x > 0
   r : int
   temp : int
   r == temp
   // noi stim si ca temp == implementarea metodei double, apelata pe x,  temp == 2 * x
   temp > 0
   ------------/
   temp == x * 2
   ------------//
   Raspuns: nu pot demontra!!!
*/
// {
//   var temp := double(x); // --> obligatie de verificare, pentru preconditie (x > 0 ==> x > 0, triviala)
                            // --> noi stim: temp == corpul metodei double, apelata pe x
                            // --> sistemul stie: temp satisface postconditia metodei (temp > 0)
//   //assert temp == 2 * x; // doar fiindca e adevarat, nu inseamna ca sistemul "stie" sa demonstreze
//                      // problema de verificare e nedecidabila
//   return temp;
// }



method double'(x : int) returns (r : int)
  requires x > 0
  ensures r > 0
  ensures r == 2 * x
{
  r := x;
  while (r < 2 * x)
    invariant x <= r <= 2 * x
  {
    r := r + 1;
  }
}

method use_double'(x : int) returns (r : int)
  requires x > 0
  ensures r == x * 2
{
  var temp := double'(x);
  return temp;
}

/*
   seq
   set
   iset
   map
   imap
   tipuri algebrice
 */

// method minArray(a : array<int>) returns (r : int)
//   requires a.Length > 0

method minSeq(s : seq<int>) returns (r : int)
  requires |s| > 0
  // r este mai mic decat orice element din secventa
  ensures forall i :: 0 <= i < |s| ==> r <= s[i] 
{
  var min := s[0];
  var i := 1;
  while (i < |s|)
    invariant 1 <= i <= |s|
    // ce este adevarat despre prefixul de lungime i al secventei?
    // ce legatura este intre min si prefixul de lungime i al secventei?
    // min este mai mic sau egal decat toate elementele de pe pozitiile 0 .. i - 1
    invariant forall j :: 0 <= j < i ==> min <= s[j]
  {
    if (s[i] < min) {
      min := s[i];
    }
    i := i + 1;
  }
  return min;
}

/*
   Invarianti (doua conditii de verificare):

   1. invariantul este adevarat la intrarea in bucla while

   |s| > 0        // |s| >= 1 == i
   min == s[0]
   i == 1
   ----------/
   1 <= i <= |s| /\ forall j :: 0 <= j < i ==> min <= s[j]
   ^^^^^^^^^^^^^    ^^^ j == 0 ^^^^^^     ^^^^^^^^^^^
     trivial                              min <= s[0]

   2. invariantul este adevarat dupa fiecare executie a corpului buclei (pp. ca a fost adev. inainte)
   i, min -> valorile inainte de corpul buclei
   i', min' -> valorile dupa corpul buclei
   
    1 <= i <= |s|
    forall j :: 0 <= j < i ==> min <= s[j]
    s[i] < min ==> min' == s[i]
    s[i] >= min ==> min' == min          // i     <  |s|
    i' == i + 1                    // i' == i + 1 <= |s|
    i < |s|  // din while (i < |s|)
   -------------/
   1 <= i' <= |s| /\ forall j :: 0 <= j < i' ==> min' <= s[j]
   1 <= i' <= |s| /\ forall j :: 0 <= j <= i ==> min' <= s[j]
   ^^^^^^^^^^^^^^    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
                     s[i] < min: --> min' == s[i]
                       0 <= j < i --> min' < min <= s[j]
                       j == i     --> min' <= s[j] == s[i]
                     s[i] >= min: --> min' == min
                       0 <= j < i --> min' == min <= s[j]
                       j == i     --> min' == min <= s[i] == s[j]
   
     
   -------------//
   
  }
   */

// method Main()
// {
//   var x := fibo2(6);
//   print x, "\n";
//   var s1 := [ 6, 3, 7, 4, 10 ];
//   var min := minSeq(s1);
//   print min, "\n";
// }



/*
   Obligatia de verificare pentru postconditie:
   
   1 <= i <= |s|             // i == |s|
   i >= |s|
   forall j :: 0 <= j < i ==> min <= s[j]
   r == min
   -----------------/
   forall i :: 0 <= i < |s| ==> r <= s[i]
   -----------------//
 */

method reverseArray(a : array<int>) returns (r : array<int>)
  ensures r.Length == a.Length
  ensures forall i :: 0 <= i < a.Length ==> r[i] == a[a.Length - 1 - i]
{
  r := new int [ a.Length ];
  /* 
  var i := 0;                      ---> FOR
  while (i < a.Length)
    invariant 0 <= i <= a.Length
   {
     BODY;
    i := i + 1;
     }
   */
  for i := 0 to a.Length
  invariant a.Length == r.Length
  invariant forall j :: 0 <= j < i ==> r[j] == a[a.Length - 1 - j]
  {
    r[i] := a[a.Length - 1 - i];
  }
}



// method reverseArray1(s : seq<int>) returns (r : array<int>)
//   ensures r.Length == |s|
//   ensures forall i :: 0 <= i < |s| ==> s[i] == r[a.Length - 1 - i]
// {
//   r := new int [ a.Length ];
//   /* 
//   var i := 0;
//   while (i < a.Length)
//     invariant 0 <= i <= a.Length
//    {
//      BODY;
//     i := i + 1;
//      }
//    */
//   for i := 0 to a.Length
//   invariant a.Length == r.Length
//   invariant forall j :: 0 <= j < i ==> a[j] == r[a.Length - 1 - j]
//   {
//     r[i] := a[a.Length - 1 - i];
//   }
// }