Boogie code

Mar 12, 2013 at 9:56 PM
Hi ....

I have a newbie question. Is there any way to view the boogie code generated by Dafny for the verification process?

Apr 15, 2013 at 10:15 PM
Yes. Run Dafny from the command line and use the /print option. For example,
    dafny MyProgram.dfy /print:MyProgram.bpl
will write the Boogie translation of the Dafny program MyProgram.dfy to the file MyProgram.bpl. You can then run Boogie directly on the .bpl file, if you wish.

If you're going to read the read the Boogie code, I recommend using some syntax highlighter, which you can find in the Util folder of the Boogie source distribution. There is also a Boogie plug-in for Eclipse.

Apr 25, 2013 at 3:01 AM
Ok Rustan....

I'll give it a shot.