Feature/Bug: Ensures clauses of bodiless functions should have reads checks

[MikaelMayer]

trait A {
  var x: int
  function Test(): int
    ensures Test() == x
}

Is not giving any error, and it's impossible to implement such a trait. However, it might be extremely useful, especially in modeling situations when the trait isn't going to be implemented at all, to perform reads checks on the ensures clause.
Reads checks on ensures clauses aren't necessary when the function is provided with a body.