feature request: naming function return values

[Chris-Hawblitzel]

Dafny methods have named return values, while Dafny function return values are anonymous:

method m(x:int, y:int) returns(z:int)
function f(x:int, y:int):int

This is nice and concise when you never have to refer to the return value by name. But sometimes you need to refer to the return value in an ensures clause. Currently, this is done by referring to the whole function call applied to its arguments:

method m(x:int, y:int) returns(z:int)
  ensures z >= 10
  ensures isEven(z)

function f(x:int, y:int):int
  ensures f(x, y) >= 10
  ensures isEven(f(x, y))

There are two issues with writing a call like "f(x, y)" in ensures clauses. First, the call is often very long to write -- not just "f(x, y)", but "myverylongfunctionname(myverylongargument1, myverylongargument2, myverylongargument3)". This can be mitigated somewhat by binding the return value to a shorter name using a "var" (let) expression, but this doesn't work across multiple ensures clauses. Second, when Dafny sees the function call "f(x, y)" in an ensures clause, it tags the function as recursive, which brings in extra machinery for layers and fuel.

These two issues could be solved independently. But both issues could be solved together with an optional named return value, something like:

function f(x:int, y:int):(z:int)
function f(x:int, y:int) returns(z:int)
function f(x:int, y:int)->z:int

Boogie, for example, already supports optional named return values from functions.

[RustanLeino]

Let's go with the syntax in the first suggestion above, namely:

function f(x:int, y:int): (z:int)

The identifier z will then be in the scope in the postcondition of f, but nowhere else. (The same will be true for twostate functions.) The name z must be different from the names of the other formal arguments. In a refinement module, if f is repeated, then the renaming rules for z should be analogous to the renaming rules of x and y, and the refining module should be allowed to name or not name the result value regardless of what the refined module did not f.

A function that declares a name for its result value should still be allowed to call itself in the postcondition like before. In other words, the function f above should be allowed to mention both z and f(x, y) in the postcondition (and these refer to the same value--a good test case).

If there's a way for Dafny not to mark the "I'm just trying to denote the result value"-calls that Chris mentions as recursive, that would be great. As it stands now, the Dafny front end cannot tell the difference, but instead this is relegated to a semantic check done by the verifier. I suggest the following improvement, which at least would cover the most common case: For a function F declared with parameters x and y, say, then, for the purpose of marking F as being recursive, ignore calls to F in the postcondition of F if the actual parameters of the call are (IdentifierExpr's denoting) exactly the formal parameters of F. For example, by this simple and coarse-grained proposed rule, a call F(x, y) (where x and y are still referring to the formals and have not been shadowed by bound variables with the same names) would be ignored for the purpose of figuring out whether or not F is recursive, but a call F((x), y) or F(x, y+0) would still cause F to be marked as recursive.

Thanks,
Rustan