for-loops in Dafny

[HPGumm]

I am about to teach a course on program verification where I intended to use Dafny. Now, I am sort of puzzled why Dafny shys away from for-loops and seems to be inconsistent about their support.

On the one hand, Dafny 4.0 seems to support for-loops both in the ascending variant: "for c:= 0 to n {...}" as well as in the descending variant: "for c:= 0 downto n {...}".

It lets me verify for-loops, but the compiler reports an error. So there seems to be some inconsistency here.

The new book "Program Proofs" mentions for-loops only in the introduction on page xx. I cannot find them anywhere in the main text - let alone any example.

I personally regard for-loops immensely helpful in programming with arrays, so I cannot understand why reasonable support is missing in Dafny.

H.Peter Gumm

[MikaelMayer]

I'm sorry to hear that you got an error using for loops. I'm happy to help. Can you provide me with a small example of the for-loop and what failed exactly?

[HPGumm]

I found the mistake. It was my error, I apologize. When compiling, my path still pointed to an older version of dafny.