Verified the final algorithm.

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;