From a3883d573de2619533660f58a8e43f23707adac6 Mon Sep 17 00:00:00 2001
From: Aadi Desai <21363892+supleed2@users.noreply.github.com>
Date: Fri, 16 Dec 2022 14:01:53 +0000
Subject: [PATCH] Add Dafny Task 1 missing comment (T1 answer)

---
 dafny/submission.dfy | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/dafny/submission.dfy b/dafny/submission.dfy
index ee6bfe6..c0063df 100644
--- a/dafny/submission.dfy
+++ b/dafny/submission.dfy
@@ -33,6 +33,11 @@ method countsquares2(n:nat) returns (result:nat)
   }
 }
 
+// countsquares was easier to verify than countsquares2 as the loop invariant
+// was the same as the post-condition of the function, as the value of result
+// after each loop iteration is simply the result of the function call with a
+// smaller input value n.
+
 predicate sorted(A:array<int>)
   reads A;
 {