diff options
Diffstat (limited to 'Test/dafny0')
| -rw-r--r-- | Test/dafny0/Answer | 10 | ||||
| -rw-r--r-- | Test/dafny0/ReturnErrors.dfy | 42 | ||||
| -rw-r--r-- | Test/dafny0/ReturnTests.dfy | 59 | ||||
| -rw-r--r-- | Test/dafny0/runtest.bat | 3 |
4 files changed, 113 insertions, 1 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index d5107ecd..51d3efcd 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -1090,3 +1090,13 @@ Execution trace: (0,0): anon14
Dafny program verifier finished with 21 verified, 9 errors
+
+-------------------- ReturnErrors.dfy --------------------
+ReturnErrors.dfy(30,10): Error: cannot have method call in return statement.
+ReturnErrors.dfy(36,10): Error: cannot have effectful parameter in multi-return statement.
+ReturnErrors.dfy(41,10): Error: can only have initialization methods which modify at most 'this'.
+3 resolution/type errors detected in ReturnErrors.dfy
+
+-------------------- ReturnTests.dfy --------------------
+
+Dafny program verifier finished with 16 verified, 0 errors
diff --git a/Test/dafny0/ReturnErrors.dfy b/Test/dafny0/ReturnErrors.dfy new file mode 100644 index 00000000..1141808a --- /dev/null +++ b/Test/dafny0/ReturnErrors.dfy @@ -0,0 +1,42 @@ +
+class N
+{
+ var i: int;
+ method newN(n: N)
+ requires n != null;
+ modifies this, n;
+ {
+ n.i := 1;
+ i := 1;
+ }
+ method safe(n: N)
+ requires n != null;
+ modifies this;
+ {
+ i := n.i;
+ }
+}
+
+method m(v: int, n: N) returns (r: int)
+ modifies n;
+ ensures r == v;
+{
+ r := v;
+}
+method testing1() returns (s: int)
+ ensures s == 3;
+{
+ var n := new N;
+ return m(3, n); // methods disallowed.
+}
+method testing2() returns (s: int, b: int)
+ ensures s == 3;
+{
+ var n := new N;
+ return m(3, n), 2; // methods disallowed.
+}
+
+method testing3() returns (n: N)
+{
+ return new N.newN(n); // disallowed, as newN() modifies n
+}
\ No newline at end of file diff --git a/Test/dafny0/ReturnTests.dfy b/Test/dafny0/ReturnTests.dfy new file mode 100644 index 00000000..a4d7fca0 --- /dev/null +++ b/Test/dafny0/ReturnTests.dfy @@ -0,0 +1,59 @@ +
+class N
+{
+ var i: int;
+ method newN(n: N)
+ requires n != null;
+ modifies this, n;
+ {
+ n.i := 1;
+ i := 1;
+ }
+ method safe(n: N)
+ requires n != null;
+ modifies this;
+ {
+ i := n.i;
+ }
+}
+
+method m(v: int, n: N) returns (r: int)
+ modifies n;
+ ensures r == v;
+{
+ r := v; // implict return still works.
+}
+
+method testing1() returns (a: int, b: set<int>)
+{
+ return 1, {1, 2, 3}; // type checking
+}
+method testing2() returns (a: int, b: int)
+ ensures a == 1 && b == 2;
+{
+ a, b := 2, 1;
+ return b, a; // test of parallel assignment.
+}
+method testing3() returns (a: int, b: int)
+ ensures a == 1 && b == 2;
+{
+ a, b := 2, 1; // these are wrong
+ if (true)
+ {
+ var a, b := 3, 4;
+ return 1, 2;// return updates non-shadowed, formal parameters correctly
+ }
+}
+
+method testing4(nnn: N) returns (n: N)
+ requires nnn != null;
+{
+ return new N.safe(nnn); // only modifies 'this', which is the fresh N
+}
+
+method testing5() returns (r: int)
+ ensures r == 2;
+{
+ r := 2;
+ return; // sanity check.
+}
\ No newline at end of file diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat index 3c64f623..f606c183 100644 --- a/Test/dafny0/runtest.bat +++ b/Test/dafny0/runtest.bat @@ -18,7 +18,8 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy Comprehensions.dfy Basics.dfy ControlStructures.dfy
Termination.dfy DTypes.dfy
TypeParameters.dfy Datatypes.dfy TypeAntecedents.dfy SplitExpr.dfy
- Refinement.dfy RefinementErrors.dfy LoopModifies.dfy) do (
+ Refinement.dfy RefinementErrors.dfy LoopModifies.dfy
+ ReturnErrors.dfy ReturnTests.dfy) do (
echo.
echo -------------------- %%f --------------------
%DAFNY_EXE% /compile:0 %* %%f
|