1

As mentioned in the Wiki on Dafny GitHub, when Dafny cannot prove an assertion in a program, it might be due to either my program is incorrect OR the incompleteness of Dafny. But I figured the counter example from Dafny is spurious after I tried understanding it, so I still have no idea if my program is correct or not.

My question is as follows. If I manage to use another Boogie backend such as Corral to check the translated Boogie program from Dafny using /print, and Corral also returns a model to invalidate the Boogie program, would that guarantee the model disprove my Dafny program and I can use it for debugging? Or is it still likely spurious so don't bother to try it?

From their papers, it seems to me that Corral and Symbooglix should guarantee that a provided model should be a concrete counter example for the translated Boogie program, so maybe my question is more on whether the Dafny program and the translated Boogie program is semantically equivalent.

PS: I tried passing translated bpl files to Corral and check specific Boogie procedure in that bpl, and Corral simply says it cannot find the procedure, so I'm debating if I want to make it work.

Chiao Hsieh
  • 13
  • 2

1 Answers1

0

It's unlikely that another backend will have any better luck with the translated Boogie file, because the reasons for incompleteness are fundamental.

For example, Dafny ships an axiomatization of several data structures, including sequences, and these axiomatizations are known to be incomplete.

If you are having trouble with understanding a specific Dafny failure, I suggest you ask another question about your specific program and include a minimal working example, if possible.

James Wilcox
  • 5,307
  • 16
  • 25
  • Thanks, James! I asked a general question because it was not for a particular program. It's that usually I do have faults when Dafny fails to prove. So there exists concrete cex, but Dafny gave me a spurious one unless I add better lemmas or stronger assumptions. For most of my faults, a bounded symbolic execution should help get concrete model (or equivalently a unit test input), and I did similar thing by adding `assume` on branches. If symbolic execution is my purpose, do I get it by using Corral or Symbooglix then? – Chiao Hsieh Sep 13 '18 at 18:24
  • Unfortunately, I'm not familiar with those tools, so I don't know whether they would work for you or not. – James Wilcox Sep 13 '18 at 22:08