From c60e0ee3fed306b611f8ab067b57ddb7f1a2d40c Mon Sep 17 00:00:00 2001
From: "Brady J. Garvin" <bgarvin@cse.unl.edu>
Date: Tue, 27 Sep 2022 19:50:16 -0500
Subject: [PATCH] Verified the final algorithm.

---
 demonstration/ECopyValues.dfy | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

diff --git a/demonstration/ECopyValues.dfy b/demonstration/ECopyValues.dfy
index db27048..8f550bc 100644
--- a/demonstration/ECopyValues.dfy
+++ b/demonstration/ECopyValues.dfy
@@ -5,7 +5,16 @@ method CopyValues<T, U>(mapping: map<T, U>, sources: map<T, T>) returns (updated
 {
   var result := map[];
   var remaining := set key | key in mapping :: key;
-  while |remaining| > 0 {
+  while |remaining| > 0
+    invariant
+      forall d | d in remaining ::
+      d in sources ==>
+      sources[d] in mapping
+    invariant
+      forall d | d in remaining ::
+      d !in sources ==>
+      d in mapping
+  {
     var destinationKey :| destinationKey in remaining;
     remaining := remaining - {destinationKey};
     var sourceKey := destinationKey;
-- 
GitLab