diff options
| author |  Dan Rosén <danr@chalmers.se> | 2014-07-07 17:24:46 -0700 |
|---|---|---|
| committer | Dan Rosén <danr@chalmers.se> | 2014-07-07 17:24:46 -0700 |
| commit | 661faf59f8e1003cdbf339260d1293e8dd77f2df (patch) | |
| tree | 37e11e8a86658fe4d69b38572f3b6fadd8d287c9 /Test/dafny0/MatchBraces.dfy.expect | |
| parent | 8de9fcae1a91acce9a1e59f292f05a95c81b3dbc (diff) | |
| parent | 93d9965a347b1a6ad70007822f01c2b032ea5436 (diff) | |
Merge
Diffstat (limited to 'Test/dafny0/MatchBraces.dfy.expect')
| -rw-r--r-- | Test/dafny0/MatchBraces.dfy.expect | 121 |
1 files changed, 121 insertions, 0 deletions
diff --git a/Test/dafny0/MatchBraces.dfy.expect b/Test/dafny0/MatchBraces.dfy.expect new file mode 100644 index 00000000..dfe1215f --- /dev/null +++ b/Test/dafny0/MatchBraces.dfy.expect @@ -0,0 +1,121 @@ +// MatchBraces.dfy
+
+datatype Color = Red | Green | Blue
+
+method M(c: Color, d: Color)
+{
+ var x := match c case Red => 5 case Green => 7 case Blue => 11;
+ var y := match c case Red => 0.3 case Green => (match d case Red => 0.18 case Green => 0.21 case Blue => 0.98) case Blue => 98.0;
+ var z := match c case Red => Green case Green => match d { case Red => Red case Green => Blue case Blue => Red } case Blue => Green;
+ var w := match c { case Red => 2 case Green => 3 case Blue => 4 } + 10;
+ var t := match c case Red => 0 case Green => match d { case Red => 2 case Green => 2 case Blue => 1 } + (match d case Red => 10 case Green => 8 case Blue => 5) case Blue => match d { case Red => 20 case Green => 20 case Blue => 10 } + match d case Red => 110 case Green => 108 case Blue => 105;
+}
+
+function Heat(c: Color): int
+{
+ match c
+ case Red =>
+ 10
+ case Green =>
+ 12
+ case Blue =>
+ 14
+}
+
+function IceCream(c: Color): int
+{
+ match c {
+ case Red =>
+ 0
+ case Green =>
+ 4
+ case Blue =>
+ 1
+ }
+}
+
+function Flowers(c: Color, d: Color): int
+{
+ match c {
+ case Red =>
+ match d {
+ case Red =>
+ 0
+ case Green =>
+ 1
+ case Blue =>
+ 2
+ }
+ case Green =>
+ match d { case Red => 3 case Green => 3 case Blue => 2 } + 20
+ case Blue =>
+ match d { case Red => 9 case Green => 8 case Blue => 7 } + match d case Red => 23 case Green => 29 case Blue => 31
+ }
+}
+
+method P(c: Color, d: Color)
+{
+ var x: int;
+ match c {
+ case Red =>
+ x := 20;
+ case Green =>
+ case Blue =>
+ }
+ match c
+ case Red =>
+ match d {
+ case Red =>
+ case Green =>
+ case Blue =>
+ }
+ case Green =>
+ var y := 25;
+ var z := y + 3;
+ case Blue =>
+ {
+ var y := 25;
+ var z := y + 3;
+ }
+ match d
+ case Red =>
+ case Green =>
+ x := x + 1;
+ case Blue =>
+}
+
+lemma HeatIsEven(c: Color)
+ ensures Heat(c) % 2 == 0;
+{
+ match c
+ case Red =>
+ assert 10 % 2 == 0;
+ case Green =>
+ assert 12 % 2 == 0;
+ case Blue =>
+}
+
+method DegenerateExamples(c: Color)
+ requires Heat(c) == 10;
+{
+ match c
+ case Red =>
+ case Green =>
+ match c {
+ }
+ case Blue =>
+ match c
+}
+
+method MoreDegenerateExamples(c: Color)
+ requires Heat(c) == 10;
+{
+ if c == Green {
+ var x: int := match c;
+ var y: int := match c { };
+ var z := match c case Blue => 4;
+ }
+}
+
+Dafny program verifier finished with 13 verified, 0 errors
+Compiled assembly into MatchBraces.dll
|