Search code examples
z3dafny

Boogie on Visual Studio


My question is about Boogie, but since no Boogie tag was available, I used the dafny tag as one that is closely related to Boogie.

I have built Boogie on Visual Studio following the instructions in the documentation. What should I do next to write Boogie code or equivalently how can I run the .bpl files in the Test folder? From what I understood is that Boogie although an intermediate verification language can be used independently as well.

Thank you.


Solution

  • There is no interactive VS mode for Boogie. If you want to write Boogie code and get design-time feedback in the editor, then the best mode available is in emacs, see https://github.com/boogie-org/boogie-friends. Still, this emacs mode does not give you error traces or verification-debugger information.