Overview

The extension implements a client-server architecture that uses the SLSP, LSP, and DAP protocols for communication. The client implementation is tightly coupled to VS Code, whereas the server implementation is fully decoupled from the client. The VDM language support is provided by the server as an implementation of VDMJ with extended capabilities to support the protocols. As a result of using the protocols, the server can be reused for any clients that support the protocols, and vice versa. Below is an overview of the components in the extension architecture:

Short description of the components:

• VS Code Components
  • Generic DAP Client: Handles the integration of the features enabled by the DAP protocol and provides the messaging infrastructure to handle the protocol on the client side.
  • DAP Client: Extends the Generic DAP Client to connect to the Debug Adapter on the server.
  • Generic LSP Client: Handles the integration of the features enabled by the LSP protocol and provides the messaging infrastructure to handle the protocol on the client side.
  • SLSP Client: Extends the Generic LSP Client with the messaging infrastructure to support the SLSP protocol.
  • Syntax Highlighting: Uses TextMate grammars to highlight VDM keywords.
  • POG Functionality Support: Implements the functionality to support the POG language feature enabled by the SLSP protocol.
  • CT Functionality Support: Implements the functionality to support the CT language feature enabled by the SLSP protocol.
  • Translate Functionality Support: Implements the functionality to support the translation language features enabled by the SLSP protocol.
• VDM Language Support Modules
  • Debug Adapter: Wraps the VDM Debugger to provide the debug functionality using the DAP protocol.
  • VDM Debugger: Provides the VDM debugger functionality.
  • SLSP Server: Wraps the VDMJ language support to provide it using the SLSP and LSP protocols.
  • VDM Language Feature Support: Provides the VDM language support functionality.

SLSP Client Features

When implementing features that use the SLSP protocol we use a design where the user interface elements (buttons, views, etc.) are decoupled from the use of the protocol itself. This is to mimic the way VS Code implements UI elements where you can implement the features without the use of a client-server architecture. Below you see a class diagram for the Proof Obligation Generation feature. This is used to describe the design, which is also used in the other features.

For several of the classes, only the functions that are mainly used are included in the class description.

Starting at the extension class you can see that the extension has multiple instances of the class SpecificationLanguageClient. This is the case since a client and server instance is created for each workspace folder. The SpecificationLanguageClient is an expansion of the VS Code class LangaugeClient to make use of the built-in functionality.

In the LanguageClient it is possible to register features that implement one of the interfaces StaticFeature or DynamicFeature. Both of these interfaces describe the functions that must be implemented to handle the initialisation of the feature between client and server. Currently, the features that as supplied for the SLSP protocol only supports static registration, hence they implement the StaticFeature interface. For POG this is implemented in the class ProofobligationGenerationFeature, which is responsible for providing a data provider for the Proof Obligation View that gets its data from the server.

The UI element for POG is called ProofObligationPanel. Only one instance of this class is created by the extension, as all the workspace folders share the same PO View. To be able to support all the workspace folders the panel can have multiple ProofObligationProvider's (one for each workspace folder). The provider is used to get the data that is shown in the PO View and subscribe to events that are associated with the feature. Furthermore, the ProofObligationPanel is responsible for registering the handlers for the commands that are contributed in the package.json file.

Class Name	Description
extension	Not a class but the content of the extension.ts file. The file describes what happens when the extension is activated and how and when new client-server pairs are created and disposed of.
SpecificaitonLanguageClient	Responsible for registering the SLSP related features.
LanguageClient	The native VS Code implementation of the LSP client.
StaticFeature	Interface describing the functions needed to register LSP feature statically.
ProofObligationGenerationFeature	Responsible for providing a data provider for the PO View, communicating with the server to get the data and convert between protocol and code formats.
ProofObligationProvider	Interface that describes the data provider for the PO View and which events are available to the feature.
ProofObligationPanel	Responsible for managing the creation and updating of the PO View. Uses the providers to get the data to display.
vscode.commands	Namespace that contains the functions needed to register and execute VS Code commands