Before tackling Insertion Sort, you should work through some of the Dafny tutorials, particularly the Guide. Copy-paste those examples into Dafny and try them out. You will not need anything more advanced for this exercise.

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.dfy".

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.dfy".

VSCode installation

If you'd like to use Dafny in your own VSCode installation, follow these instructions. In particular, do the following steps:

Notes: Dafny highlighting will look nice in VSCode even if .NET and the Dafny local server are not installed, so beware! Also, in my own Windows installation of VSCode, which is already using WSL2/Ubuntu for serving OCaml, I wasn't sure whether to install the Linux .NET on WSL2 or the Windows native .NET, so I just used the gitpod in-the-browser Dafny that's suggested above.

Source code

If you are using your own VSCode/Dafny installation, here's the Sort exercise that you can copy-past as sort.dfy:

// 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;
  }
}