program doesn't parse

[pamelazave]

Both Visual Studio and CL versions of Dafny can't parse this file. Problem: missing r-brace on line 186. Both I and my colleagues have gone over it repeatedly and cannot find a problem with the braces. Does anyone have any advice?

Please note that the file included is a Dafny program. When I tried to upload it, GitHub would not accept a .dfy file, so I changed the file type to .txt.

Thanks!

rollover4.txt

[cpitclaudel]

You have an assert between your if and your else, which is not valid syntax:

if A {
  …
}
assert B;
else {
  …
}

For this sort of bugs, I would recommend trying to minimize your program: it quickly makes it clear where the error comes from.

[pamelazave]

Thank you! Can you tell me what it means to minimize my program?

[cpitclaudel]

Yes: remove the irrelevant bits.
To debug your issue I deleted everything before and after the method where the error was, and the error remained. Then I removed all the requires and ensures clauses, all the arguments to the method, all the comments, and everything after the else {} block, and the error was still there. Then I removed the contents of the if {} before the issue, then same with the else {} after it, and eventually I had something very small and the error was obvious.

[pamelazave]

I understand, thanks again.