diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-05-19 11:53:56 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-05-19 11:53:56 -0700 |
| commit | de0a78a69aac57b2189caf7d8490975f25aea91a (patch) | |
| tree | c94831db7e3d99c333afe55d5d586b8147dace31 /Test/dafny0/ControlStructures.dfy | |
| parent | b665a914c81085cf3ac4e97ea3c73673cfe8ca4b (diff) | |
Dafny: let verifier, not the resolver, check for missing cases in match expressions/statements
Diffstat (limited to 'Test/dafny0/ControlStructures.dfy')
| -rw-r--r-- | Test/dafny0/ControlStructures.dfy | 65 |
1 files changed, 65 insertions, 0 deletions
diff --git a/Test/dafny0/ControlStructures.dfy b/Test/dafny0/ControlStructures.dfy new file mode 100644 index 00000000..eed74634 --- /dev/null +++ b/Test/dafny0/ControlStructures.dfy @@ -0,0 +1,65 @@ +datatype D = Green | Blue | Red | Purple;
+
+method M0(d: D)
+{
+ match (d) { // error: two missing cases: Blue and Purple
+ case Green =>
+ case Red =>
+ }
+}
+
+method M1(d: D)
+ requires d != #D.Blue;
+{
+ match (d) { // error: missing case: Purple
+ case Green =>
+ case Red =>
+ }
+}
+
+method M2(d: D)
+ requires d != #D.Blue && d != #D.Purple;
+{
+ match (d) {
+ case Green =>
+ case Red =>
+ }
+}
+
+method M3(d: D)
+ requires d == #D.Green;
+{
+ if (d != #D.Green) {
+ match (d) {
+ // nothing here
+ }
+ }
+}
+
+method M4(d: D)
+ requires d == #D.Green || d == #D.Red;
+{
+ if (d != #D.Green) {
+ match (d) { // error: missing case Red
+ // nothing here
+ }
+ }
+}
+
+function F0(d: D): int
+{
+ match (d) // error: missing cases Red
+ case Purple => 80
+ case Green => 0
+ case Blue => 2
+}
+
+function F1(d: D, x: int): int
+ requires x < 100;
+ requires d == #D.Red ==> x == 200; // (an impossibility, given the first precondition, so d != Red)
+{
+ match (d)
+ case Purple => 80
+ case Green => 0
+ case Blue => 2
+}
|