blob: dfe1215ff50c7ad2ee62302c95c6be9762069d31 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
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
|
