Boogie Editors (Eclipse, TextMate, ACE)

Jul 4, 2012 at 1:51 PM

We are currently working on a tool that targets Boogie as output language. To enable efficient work with larger BPL files, we have developed an Eclipse-based Boogie Editor. As we believe this editor to be useful for others, we have put it up on codeplex:

Some of the features:

  • Syntax and semantic highlighting
  • Navigable outline view of code structure
  • Pretty-prints special keywords (forall, exists) and ASCII operators (<==>, ...) as Unicode symbols
  • Jump to declaration support
  • Buttons to type-check or verify Boogie program
  • Errors in console as hyperlinks

We also provide Boogie syntax highlighting modes for TextMate and ACE.