summaryrefslogtreecommitdiff
path: root/Chalice/tests/examples/RockBand.chalice
blob: 379b41135e082ecd5933e051b6ad33d975501a6a (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
// chalice-parameter=-checkLeaks -defaults -autoFold
// verify this program with -checkLeaks -defaults -autoFold

class Client {
  method Main() {
    var b := new RockBand
    call b.Init()
    call b.Play()
    call b.Play()
    call b.Dispose()
  }
}

class RockBand module M {
  var gigs: int
  var gt: Guitar
  var doowops: seq<Vocalist>
  var b3: Organ
  predicate Valid {
    acc(gigs) && 0 <= gigs &&
    acc(gt) && gt != null && gt.Valid &&
    acc(gt.mu) &&  // to enable an eventual free
    acc(doowops) && //forall d: Vocalist in doowops :: d != null && d.Valid} &&
    acc(b3) && b3 != null && b3.Valid &&
    acc(b3.mu)  // to enable an eventual free
  }

  method Init()
    requires acc(this.*)
    ensures Valid
  {
    gigs := 0
    gt := new Guitar
    call gt.Init()
    b3 := new Organ
    call b3.Init()
  }

  method Dispose()
    requires Valid && acc(mu)
  {
    call gt.Dispose()
    call b3.Dispose()
    free this
  }

  method Play()
    requires Valid
    ensures Valid
  {
    gigs := gigs + 1
    call gt.Strum()
    call b3.Grind()
  }
}

class Guitar module Musicians {
  predicate Valid { true }
  method Init()
    requires acc(this.*)
    ensures Valid
  {
  }
  method Dispose()
    requires Valid && acc(mu)
  {
    free this
  }
  method Strum()
    requires Valid
    ensures Valid
  {
  }
}

class Vocalist module Musicians {
  predicate Valid { true }
  method Init()
    requires acc(this.*)
    ensures Valid
  {
  }
  method Dispose()
    requires Valid && acc(mu)
  {
    free this
  }
  method Strum()
    requires Valid
    ensures Valid
  {
  }
}

class Organ module Musicians {
  predicate Valid { true }
  method Init()
    requires acc(this.*)
    ensures Valid
  {
  }
  method Dispose()
    requires Valid && acc(mu)
  {
    free this
  }
  method Grind()
    requires Valid
    ensures Valid
  {
  }
}