Before tackling Insertion Sort, you should work through some of the Dafny tutorials, particularly the "Guide" and perhaps "Termination." You will not need anything more advanced for this exercise, and you probably won't even need "Termination."

To show that this is only half of the specification of "sort": Rewrite the body of the sort function so that it initializes the array a to all zeros, and prove that it satisfies the "ensures" specification. Upload that as "sort-bogus.txt".

For the serious among you: Read about Multisets in Dafny. Strengthen the requires/ensures clauses of the sort function to specify that the output array represents the same multiset as the input, and prove that in Dafny. Upload this full specification of sort as "sort-full.txt".

Source code

In case the Dafny Insertion Sort breaks for some reason, then just use the standard Dafny link, and paste in this program:

// Insertion sort exercise, Andrew W. Appel, March 2013, updated April 2018

predicate sorted(a: array,  lo:int, hi:int)
 // Fix the bugs here by filling in some missing lines
 { forall j,k:: lo<=j a[j]<=a[k]}

method sort(a: array)
 // fill in some missing lines here
 ensures sorted(a, 0, a.Length);
 // add enough assertions and invariants below to prove the "ensures"
 {var i: int;
  if (a.Length==0) {return;}
  i:=1;
  while (i < a.Length)
    {if (a[i] < a[0]) 
      {a[0],a[i]:=a[i],a[0];}
     i:=i+1;
    }
     
  i:=1;
  while (i < a.Length)
  {var j : int := i;
   var v : int := a[i];
   while (v < a[j-1])
    { a[j]:=a[j-1];
      j:=j-1;
    }
    a[j]:=v;
    i:=i+1;
  }
}