1 2 3 4 5 6 7 8 9 10 11 12
procedure {:checksum "P0$proc#0"} P0(); // Action: verify implementation {:id "P0"} {:checksum "P0$impl#0"} P0() { call P0(); } function F0() : bool { true }