diff --git a/demonstration/AMinimumOfThree.dfy b/demonstration/AMinimumOfThree.dfy
index 5b779003eef62bc0a1230fa9c3ad85b8fd71bbf3..6d2d8190260f6bbcf98dc535d8e36e320e49ad34 100644
--- a/demonstration/AMinimumOfThree.dfy
+++ b/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;
diff --git a/demonstration/BCountLeadingZeros.dfy b/demonstration/BCountLeadingZeros.dfy
index e002aafe5e69d6aaca9bd2c5bff602f006f3f3b4..1442c30542309a4604e1c791481f00e2408e58a0 100644
--- a/demonstration/BCountLeadingZeros.dfy
+++ b/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;
     }
diff --git a/demonstration/CListToSet.dfy b/demonstration/CListToSet.dfy
index 6e474654440df3a3d02745fee5dcadd825a079a0..6d4e0aba1820fd93b7e82164f0a0c8f72504f687 100644
--- a/demonstration/CListToSet.dfy
+++ b/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;
 }
diff --git a/demonstration/DSetToList.dfy b/demonstration/DSetToList.dfy
index e218635878bbf0fd4cbb200e9ece44f7f0099fd0..0f91635ea5b34a5a5f18578079c47e787e7e4b8d 100644
--- a/demonstration/DSetToList.dfy
+++ b/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];
diff --git a/practice/CMapOverSequence.dfy b/practice/CMapOverSequence.dfy
index f0237aab46c73ad167fee473b3391fc4e218c6f3..545df64c0d5d484b10b427296fd066cf04956c52 100644
--- a/practice/CMapOverSequence.dfy
+++ b/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;
   }
diff --git a/practice/DReverse.dfy b/practice/DReverse.dfy
index f25c41abd3ec8e2adff00f5c0c61757ec90b9aec..d2ebea4618d96e868a86644bf4c9782cddf2dc95 100644
--- a/practice/DReverse.dfy
+++ b/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]];
   }