// Your goal is to complete this file to a point where the three 'dafny'
// commands shown in the assignment write-up succeed!
// Specifically, add enough 'invariant' lines to the loops so that verification
// goes through.

// This assignment is meant as a warm-up focused on making sure Dafny is
// installed properly, so you should be able to find almost all details in the
// code presented in the first class.

// A _module_ is a unit of related definitions in Dafny.
// We use one to organize your solutions.
module Pset0 {
  // Complete the verification of this small variation on the insertion-sort
  // example from the first class.  In class, we proved a version that sorts an
  // array in *increasing* order, whereas your task here is to prove this
  // version that sorts in *decreasing* order.
  //
  // You should add 'invariant' lines as needed to get Dafny to accept this
  // method as implementing its specification.  The proof doesn't need to be
  // very different from what we saw in class.  We're not expecting you to
  // understand the ins and outs of Dafny yet; this exercise is a nudge to make
  // sure everyone has Dafny installed properly and can write and check simple
  // proofs.
  method InsertionSortDescending(a: array<int>)
    modifies a
    ensures multiset(a[..]) == old(multiset(a[..]))
    ensures forall n, m :: 0 <= n < m < a.Length ==> a[n] >= a[m]
    // Note the one-character change just above, from '<' to '>'!
  {
    for i := 0 to a.Length
    {
      var lowest := i;

      for j := i+1 to a.Length
      {
        // This next line is the only change to the implementation,
        // also replacing '<' with '>'.
        if a[j] > a[lowest] {
          lowest := j;
        }
      }

      var old_i := a[i];
      a[i] := a[lowest];
      a[lowest] := old_i;
    }
  }
}