diff options
| author |  Mike Barnett <mbarnett@microsoft.com> | 2011-05-19 13:26:13 -0700 |
|---|---|---|
| committer | Mike Barnett <mbarnett@microsoft.com> | 2011-05-19 13:26:13 -0700 |
| commit | 03b24df6c2fa4217f74d3cc76785ab6babbe6f2f (patch) | |
| tree | 02004c12ab9b045e00c5f552e5d66a5c76c54e83 /Test/dafny0/ControlStructures.dfy | |
| parent | 0a1cb72eec7026923f21a097e80d161f9c86fb44 (diff) | |
| parent | 9087bb0fbc57c065ce9f0c3d1b1dbf4a67bd4a3d (diff) | |
Merge
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
+}
|