diff options
| author |  rustanleino <unknown> | 2010-06-08 18:05:23 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-06-08 18:05:23 +0000 |
| commit | 2e8f477b81b1c5c6d3c3f600abac3874548a9e4d (patch) | |
| tree | 03e89bdb4df3a689b7217c5e913557c5b6c6df99 /Test/dafny1/SumOfCubes.dfy | |
| parent | 22e67dc18705c19b617678358c8e859349938ac3 (diff) | |
Boogie:
* Look for Z3 versions up to 2.15 (but did not implement a better algorithm for it).
* Added prover-path output as part of /trace flag (that probably isn't the best command-line option for it).
Dafny:
* Split off some tests from Test/dafny0 into Test/dafny1.
* Added Test/dafny1/UltraFilter.dfy.
Diffstat (limited to 'Test/dafny1/SumOfCubes.dfy')
| -rw-r--r-- | Test/dafny1/SumOfCubes.dfy | 106 |
1 files changed, 106 insertions, 0 deletions
diff --git a/Test/dafny1/SumOfCubes.dfy b/Test/dafny1/SumOfCubes.dfy new file mode 100644 index 00000000..b4fab490 --- /dev/null +++ b/Test/dafny1/SumOfCubes.dfy @@ -0,0 +1,106 @@ +class SumOfCubes {
+ static function SumEmUp(n: int, m: int): int
+ requires 0 <= n && n <= m;
+ decreases m - n;
+ {
+ if m == n then 0 else n*n*n + SumEmUp(n+1, m)
+ }
+
+ static method Socu(n: int, m: int) returns (r: int)
+ requires 0 <= n && n <= m;
+ ensures r == SumEmUp(n, m);
+ {
+ call a := SocuFromZero(m);
+ call b := SocuFromZero(n);
+ r := a - b;
+ call Lemma0(n, m);
+ }
+
+ static method SocuFromZero(k: int) returns (r: int)
+ requires 0 <= k;
+ ensures r == SumEmUp(0, k);
+ {
+ call g := Gauss(k);
+ r := g * g;
+ call Lemma1(k);
+ }
+
+ ghost static method Lemma0(n: int, m: int)
+ requires 0 <= n && n <= m;
+ ensures SumEmUp(n, m) == SumEmUp(0, m) - SumEmUp(0, n);
+ {
+ var k := n;
+ while (k < m)
+ invariant n <= k && k <= m;
+ invariant SumEmDown(0, n) + SumEmDown(n, k) == SumEmDown(0, k);
+ {
+ k := k + 1;
+ }
+ call Lemma3(0, n);
+ call Lemma3(n, k);
+ call Lemma3(0, k);
+ }
+
+ static function GSum(k: int): int
+ requires 0 <= k;
+ decreases k;
+ {
+ if k == 0 then 0 else GSum(k-1) + k-1
+ }
+
+ static method Gauss(k: int) returns (r: int)
+ requires 0 <= k;
+ ensures r == GSum(k);
+ {
+ r := k * (k - 1) / 2;
+ call Lemma2(k);
+ }
+
+ ghost static method Lemma1(k: int)
+ requires 0 <= k;
+ ensures SumEmUp(0, k) == GSum(k) * GSum(k);
+ {
+ var i := 0;
+ while (i < k)
+ invariant i <= k;
+ invariant SumEmDown(0, i) == GSum(i) * GSum(i);
+ {
+ call Lemma2(i);
+ i := i + 1;
+ }
+ call Lemma3(0, k);
+ }
+
+ ghost static method Lemma2(k: int)
+ requires 0 <= k;
+ ensures 2 * GSum(k) == k * (k - 1);
+ {
+ var i := 0;
+ while (i < k)
+ invariant i <= k;
+ invariant 2 * GSum(i) == i * (i - 1);
+ {
+ i := i + 1;
+ }
+ }
+
+ static function SumEmDown(n: int, m: int): int
+ requires 0 <= n && n <= m;
+ decreases m;
+ {
+ if m == n then 0 else SumEmDown(n, m-1) + (m-1)*(m-1)*(m-1)
+ }
+
+ ghost static method Lemma3(n: int, m: int)
+ requires 0 <= n && n <= m;
+ ensures SumEmUp(n, m) == SumEmDown(n, m);
+ {
+ var k := n;
+ while (k < m)
+ invariant n <= k && k <= m;
+ invariant SumEmUp(n, m) == SumEmDown(n, k) + SumEmUp(k, m);
+ {
+ k := k + 1;
+ }
+ }
+}
|