1 2 3 4 5 6 7
procedure {:checksum "0"} P(); requires 0 != 0; implementation {:id "P"} {:checksum "1"} P() { assert 1 != 1; }