/* SE 504  Spring 2026
** HW #8: Incomplete Dafny code 
*/


// Utilities
// ---------

function MinOfTwo(x: int, y: int): int
   { if x < y then x else y }


function MaxOfTwo(x: int, y: int): int
   { if x > y then x else y }



// -----------------------
// Problem #1 (from HW# 6)
// -----------------------

ghost function h(n: int): int
{
  if n < 2 then n else h(n-2) - h(n-1)
}

method Compute_h(N: nat) returns (y: int)
  ensures y == h(N)
{
  // To be completed
}


// -----------------------
// Problem #2 (from HW #6)
// -----------------------

/* S(k) is the sum of the first k elements of array b[].
*/
ghost function S(b: array< int >, k: nat): int
  reads b
  requires k <= b.Length
{
  if k == 0 then 0 else S(b, k-1) + b[k-1]
}

/* To use Gries/Schneider notation:
** NumSignChanges(b,n) = (#i | 1 <= i <= n : S(b,i-1) * S(b,i) < 0)
*/
ghost function NumSignChanges(b: array< int >, n: nat): nat
  reads b
  requires n <= b.Length
{
  if n == 0 then 0
  else 12345
  // above line needs correction
}

method ComputeNumSignChanges(b: array<int>) returns (r: nat)
  requires b.Length != 0
  ensures r == NumSignChanges(b, b.Length)
{
  // to be completed
}



// -----------------------
// Problem #3 (from HW #6)
// -----------------------


/* Returns (MAX p,q | 0 <= p <= q < b.Length :: b[q] - b[p])
*/
ghost function MaxDiff(b: array<int>): int
  reads b
  requires b.Length != 0
{
  MaxDiffAux(b, b.Length)
}

/* Returns (MAX p,q | 0 <= p <= q < n :: b[q] - b[p])
*/
ghost function MaxDiffAux(b: array<int>, n: nat): int 
  reads b
  requires b.Length != 0
  requires 0 < n <= b.Length
{
  -99   // to be completed
}

/* True iff b[q] - b[p] = (MAX i,j | 0 <= i <= j < b.Length : b[j] - b[i]).
** That is, the maximum difference between any two elements of b[], where the
** smaller occurs at a non-higher numbered location than the larger, is
** b[q] - b[p].
*/
ghost predicate AreMaxDiffLocs(b: array<int>, p: nat, q: nat) 
  reads b
  requires b.Length != 0
  requires p <= q < b.Length
{
  AreMaxDiffLocsAux(b, p, q, b.Length)
}

/* True iff b[q] - b[p] = (MAX i,j | 0 <= i <= j < n : b[j] - b[i]).
** That is, the maximum difference between any two elements of b[0..n), 
** where the smaller occurs at a non-higher numbered location than the
** larger, is b[q] - b[p].
*/
ghost predicate AreMaxDiffLocsAux(b: array<int>, p: nat, q: nat, n: nat) 
  reads b
  requires b.Length != 0
  requires p <= q < n <= b.Length
{
  forall i,j | 0 <= i <= j < n :: b[q] - b[p] >= b[j] - b[i]
}

/* Lemma that draws a connection between the MaxDiffAux() function
** and the AreMaxDiffLocsAux() predicate.
** Supplying a proof would be outstanding.
** Making use of it as an axiom would be good, too, in order to
** verify the preferred postcondition of method below.
*/
lemma Lemma1(a: array<int>, p: nat, q: nat, n: nat)
  requires a.Length != 0
  requires p <= q < n <= a.Length
  ensures AreMaxDiffLocsAux(a, p, q, n) <==> (a[q] - a[p] == MaxDiffAux(a, n))


method ComputeMaxDiffLocs(b: array<int>) returns (p: nat, q: nat)
  requires b.Length != 0
  ensures p <= q < b.Length
  ensures b[q] - b[p] == MaxDiff(b)
  // Postcondition on next line is preferred, but harder to verify.  Try!
  //ensures AreMaxDiffLocs(b, p, q)
{
  // to be completed
}




