summaryrefslogtreecommitdiff
path: root/Test/dafny0/ControlStructures.dfy
diff options
context:
space:
mode:
authorGravatar Rustan Leino <leino@microsoft.com>2011-05-19 11:53:56 -0700
committerGravatar Rustan Leino <leino@microsoft.com>2011-05-19 11:53:56 -0700
commitde0a78a69aac57b2189caf7d8490975f25aea91a (patch)
treec94831db7e3d99c333afe55d5d586b8147dace31 /Test/dafny0/ControlStructures.dfy
parentb665a914c81085cf3ac4e97ea3c73673cfe8ca4b (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.dfy65
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
+}