1 2 3 4 5 6 7 8 9 10 11 12 13
method M() { N(); assert false; // error } method N() ensures P; predicate P { true }