supleed2/ELEC70056-HSV-CW1
1
0
Fork 0
mirror of https://github.com/supleed2/ELEC70056-HSV-CW1.git synced 2024-11-10 02:15:47 +00:00
Code Issues Packages Projects Releases Wiki Activity

Dafny Task 1 complete

Browse source
This commit is contained in:
Aadi Desai 2022-11-21 13:50:18 +00:00
parent d2614f4946
commit 30874e2405
No known key found for this signature in database
GPG key ID: CFFFE425830EF4D9
1 changed files with 12 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
dafny/submission.dfy
View file

@ -4,22 +4,30 @@
// Authors: John Wickerson // Authors: John Wickerson
method countsquares(n:nat) returns (result:nat) method countsquares(n:nat) returns (result:nat)
//ensures result == ... ensures result == (n * (n + 1) * (2 * n + 1)) / 6;
{ {
var i := 0; var i := 0;
result := 0; result := 0;
while i < n { while i < n
invariant 0 <= i <= n;
decreases n - i;
invariant result == (i * (i + 1) * (2 * i + 1)) / 6;
{
i := i + 1; i := i + 1;
result := result + i * i; result := result + i * i;
} }
} }
method countsquares2(n:nat) returns (result:nat) method countsquares2(n:nat) returns (result:nat)
// ensures result == ... ensures result == (n * (n + 1) * (2 * n + 1)) / 6;
{ {
var i := n; var i := n;
result := 0; result := 0;
while i > 0 { while i > 0
invariant 0 <= i <= n;
decreases i;
invariant result == ((n * (n + 1) * (2 * n + 1)) / 6) - ((i * (i + 1) * (2 * i + 1)) / 6);
{
result := result + i * i; result := result + i * i;
i := i - 1; i := i - 1;
} }