Verified most algorithms in Week 5 of class.

demonstration/AMinimumOfThree.dfy

@@ -5,10 +5,10 @@ method MinimumOfThree(first: real, second: real, third: real) returns (minimum:
   ensures minimum <= third
 {
   var result := first;
-  if second < first && second < third {
+  if second <= first && second <= third {
     result := second;
   }
-  if third < first && third < second {
+  if third <= first && third <= second {
     result := third;
   }
   return result;

demonstration/BCountLeadingZeros.dfy

@@ -6,7 +6,12 @@ method CountLeadingZeros(sequence: seq<nat>) returns (count: nat)
   ensures count < |sequence| ==> sequence[count] != 0
 {
   var index := 0;
-  while index < |sequence| {
+  while index < |sequence|
+    invariant index <= |sequence|
+    invariant
+      forall i | 0 <= i < index ::
+      sequence[i] == 0
+  {
     if sequence[index] != 0 {
       break;
     }

demonstration/CListToSet.dfy

@@ -7,9 +7,16 @@ method ListToSet<T>(list: seq<T>) returns (asSet: set<T>)
 {
   var result := {};
   var index := 0;
-  while index < |list| {
+  while index < |list|
+    invariant |result| == index
+    invariant
+      forall i | index <= i < |list| ::
+      list[i] !in result
+    invariant index <= |list|
+  {
     result := result + {list[index]};
     index := index + 1;
   }
+  assert index == |list|;
   return result;
 }

demonstration/DSetToList.dfy

@@ -6,7 +6,12 @@ method SetToList<T>(collection: set<T>) returns (asList: seq<T>)
 {
   var result := [];
   var remaining := collection;
-  while |remaining| > 0 {
+  while |remaining| > 0
+    invariant |result| == |collection| - |remaining|
+    invariant
+      forall x | x in collection - remaining ::
+      x in result
+  {
     var element :| element in remaining;
     remaining := remaining - {element};
     result := result + [element];

practice/CMapOverSequence.dfy

@@ -6,7 +6,13 @@ method MapOverSequence<T, U>(f: T -> U, inputs: seq<T>) returns (outputs: seq<U>
 {
   var results := [];
   var index := 0;
-  while index < |inputs| {
+  while index < |inputs|
+    invariant |results| == index
+    invariant index <= |inputs|
+    invariant
+      forall i | 0 <= i < |results| ::
+      results[i] == f(inputs[i])
+  {
     results := results + [f(inputs[index])];
     index := index + 1;
   }

practice/DReverse.dfy

@@ -6,7 +6,13 @@ method Reverse<T>(list: seq<T>) returns (reversed: seq<T>)
 {
   var result := [];
   var index := |list|;
-  while index > 0 {
+  while index > 0
+    invariant |result| == |list| - index
+    invariant index >= 0
+    invariant
+      forall i | 0 <= i < |result| ::
+      result[i] == list[|list| - i - 1]
+  {
     index := index - 1;
     result := result + [list[index]];
   }