diff options
| author |  rustanleino <unknown> | 2010-05-13 19:02:06 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-05-13 19:02:06 +0000 |
| commit | a660fb79bf527b42e3238b1810143f4fc3f3b827 (patch) | |
| tree | 49ab2f1cdd38b97aaf8af0504fd32a986bbdd20f /Test | |
| parent | f34f3551a17f9971231cd5c8fec8f27b6f9337b7 (diff) | |
Dafny:
* Effectively make all in- and out-parameters of ghost methods ghosts.
* Added DafnyRuntime.cs back in, which is needed to run Dafny programs, but which, unfortunately, is currently not being used in the test suite (something we should address)
Diffstat (limited to 'Test')
| -rw-r--r-- | Test/dafny0/Answer | 3 | ||||
| -rw-r--r-- | Test/dafny0/Modules0.dfy | 16 | ||||
| -rw-r--r-- | Test/dafny0/SumOfCubes.dfy | 2 |
3 files changed, 19 insertions, 2 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 7ac8ff37..726a6c13 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -273,7 +273,8 @@ Modules0.dfy(51,6): Error: inter-module calls must follow the module import rela Modules0.dfy(62,6): Error: inter-module calls must follow the module import relation (so module X1 must transitively import X2)
Modules0.dfy(72,6): Error: inter-module calls must follow the module import relation (so module X0 must transitively import X1)
Modules0.dfy(91,4): Error: inter-module calls must follow the module import relation (so module _default must transitively import YY)
-7 resolution/type errors detected in Modules0.dfy
+Modules0.dfy(116,16): Error: ghost variables are allowed only in specification contexts
+8 resolution/type errors detected in Modules0.dfy
-------------------- Modules1.dfy --------------------
Modules1.dfy(55,3): Error: decreases expression must be bounded below by 0
diff --git a/Test/dafny0/Modules0.dfy b/Test/dafny0/Modules0.dfy index 0e0d3ab3..3e8d1e25 100644 --- a/Test/dafny0/Modules0.dfy +++ b/Test/dafny0/Modules0.dfy @@ -104,3 +104,19 @@ method ProcG(g: ClassG) { call g.T(); // allowed: intra-module call
var t := g.TFunc(); // allowed: intra-module call
}
+
+// ---------------------- some ghost stuff ------------------------
+
+class Ghosty {
+ method Caller() {
+ var x := 3;
+ ghost var y := 3;
+ call Callee(x, y); // fine
+ call Callee(x, x); // fine
+ call Callee(y, x); // error: cannot pass in ghost to a physical formal
+ call Theorem(x); // fine
+ call Theorem(y); // fine, because it's a ghost method
+ }
+ method Callee(a: int, ghost b: int) { }
+ ghost method Theorem(a: int) { }
+}
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);
{
|