Dafny Language Server Redesign

In unserer Studienarbeit wurde der Dafny Language Server in C# neu implementiert. Das in TypeScript geschriebene Visual Studio Code Plugin, welches die Sprache Dafny unterstützt, kommuniziert über das LSP direkt mit dem Language Server.

SA Plakatübersicht

Ausgangslage

Dafny ist eine formale Programmiersprache, um die Korrektheit eines Programms mit preconditions, postconditions, loop invariants und loop variants zu beweisen. In einer vorangegangenen Bachelorarbeit wurde ein Plugin für Visual Studio Code implementiert, um auf Dafny-spezifische statische Analysefunktionen zuzugreifen.

Wenn Dafny beispielsweise keine postconditions nachweisen kann, wird der Code hervorgehoben und ein counter example angezeigt. Darüber hinaus bietet es Zugriff auf Codekompilierung, Vorschläge zur automatischen Vervollständigung und verschiedene automatisierte Refactorings.

Das Plugin kommuniziert mit einem Sprachserver unter Verwendung des Language Server Protocol (LSP) von Microsoft, das die Kommunikation zwischen einer Entwicklungsumgebung (IDE) und einem Language Server standardisiert. Der Language Server selbst greift über eine proprietäre JSON-Schnittstelle auf die Dafny-Bibliothek zu, die das Backend der Dafny-Sprachanalyse enthält.

Ziele

Das Ziel dieser Arbeit war es, den Language Server so zu gestalten, dass er direkt in die Dafny-Bibliothek integriert werden kann, und die proprietäre JSON-basierte Interaktion zu übergehen. Anschliessend können so neue Sprachfunktionen implementiert und über das Sprachserverprotokoll angeboten werden. Um direkten Zugriff auf die Dafny-Bibliothek zu haben, wird der Sprachserver in C# neu implementiert.

Ergebnis

Der bereits vorhandene Language Server könnte durch unseren neu geschriebenen Server ersetzt werden. Da in ihm die Dafny-Bibliothek integriert ist, kann auf alle Funktionen direkt zugegriffen werden. Dies macht die proprietäre Schnittstelle zwischen dem alten Sprachserver und der Dafny-Bibliothek überflüssig. Die meisten Funktionen der vorherigen Bachelorarbeit werden mit dem neuen Language Server unterstützt. Diese beinhalten:

  • Kompilierung und Codeüberprüfung􏰤
  • Syntax- und Fehlerhervorhebung
  • Vorschläge für die automatische Vervollständigung
  • Code Lens
  • Go to Definition

Mit dem neuen Language Server können weitere Funktionen auf bequeme und einheitliche Weise hinzugefügt werden. Dies ermöglicht die Integration in andere IDEs nebst Visual Studio Code.