summaryrefslogtreecommitdiff
path: root/Test/dafny0/SumOfCubes.dfy
diff options
context:
space:
mode:
Diffstat (limited to 'Test/dafny0/SumOfCubes.dfy')
-rw-r--r--Test/dafny0/SumOfCubes.dfy2
1 files changed, 1 insertions, 1 deletions
diff --git a/Test/dafny0/SumOfCubes.dfy b/Test/dafny0/SumOfCubes.dfy
index f3359778..e5fe9473 100644
--- a/Test/dafny0/SumOfCubes.dfy
+++ b/Test/dafny0/SumOfCubes.dfy
@@ -49,7 +49,7 @@ class SumOfCubes {
if k == 0 then 0 else GSum(k-1) + k-1
}
- ghost static method Gauss(k: int) returns (r: int)
+ static method Gauss(k: int) returns (r: int)
requires 0 <= k;
ensures r == GSum(k);
{