diff options
| author |  Rustan Leino <unknown> | 2013-07-24 06:54:25 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2013-07-24 06:54:25 -0700 |
| commit | 0e41af83b8a0fb4e9d299a173132ab119d1c98dc (patch) | |
| tree | 15f58c730ad3dfba3b40eb2b319f8cf6e1ec6383 /Test/dafny0 | |
| parent | c8a4860260bf2c430e0339760c044d53af9a87eb (diff) | |
Allow field names to be sequences of digits (this is nice, for example, to define a Tuple with fields .0 and .1)
Diffstat (limited to 'Test/dafny0')
| -rw-r--r-- | Test/dafny0/Answer | 2 | ||||
| -rw-r--r-- | Test/dafny0/Compilation.dfy | 21 |
2 files changed, 22 insertions, 1 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 60599a14..c1e04f2a 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -2160,5 +2160,5 @@ Execution trace: Dafny program verifier finished with 28 verified, 2 errors
-Dafny program verifier finished with 26 verified, 0 errors
+Dafny program verifier finished with 30 verified, 0 errors
Compiled assembly into Compilation.exe
diff --git a/Test/dafny0/Compilation.dfy b/Test/dafny0/Compilation.dfy index 9c19a404..5120bf81 100644 --- a/Test/dafny0/Compilation.dfy +++ b/Test/dafny0/Compilation.dfy @@ -127,3 +127,24 @@ method Caller() { var p := new M.public;
var x := p.private;
}
+
+// ----- digits-identifiers for destructors -----
+
+datatype Tuple<T,U> = Pair(0: T, 1: U, r: int, s': int)
+
+method DigitsIdents(t: Tuple<int, Tuple<int, bool>>)
+{
+ var x: int := t.0;
+ var y: bool := t.1.1;
+ var z: int := t.r + t.1.r + t.1.s';
+}
+
+class DigitsClass {
+ var 7: bool;
+ method M(c: DigitsClass)
+ requires c != null;
+ {
+ var x: int := if this.7 then 7 else if c.7 then 8 else 9;
+ }
+}
+
|