ensuring does not work with return

[two-heart]

I would expect both examples to work the same way. E.g., by stainless translating the first to the second.

  def getOne(): Int = {
    1
  }.ensuring(res => res == 1)

  def getOne(): Int = {
    return 1
  }.ensuring(res => res == 1)

However, while the first verifies, the second gives the error:

[ Error  ] SubList.scala:43:5: value ensuring is not a member of Nothing
             }.ensuring(res => res == 1)
               ^

Note this is a minimal example. I encountered the problem when trying to prove more complex imperative code, where writing return statements makes more sense than here.

[mario-bucev]

Hello!
The above snippet is rejected by the Scala compiler as well:

-- [E008] Not Found Error: i1362.scala:4:4 -------------------------------------
2 |  def getOne(): Int = {
3 |    return 1
4 |  }.ensuring(res => res == 1)
  |                      ^
  |                      value ensuring is not a member of Nothing
1 error found

This is due to the return being non-local, as discussed here: scala/bug#9838

A workaround would be to extract the definition of getOne() into a new function without postconditions. Note that preconditions would still need to be specified (i.e. duplicated).

In case the function is recursive, things get a bit more spicy because one usually needs the postcondition of the said function to prove things.
For example, if we have this definition:

import stainless.lang._
import stainless.annotation._

// Does not compile
def summed(x: BigInt): BigInt = {
  decreases(x)
  require(x >= 0)
  if (x == 0) return x
  return x + summed(x - 1)
}.ensuring(_ == x * (x + 1) / 2)

we could extract the body of summed as follows:

def summed(x: BigInt): BigInt = {
  decreases(x)
  require(x >= 0)
  summedImpl(x)
}.ensuring(_ == x * (x + 1) / 2)

@inlineOnce // this tells Stainless to inline this function for verification
def summedImpl(x: BigInt): BigInt = {
  require(x >= 0) // duplicated precondition
  if (x == 0) return x
  return x + summed(x - 1) // calls the original function
}