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 logistics

  1. Install VSCode if you don't have it already.
  2. Install the Dafny extension for VSCode.
  3. If you don't already have .NET installed, VSCode will prompt you to click to install it; go ahead.
  4. Edit a file with a .dfy extension. The first time, you may need to restart VSCode so it sees the new .NET installation.
Notes: Dafny highlighting will look nice in VSCode even if .NET and the Dafny local server are not installed, so beware!

Source code

Here is sort.dfy: 

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

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

method sort(a: array<int>)
 // 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;
  }
}