Förslag till invarianter till programmen från föreläsning 5.

Vissa av invarianterna är förenklade och därmed inte fullständigt
matematiskt/logiskt riktiga, men det ska inte vara något problem 
att med hjälp av dom bli övertygad om att programmen är korrekta.



InsertionSort(v[1..n]) =
POST v[1..n] sorterad, v[1..n] permutation av indata
for i:=2 to n do
   INV v[1..i-1] sorterad, v[1..n] permutation av indata
   x:=v[i]
   j:=i
   while j>1 and v[j-1]>x do
      INV v[1..j-1] sorterad, v[j+1..i] sorterad, v[j-1]<=v[j+1], x<v[j+1], perm
      v[j]:=v[j-1]
      j:=j-1
   v[j]:=x



SelectionSort(v[1..n]) =
POST v[1..n] sorterad, v[1..n] permutation av indata
for i:=1 to n-1 do
   INV v[1..i-1] sorterad, v[i-1]<=alla element i v[i..n], permutation
   mini:=i
   for j:=i+1 to n do
      INV v[mini] minsta elementet i v[i..j-1], permutation
      if v[j]<v[mini] then mini:=j
   tmp:=v[i]
   v[i]:=v[mini]
   v[mini]:=tmp