Dafny: infinite recursion with refinement

Oct 26, 2012 at 8:27 PM

I'm wonder does this program terminate: http://rise4fun.com/Dafny/TNH2 . Dafny says it terminates but it has infinite recursion!

Oct 27, 2012 at 10:17 PM

The program does not have infinite recursion.  Here is a version of the program with method bodies, making it compile: http://rise4fun.com/Dafny/Axmp  It verifies and compiles, and running it does terminate.

I think you may be thinking that all uses of A0 will automatically be replaced by A1.  That is not so.  If that's what you want, then you have to say so in the modules, either by using clauses like "import A as A0 default A1" or by declaring a refinement of B1 and saying "import A = A1;".

For example, something like http://rise4fun.com/Dafny/st5 or http://rise4fun.com/Dafny/9Soi, but note that these programs produce an error about cyclic module imports.


Oct 27, 2012 at 11:08 PM

Thank you, Rustan! I tried to write a program with two modules in which the first module uses the second module and vice versa. I got a message about cyclic imports. And after that I concludes I should use imports of "interfaces". I've implemented this idea but I think this program has an infinite loop (modules A0 and B0 are "interfaces", so ). I may refine imports to any new modules which don't call methods recursively, and so this program mightn't have an infinite loop.