Dafny translation into Boogie

Coordinator
Jun 21, 2015 at 2:34 PM
I received the following question, which I'm answering here.
I'm a graduate studant ... doing a research about programming languages and I have some questions about the way how Dafny works. I know that Dafny use Boogie and Z3 and I'd like to know how Danfy is translated to Boogie and how Boogie is translated to Z3. I've been search at internet but I cannot find anything about this translation.

Do you have some material that explain how those translation woks?

Another thing that I don't know is: If Dafny has recursive function and Z3 seems does not have, how Dafny translate recursive function to Z3?
My Marktoberdorf 2008 lecture notes, "Specification and verification of object-oriented software", give the translation of Dafny into Boogie. Many things have evolved in the Dafny translation since 2008, but these lecture notes should still be useful. Some general features that have been added since then are described in the main Dafny publication: Leino, "Dafny: An Automatic Program Verifier for Functional Correctness", LPAR-16.

The Marktoberdorf 2008 lecture notes also explain Boogie, but if you want a more detailed description of how verification conditions are actually generated from Boogie code, see Barnett and Leino, "Weakest preconditions for unstructured programs", PASTE 2005.

The best description of how recursive functions are translated, today, in Dafny is found in Amin, Leino, and Rompf, "Computing with an SMT solver", TAP 2014. There are many other features of Dafny that have no direct counterpart in Boogie or Z3. These include, for example, induction [Leino, VMCAI 2012], co-induction [Leino and Moskal, FM 2014], proof calculations [Leino and Polikarpova, VSTTE 2013], and unlimited unfolding of recursive functions [Amin, Leino, and Rompf, TAP 2014].

Rustan