diff options
| author |  Rustan Leino <unknown> | 2014-04-04 10:58:05 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2014-04-04 10:58:05 -0700 |
| commit | 6c8b9222e5eb724258ddb92662c9fcbe470f1a1d (patch) | |
| tree | c09a504f43d03aaaa8394986265b9a82b5c5056a /Test/dafny0 | |
| parent | e8bae7e26441d2077d33a8b771c7d559eaee5d71 (diff) | |
| parent | 4937d6e714913a2645d3fd00be376ada31057433 (diff) | |
Merge
Diffstat (limited to 'Test/dafny0')
| -rw-r--r-- | Test/dafny0/Answer | 4 | ||||
| -rw-r--r-- | Test/dafny0/DatatypeUpdate.dfy | 21 | ||||
| -rw-r--r-- | Test/dafny0/runtest.bat | 2 |
3 files changed, 26 insertions, 1 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 204f2dcc..517f1182 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -2198,6 +2198,10 @@ Execution trace: Dafny program verifier finished with 25 verified, 11 errors
+-------------------- DatatypeUpdate.dfy --------------------
+
+Dafny program verifier finished with 2 verified, 0 errors
+
-------------------- Superposition.dfy --------------------
Verifying CheckWellformed$$_0_M0.C.M ...
diff --git a/Test/dafny0/DatatypeUpdate.dfy b/Test/dafny0/DatatypeUpdate.dfy new file mode 100644 index 00000000..d78b453c --- /dev/null +++ b/Test/dafny0/DatatypeUpdate.dfy @@ -0,0 +1,21 @@ +
+datatype MyDataType = MyConstructor(myint:int, mybool:bool)
+ | MyOtherConstructor(otherbool:bool)
+ | MyNumericConstructor(42:int);
+
+method test(foo:MyDataType, x:int) returns (abc:MyDataType, def:MyDataType, ghi:MyDataType, jkl:MyDataType)
+ requires foo.MyConstructor?;
+ ensures abc == foo[myint := x + 2];
+ ensures def == foo[otherbool := !foo.mybool];
+ ensures ghi == foo[myint := 2][mybool := false];
+ //ensures jkl == foo[non_destructor := 5]; // Resolution error: no non_destructor in MyDataType
+ ensures jkl == foo[42 := 7];
+{
+ abc := MyConstructor(x + 2, foo.mybool);
+ abc := foo[myint := x + 2];
+ def := MyOtherConstructor(!foo.mybool);
+ ghi := MyConstructor(2, false);
+ jkl := foo[42 := 7];
+
+ assert abc[myint := abc.myint - 2] == foo[myint := x];
+}
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat index a4c3914f..525f6565 100644 --- a/Test/dafny0/runtest.bat +++ b/Test/dafny0/runtest.bat @@ -29,7 +29,7 @@ for %%f in (TypeTests.dfy NatTypes.dfy RealTypes.dfy Definedness.dfy IteratorResolution.dfy Iterators.dfy
RankPos.dfy RankNeg.dfy
Computations.dfy ComputationsNeg.dfy
- Include.dfy AutoReq.dfy ModifyStmt.dfy) do (
+ Include.dfy AutoReq.dfy DatatypeUpdate.dfy ModifyStmt.dfy) do (
echo.
echo -------------------- %%f --------------------
%DAFNY_EXE% /compile:0 /print:out.bpl.tmp /dprint:out.dfy.tmp %* %%f
|