diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-12-19 15:35:32 -0800 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-12-19 15:35:32 -0800 |
| commit | 4e73a3397844fa7802854fd059a32b0c33c46de7 (patch) | |
| tree | 399eaedc8e1f1fc9d4e5ce4b6bacd0c85c22b808 /Test/dafny0/Datatypes.dfy | |
| parent | a0ab18fd4acd127715d273cf8ab163a4086fe359 (diff) | |
Dafny: for a datatype with just one constructor, don't check (but do assume) that destructors are applied only to those values constructed by that one-and-only constructor
Diffstat (limited to 'Test/dafny0/Datatypes.dfy')
| -rw-r--r-- | Test/dafny0/Datatypes.dfy | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/Test/dafny0/Datatypes.dfy b/Test/dafny0/Datatypes.dfy index aff12fda..c4899f38 100644 --- a/Test/dafny0/Datatypes.dfy +++ b/Test/dafny0/Datatypes.dfy @@ -205,6 +205,24 @@ method MatchingDestructor(d: XList) returns (r: XList) r := XCons(5, XNil);
}
+datatype Triple = T(a: int, b: int, c: int); // just one constructor
+datatype TripleAndMore = T'(a: int, b: int, c: int) | NotATriple;
+
+method Rotate0(t: Triple) returns (u: Triple)
+{
+ u := T(t.c, t.a, t.b);
+}
+
+method Rotate1(t: TripleAndMore) returns (u: TripleAndMore)
+{
+ if {
+ case t.T'? =>
+ u := T'(t.c, t.a, t.b);
+ case true =>
+ u := T'(t.c, t.a, t.b); // error: t may be NotATriple
+ }
+}
+
// -------------
method FwdBug(f: Fwd, initialized: bool)
|