Add Dafny Task 1 missing comment (T1 answer)

This commit is contained in:
Aadi Desai 2022-12-16 14:01:53 +00:00
parent a926e4e941
commit a3883d573d
No known key found for this signature in database
GPG key ID: CFFFE425830EF4D9

View file

@ -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;
{