summaryrefslogtreecommitdiff
path: root/Test/dafny0/MatchBraces.dfy.expect
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