Refinement from recursion to loop?

[mschwerhoff]

Does Dafny provide any refinement constructs, in the spirit of "module B refines module A", for replacing a recursive implementation with a loop?

As illustration, consider the following simple example with two implementations of the Fibonacci function:

function fib_rec(n: nat): nat {
	if n <= 1 then n else fib_rec(n - 1) + fib_rec(n - 2)
}

method fib_imp(n: nat) returns (b: nat)
	ensures b == fib_rec(n)
{
	b := 0;
	var i: int := 0;
	var c := 1;

	while i < n
		invariant 0 <= i <= n
		invariant b == fib_rec(i)
		invariant c == fib_rec(i + 1)
	{
		b, c := c, b + c;
		i := i + 1;
	}
}

The loop-based bottom-up computation implicitly refines the recursive top-down computation, via appropriate invariants and postconditions. However, I'm wondering if more specific language support would simplify proving such refinements.

For example, although not an issue in the simple case of Fibonacci: the recursive function could have additional preconditions that check certain well-definedness properties (e.g. that numbers and indices are in certain ranges, that objects are not null, that sequences are not empty or of certain length), and in the current "implicit refinement" prove as illustrated above, these would most likely have to be duplicated by the loop invariant.

Thoughts and suggestions are welcome :-)