From 89e43a3a05c428506420530ecd349e42401b576e Mon Sep 17 00:00:00 2001
From: "Brady J. Garvin" <bgarvin@cse.unl.edu>
Date: Thu, 22 Sep 2022 17:16:56 -0500
Subject: [PATCH] Verified most algorithms in Week 5 of class.

---
 demonstration/AMinimumOfThree.dfy    | 4 ++--
 demonstration/BCountLeadingZeros.dfy | 7 ++++++-
 demonstration/CListToSet.dfy         | 9 ++++++++-
 demonstration/DSetToList.dfy         | 7 ++++++-
 practice/CMapOverSequence.dfy        | 8 +++++++-
 practice/DReverse.dfy                | 8 +++++++-
 6 files changed, 36 insertions(+), 7 deletions(-)

diff --git a/demonstration/AMinimumOfThree.dfy b/demonstration/AMinimumOfThree.dfy
index 5b77900..6d2d819 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 e002aaf..1442c30 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 6e47465..6d4e0ab 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 e218635..0f91635 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 f0237aa..545df64 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 f25c41a..d2ebea4 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]];
   }
-- 
GitLab