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 | 7992533629faca61ea8a3761b2ee21fd6f27ac18 (patch) | |
| tree | 8d17a7165af962ecb71ca9a6e15a59563c13efa4 /Test/dafny0/ControlStructures.dfy | |
| parent | 288ff050fcb1089a75aa5b0f792789ab94efebb7 (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
+}
|