diff options
| author |  Jason Koenig <unknown> | 2011-06-29 17:41:26 -0700 |
|---|---|---|
| committer | Jason Koenig <unknown> | 2011-06-29 17:41:26 -0700 |
| commit | 0c344651c1b3d9b4f1e073980b3c4cc9332a6d54 (patch) | |
| tree | ea05159d30764a53ba709a12ecd0d3e6437890ac /Test/dafny0/ReturnTests.dfy | |
| parent | 6c554ef06d3e90aff8162ca6dcba5ad2e4bc247a (diff) | |
Added regression tests for new return statements with parameters.
Diffstat (limited to 'Test/dafny0/ReturnTests.dfy')
| -rw-r--r-- | Test/dafny0/ReturnTests.dfy | 59 |
1 files changed, 59 insertions, 0 deletions
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 |