// Work done in lecture on April 22, 2025 to illustrate Dafny


// Solution to Problem 1 of HW #3: 

// Recursive definition of function f, as given.
function f(k: nat): int
{
    if k == 0 then 1
    else if k == 1 then 2
    else 5*f(k-1) - 6*f(k-2)
}

// Method to implement function f.
method Compute_f(N: nat) returns (current: int)
   ensures current == f(N)
{
   var i: nat := 0;
   var next: int := 2;
   current := 1;
   while i != N 
      decreases N-i
      invariant i <= N
      invariant current == f(i)
      invariant next == f(i+1)
   {
      current, next := next, 5*next - 6*current;
      i := i+1;
   }
}


// ----------------------------------------------------
// Solution to a variation of Problem 2 of HW #3.
// Here the sum of the integers in the range [0..Y)
// is computed in a straightforward way, rather than in
// the roundabout way that the given program does it.

// Yields (+i | low <= i < high : i), i.e., the sum of the integers
// in the range [low..high).
function sumOfRange(low: int, high: int): int
   requires low <= high
   decreases high - low
{
   if low == high then 0  // empty range
   //else low + sumOfRange(low+1, high)
   else sumOfRange(low,high-1) + high-1
}

/* Computes the sum of the integers in the range [0..Y) and
** returns it in output variable z.
*/
method ComputeSumToY(Y: nat) returns (z: nat)
   ensures z == sumOfRange(0,Y)
{
   var i: nat := 0;
   z := 0;
   while i != Y
      decreases Y - i
      invariant 0 <= i <= Y
      invariant z == sumOfRange(0,i) 
   {
      i,z := i+1, z+i;
   }
}


// -------------------------------------------
// Solution to a variation of Problem 3 of HW #3, which
// is to identify the maximum element in a given array.

/* Yields true iff 'val' is the maximum value in b[low..high)
*/
predicate isMaxInArraySeg(b: array<int>, low: nat, high: nat, val: int)
   reads b 
   requires 0 <= low <= high <= b.Length
{
   (forall j | low <= j < high :: b[j] <= val) &&
   (exists j | low <= j < high :: b[j] == val)

}

/* Returns the maximum value in the given array (in the output
** variable 'biggest').
*/
method ComputeArrayMax(b: array<int>) returns (biggest: int)
   requires b.Length != 0
   ensures isMaxInArraySeg(b, 0, b.Length, biggest)
   // Alternatively, we could avoid using the isMaxInArraySeg()
   // function by including the two "ensures" clauses below.
   //ensures forall j | 0 <= j < b.Length :: b[j] <= biggest
   //ensures exists j | 0 <= j < b.Length :: biggest == b[j]
{
   var k: nat := 1;
   biggest := b[0];
   while k != b.Length 
      decreases b.Length - k
      invariant 1 <= k <= b.Length
      invariant isMaxInArraySeg(b, 0, k, biggest)
      // Alternatively, we could use the two invariants below
      // rather than using the isMaxInArraySeg() function
      //invariant forall j | 0 <= j < k :: b[j] <= biggest
      //invariant exists j | 0 <= j < k :: b[j] == biggest
   {
      if b[k] > biggest { biggest := b[k]; }
      k := k+1;
   }
}


// ---------------------------------------------------
// Solution to Problem 1 of HW #5:

/* Yields the maximum of its two arguments.
*/
function maxOf(x: int, y:int): int
{ if x >= y then x else y }

/* Yields the minimum of its two arguments.
*/
function minOf(x: int, y: int): int
{ if x <= y then x else y }

/* Tail-recursive definition of the H function.
*/
function H(m: nat, n: nat): nat
{
   if minOf(m,n) == 0 then maxOf(m,n)
   else H(m-1,n-1)
}

/* Computes H(M,N), placing the value in output variable k.
*/
method ComputeH(M: nat, N: nat) returns (k: nat)
   ensures k == H(M,N)
{
   var m: nat := M;
   var n: nat := N;
   while minOf(m,n) != 0 
      decreases m
      // Alternative bound functions:
      //decreases n
      //decreases minOf(m,n)
      //decreases maxOf(m,n)
      invariant H(m,n) == H(M,N)
   {
      m,n := m-1,n-1;
   }
   k := maxOf(m,n);
}


// ---------------------------------------------------
// Solution to Problem 2 of HW #5:

/* Pseudo-tail recursive definition of function G.
*/
function G(n: nat): nat
{
   if n == 0 then 0
   else 2 + G(n-1)
}

// Interesting...here I've defined G' directly from G
// rather than using the tail recursive definition (which is
// commented out).  Dafny verifies computeG() either way,
// but see remark there.
function G'(n: nat, k: nat): nat
{
  k + G(n)
  //if n == 0 then k
  //else G'(n-1,k+2)
}

/* Computes G(N) and puts value into output variable k.
*/
method computeG(N: nat) returns (k: nat) 
   ensures k == G(N) == G'(N,0)
{
   var n: nat := N;
   k := 0;
   while n != 0
      decreases n
      // Note: the equivalence G'(n,k) == k + G(n) below cannot be verified
      //       by Dafny if the tail recursive definition of G' is used.
      invariant G'(N,0) == G'(n,k) == k + G(n) == G(N)
      invariant G(N) == k + G(n)
   {
      n,k := n-1, k+2;
   }
}



// -----------------------------------------------
// Solution to the Prefix Sums problem:


/* Yields the sum of the elements in s[0..n]
*/
function prefixSumSeq(s: seq<int>, n: nat) : int
  requires 0 <= n < |s|
  decreases n
{
  if n == 0 then s[0] else prefixSumSeq(s, n-1) + s[n]
}

/* Computes the prefix sums of the given array "in place".
*/
method ComputePrefixSumsInPlace(a : array<int>, ghost oldA: seq<int>)
  modifies a
  requires a.Length != 0
  requires |oldA| == a.Length
  requires oldA[0..|oldA|] == a[0..a.Length]
  ensures forall i | 0 <= i < a.Length :: a[i] == prefixSumSeq(oldA,i)
{
  var n : nat := 1;
  while n != a.Length
    decreases a.Length - n
    invariant 1 <= n <= a.Length
    invariant oldA[n..] == a[n..]
    // The expression below means the same thing as the one above.
    //invariant forall j | n <= j < a.Length :: oldA[j] == a[j]
    invariant forall i | 0 <= i < n :: a[i] == prefixSumSeq(oldA,i)
  {
    n, a[n] := n+1, a[n-1] + a[n];
  }
}