1 2 3 4 5 6 7 8 9 10 11 12 13 14 15
var g: int; procedure main() modifies g; { g := 0; call foo(); assert g == 1; } procedure foo() modifies g; { g := g + 1; }