Closed leonhandreke closed 12 years ago
Even better, try to prove the following program:
function Integer noop(Integer a)
/* troll */ _ensures _return = a
{
return a
}
The postcondition and the following text up to return
are marked green.
When trying to prove the following program, the
_ensures
is colored in green (as it should). However,// troll comment
is also colored. This shouldn't happen.