class Cell { var val: int } channel Ch(c: Cell) where c != null ==> acc(c.val) && 0 <= c.val && credit(this) class Program { method Main() { var ch := new Ch fork tk0 := Producer(ch) fork tk1 := Consumer(ch) join tk0 join tk1 } method Producer(ch: Ch) requires ch != null ensures credit(ch) { var i := 0 while (i < 25) { var x := i*i var c := new Cell { val := x } send ch(c) i := i + 1 } send ch(null) } method Consumer(ch: Ch) requires rd(ch.mu) && waitlevel << ch.mu requires credit(ch) ensures rd(ch.mu) { var c: Cell receive c := ch while (c != null) invariant rd(ch.mu) && waitlevel << ch.mu invariant c != null ==> acc(c.val) && 0 <= c.val && credit(ch) { var i := c.val receive c := ch } } }