While or For Loop in function

[dreamqin68]

Hi All,

What is the correct way to use While or forall loop in function? I found that it is not the same as using in method.

Thanks in advance.

[cpitclaudel]

Hi there,

while and forall statements are not supported in functions — in fact, no statements are! Function bodies can only use expressions (that and the fact that methods are opaque are the main differences between functions and methods).

[MikaelMayer]

I'll add to this answer that, although you cannot use statements, you can use recursivity to achieve your goal. In fact, recursivity is the only way in the functional world of expressions to emulate a changing state.

For example, let's say you want to compute factorial:

method factorial(i: int) returns (r: int)
{
  r := 1;
  var t := i;
  while t > 0 {
    r := r * t;
    t := t - 1;
  }
  return r;
}

You can convert this to a recursive function by looking at the variables that you are modifying, and placing them as the arguments of an auxiliary function:

method factorial(i: int) returns (r: int)
{
  return factorial_aux(1, i);
}
function method factorial_aux(r: int, t: int) returns (r: int) {
   if t > 0  then
   factorial_aux(
    /* r:= */ r * t,
    /* t:= */ t - 1)
  else
    /*return*/ r
}

[dreamqin68]

Great！Thanks!

[dreamqin68]

Okay, thank you!

[davidcok]

This point also argues for having a library of stream functions in Dafny -- they can stand in for many loops