// -----------------------
// Problem #4 (from HW #6)
// -----------------------

ghost function H(m: nat, n: nat): nat
{
  if m == 0 then n else H(m-1, 2*n)
}

method ComputeH(M: nat, N: nat) returns (k: nat)
  ensures k == H(M, N)
{
  // to be completed
}



// -----------------------
// Problem #5 (from HW #6)
// -----------------------

ghost function G(n: nat): nat
{
  if n == 0 then 0 else n + G(n-1)
}

method ComputeG(N: nat) returns (k: nat)
  ensures k == G(N)
{
  // to be completed
}




// ----------------------------------
// Problem #6 (Problem #2 from HW #7)
// ----------------------------------

/* Modifies the given array so that each element (except for the last, which
** remains unchanged) is equal to the minimum of its original value and the
** original value of its successor.
*/
method Prob_7_2(b: array<int>)
  modifies b
  requires b.Length != 0
  ensures forall i | 1 <= i < b.Length :: b[i-1] == MinOfTwo(old(b[i-1]), old(b[i]))
  ensures b[b.Length-1] == old(b[b.Length-1])
{
  // to be completed
}

// Alternative to method above:
method Prob_7_2_WithSeq(b: array<int>, ghost bOrig: seq<int>)
  modifies b
  requires b.Length != 0
  requires bOrig == b[..]
  ensures forall i | 1 <= i < b.Length :: b[i-1] == MinOfTwo(bOrig[i-1], bOrig[i])
  ensures b[b.Length-1] == bOrig[b.Length-1]
{
  // to be completed
}



// ----------------------------------
// Problem #7 (Problem #3 from HW #7)
// ----------------------------------

/* Modifies the given array so that each element (except for the first,
** which remains unchanged) is equal to the difference between its
** original value and the original value of its predecessor.
*/
method Prob_7_3(b: array<int>)
  modifies b
  requires b.Length != 0
  ensures forall i | 1 <= i < b.Length :: b[i] == old(b[i]) - old(b[i-1])
  ensures b[0] == old(b[0])
{
  // to be completed
}

// Alternative to method above:
method Prob_7_3_WithSeq(b: array<int>, ghost bOrig: seq<int>)
  modifies b
  requires b.Length != 0
  requires bOrig == b[..]
  ensures forall i | 1 <= i < b.Length :: b[i] == bOrig[i] - bOrig[i-1]
  ensures b[0] == bOrig[0]
{
  // to be completed
}



// ----------------------------------
// Problem #8 (Problem #4 from HW #7)
// ----------------------------------

/* True iff the elements in a[low..high) are in ascending order.
*/
ghost predicate Ascending(a: array<int>, low: nat, high: nat)
  reads a
  requires low <= high <= a.Length
{
  forall i,j | low <= i <= j < high :: a[i] <= a[j]
}

/* True iff every value in a[..p) is <= every value in a[p..]
*/
ghost predicate Boundary(a: array<int>, p: nat)
  reads a
  requires p <= a.Length
{
  forall i,j | 0 <= i < p  &&  p <= j < a.Length :: a[i] <= a[j]
}

/* Returns the index of a maximum element in a[low..high).
*/
method ComputeLocOfMax(a: array<int>, low: nat, high: nat) returns (k: nat)
  requires low < high <= a.Length
  ensures low <= k < high
  ensures forall j | low <= j < high :: a[j] <= a[k]
{
  // to be completed
}

/* Rearranges the elements of the given array so that they are
** in ascending order.
*/
method SelectionSort(b: array<int>, ghost bOrig: array<int>)
  modifies b
  requires b.Length == bOrig.Length
  requires multiset(b[..]) == multiset(bOrig[..])
  ensures Ascending(b, 0, b.Length)
  ensures multiset(b[..]) == multiset(bOrig[..])
{
  var m: nat := b.Length;
  while m != 0
    // loop invariant and bound function information missing
  {
    var k: nat := ComputeLocOfMax(b, 0, m);
    b[k], b[m-1] := b[m-1], b[k];
    m := m-1;
  }
}