diff options
| author |  mikebarnett <unknown> | 2009-07-15 21:03:41 +0000 |
|---|---|---|
| committer | mikebarnett <unknown> | 2009-07-15 21:03:41 +0000 |
| commit | ce1c2de044c91624370411e23acab13b0381949b (patch) | |
| tree | 592539996fe08050ead5ee210c973801611dde40 /Chalice/examples/RockBand.chalice | |
Initial set of files.
Diffstat (limited to 'Chalice/examples/RockBand.chalice')
| -rw-r--r-- | Chalice/examples/RockBand.chalice | 111 |
1 files changed, 111 insertions, 0 deletions
diff --git a/Chalice/examples/RockBand.chalice b/Chalice/examples/RockBand.chalice new file mode 100644 index 00000000..c7a2bba0 --- /dev/null +++ b/Chalice/examples/RockBand.chalice @@ -0,0 +1,111 @@ +// 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
+ {
+ }
+}
|