Pancake annotation positions

[JunmingZhao42]

From a pure usability perspective, the current annotations have to sit inside a function body or a loop body like:

fun main() {
  /@ requires ... @/
  /@ ensures ... @/
 
  // blah..

  while {
    /@ invariant .. @/
  }

}

which works as it is; but a bit counter-intuitive. A nicer way would be to put the annotations outside the bodies.