Guarded-by Monitor Invariant

A client of a sorted list that acquires a monitor (lock) before changing the list. The first monitor invariant requires the list to be sorted; the second is a two-state invariant and requires the changed flag to be set whenever a thread changes the content of the list between acquiring and releasing the monitor.

field changed: Bool field l: Ref field held: Int method test(this: Ref, e1: Int, e2: Int) ensures [true, forperm[held] r :: false] { // acquire l inhale acc(this.l) && acc(this.l.data) && acc(this.changed) && sorted(this.l.data) inhale acc(this.held) label acq var tmp: Int tmp := insert(this.l, e1) tmp := insert(this.l, e2) assert this.l.data[0] <= this.l.data[1] this.changed := true // release l exhale acc(this.l) && acc(this.l.data) && acc(this.changed) && sorted(this.l.data) && (old[acq](this.l.data) == this.l.data || this.changed) exhale acc(this.held) } /***** Code from Figure 2 *****/ field data: Seq[Int] define sorted(s) forall i: Int, j: Int :: 0 <= i && i < j && j < |s| ==> s[i] <= s[j] method insert(this: Ref, elem: Int) returns (idx: Int) requires acc(this.data) && sorted(this.data) ensures acc(this.data) && sorted(this.data) ensures 0 <= idx && idx <= old(|this.data|) ensures this.data == old(this.data)[0..idx] ++ Seq(elem) ++ old(this.data)[idx..] { idx := 0 while(idx < |this.data| && this.data[idx] < elem) invariant acc(this.data, 1/2) invariant 0 <= idx && idx <= |this.data| invariant forall i: Int :: 0 <= i && i < idx ==> this.data[i] < elem { idx := idx + 1 } this.data := this.data[0..idx] ++ Seq(elem) ++ this.data[idx..] }