The Specification Language Server Protocol - overturetool/vdm-vscode GitHub Wiki

To support the specification language features the Specification Language Server Protocol (SLSP) has been developed. It builds on the design and specification of the LSP protocol. The following page describes considerations together with noteworthy details of the SLSP protocol and its design. Most of this information is copied from the Master's thesis by Rask and Madsen. The protocol types and messages can be found in the directory src/slsp/protocol/.

Reuse of the LSP Protocol

The SLSP protocol takes advantage of the existing messages and message infrastructure defined in the LSP protocol. This enables multiple levels of reuse:

  • Base Protocol: Three basic message types are defined in the LSP base protocol, namely: request, response and notification. These are reused in the SLSP protocol through the action of extending their existing entries with new types and/or entries, or by defining new variants. As a result, all SLSP protocol messages conform to the definition of the base messages defined by the LSP protocol.

  • Basic structures: The LSP protocol includes a number of basic structures that can be used when defining messages. Some of these are used in the SLSP protocol to create messages that resemble the messages defined in the LSP specification. The structures also include standards for progress notifications used by the server to stream results or publish execution completion percentages. Furthermore, it is defined how to cancel requests and which errors can be used in replies. This is also reused in the SLSP protocol.

  • Infrastructure: The LSP protocol defines communication sequences, messages and replies to ensure errorless client-server communication for the different language features. An example is the ‘initialise’ interaction defined to be the first communication exchange between a client and server to match capabilities (i.e., their support for different features). The SLSP protocol is by design an extension of the LSP protocol and as such is reusing this interaction and extending the involved messages as described in later sections.

  • Synchronisation: The LSP protocol defines messages for text synchronisation between client and server, which are leveraged directly by the SLSP protocol. Therefore, as parts of this synchronisation scheme are non-optional for LSP protocol implementations, the same is the case for an implementation of the SLSP protocol. This allows the message design for features supported in the SLSP protocol to assume that files (i.e., specifications) are available to the server. In addition, this synchronisation scheme is also what enables the language-neutral data types used by both protocols.

  • Features: A host of different programming language features are already supported by the LSP protocol. Thus, messages relevant for specification language features, such as syntax- and type-checking, are indirectly reused since these LSP messages are a subset of the SLSP protocol.

These different levels of reuse eliminate the need for designing a lot of the essential but basic message infrastructure together with the corresponding messages that would otherwise be needed in the SLSP protocol. Likewise, it also contributes to the support of a number of editor-related features that is relevant not only for editing specification languages but also in conjunction with some of the more specialised specification language features.

Methodology

The process of supporting a specification language in a given IDE by leveraging the SLSP protocol can be divided into four overall steps as illustrated in the figure below.

The processes depicted in the figure can be completed in parallel if no existing IDE and server support are available. Alternatively, only the process for the missing implementation must be completed. Following is a description of each of the steps involved in the process for the IDE:

  1. As the SLSP protocol extends the existing LSP protocol, the IDE needs to support the core elements of the LSP protocol. That is, the messaging infrastructure, basic messages, types and document synchronisation mechanisms. Furthermore, if language features that are supported by the LSP protocol are needed, e.g., type-checking and syntax-checking, parts of the protocol-specific to these features also need to be implemented. Thus, it is beneficial to consider an IDE that has native support for the LSP protocol, as this can reduce the implementation effort.
  2. Debugging functionality is not supported by the SLSP protocol but by the separate DAP protocol. As such, if debugging of the specification language is possible the IDE should support the DAP protocol to be able to handle debugging functionality. In addition, the CT functionality ‘debug trace in interpreter’ can be implemented using the DAP protocol. If the mentioned functionality is not relevant for the language this step can be skipped entirely.
  3. Support for the SLSP protocol needs to be implemented and integrated with the existing support for the LSP protocol.
  4. To leverage the feature functionality available through the implementations for the LSP, DAP and SLSP protocols, front-end logic and views specific to the IDE needs to be implemented. If support for the LSP and DAP protocols are native to the IDE the existing GUI implementation for these protocols can be leveraged.

The support for a specification language furthermore relies on a language server to provide the necessary language features. Thus, the server must support the SLSP protocol, and by dependency also the core of the LSP protocol, and possibly the DAP protocol, to be able to expose the language features it can provide to the IDE. This process is also illustrated in the figure, however, the approach differs from that of the IDE process by focusing on the available language features in the server. The description of the steps involved is as follows:

  1. If the server can provide editor features, support for the LSP protocol should be implemented. This includes not only the core parts of the protocol but also those specific to the editor features that the server can provide.
  2. If the server can provide debugging functionality, support for the DAP protocol should be implemented. This functionality can alternatively be provided by a different server or not at all if the specification language can not be executed.
  3. Support for the SLSP protocol must be implemented to handle communication-related to the specification language features that the server can provide. If support for the LSP protocol has not been implemented in step one, the core LSP protocol, i.e., the messaging infrastructure, basic messages, types and document synchronisation mechanisms, must be implemented in this step.
  4. To expose the specification language features that the server can provide, i.e., editor features, debugging functionality and/or specific specification language features, the logic that couples the protocol messages with related functionality must be implemented.

As is evident from the process of implementing protocol support in a server, it is entirely possible to have a language server that only exposes features specific to specification languages, e.g., POG and CT, using the SLSP protocol. However, the adequacy of such a server implementation is questionable, as editor related features are highly relevant in a proper IDE.

Protocol Outline

See here for the full outline of the SLSP protocol.