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
var g:int; procedure {:yields} {:stable} PB() modifies g; { g := g + 1; } procedure {:yields} {:stable} PC() ensures g == 3; { g := 3; yield; assert g == 3; } procedure {:yields} {:stable} PD() { call PC(); assert g == 3; yield; } procedure {:entrypoint} {:yields} Main() { while (true) { call PB() | PC() | PD(); } }