-
Notifications
You must be signed in to change notification settings - Fork 12
Feature Wishlist
From the Thesis document:
Integrating a debugger into the plugin would be great, since this is a feature that is very often used and very helpful when searching for bugs. An existing solution already supports this feature, namely the Visual Studio integration [Mic17e] of Dafny. This already works very well and can be used as a guideline when developing an own integration. It is also a feature that programmers have become used to in all modern IDEs, so it should be part of any language integration.
Sadly it is also quite a difficult task since the interaction between an IDE, an executable and a debugger is complex. While the Visual Studio integration is open source, it is written in C# and can therefore interface directly with the Dafny pipeline, which is heavily done in that integration. It would take quite some work to abstract this direct interaction into a clean API that extends the existing API of the Dafny pipeline. Using this API, a language server could provide an own implementation of a debugger.
Designing this complex component was well out of scope for this project. It is estimated that, depending on the preexisting knowledge, this would be an endeavor of about two to four weeks time and probably would have to rely on at least some help by the Dafny development team. While this task is difficult, the result would be having an important feature that all users of modern IDEs anticipate in a language integration. It therefore should be a primary consideration when deciding on how to extend this project.