diff options
Diffstat (limited to 'Test/dafny0/DatatypeUpdate.dfy')
-rw-r--r-- | Test/dafny0/DatatypeUpdate.dfy | 21 |
1 files changed, 21 insertions, 0 deletions
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];
+}
|