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

Content

Base Protocol

The base protocol consists of a header and a content part (comparable to HTTP). The header and content part are separated by \r\n.

Header Part

The header part consists of header fields. Each header field is comprised of a name and a value, separated by ‘: ’ (a colon and a space). The structure of header fields conform to the HTTP semantic. Each header field is terminated by \r\n. Consider- ing the last header field and the overall header itself are each terminated with \r\n, and that at least one header is mandatory, this means that two \r\n sequences al- ways immediately precede the content part of a message. Currently the following header fields are supported:

Header Field Name Value Type Description
Content-Length number The length of the content part in bytes. This header is required.
Content-Type string The mime type of the content part. Defaults to application/vscode-jsonrpc; charset=utf-8

The header part is encoded using the ‘ascii’ encoding. This includes the \r\n separating the header and content part.

Content Part

Contains the actual content of the message. The content part of a message uses JSON-RPC to describe requests, responses and notifications. The content part is encoded using the charset provided in the Content-Type field. It defaults to utf-8, which is the only encoding supported right now. If a server or client receives a header with a different encoding than utf-8 it should respond with an error.

(Prior versions of the protocol used the string constant utf-8 which is not a correct encoding constant according to specification.) For backwards compatibility it is highly recommended that a client and a server treats the string utf-8 as utf-8.

Example

Content-Length: ...\r\n
\r\n
{
    "jsonrpc": "2.0",
    "id": 1,
    "method": "textDocument/didOpen",
    "params": {
        ...
    }
}

Base Protocol JSON structures

The following TypeScript definitions describe the base JSON-RPC protocol:

Abstract Message

A general message as defined by JSON-RPC. The language server protocol always uses "2.0" as the jsonrpc version.

interface Message {
    jsonrpc: string;
}

Request Message

A request message to describe a request between the client and the server. Every processed request must send a response back to the sender of the request.

interface RequestMessage extends Message {
    /**
     * The request id.
     */
    id: number | string;

    /**
     * The method to be invoked.
     */
    method: string;

    /**
     * The method's params.
     */
    params?: array | object;
}

Response Message

A Response Message sent as a result of a request. If a request doesn’t provide a result value the receiver of a request still needs to return a response message to conform to the JSON RPC specification. The result property of the ResponseMessage should be set to null in this case to signal a successful request.

interface ResponseMessage extends Message {
    /**
     * The request id.
     */
    id: number | string | null;

    /**
     * The result of a request. This member is REQUIRED on success.
     * This member MUST NOT exist if there was an error invoking the method.
     */
    result?: string | number | boolean | object | null;

    /**
     * The error object in case a request fails.
     */
    error?: ResponseError;
}

interface ResponseError {
    /**
     * A number indicating the error type that occurred.
     */
    code: number;

    /**
     * A string providing a short description of the error.
     */
    message: string;

    /**
     * A primitive or structured value that contains additional
     * information about the error. Can be omitted.
     */
    data?: string | number | boolean | array | object | null;
}

export namespace ErrorCodes {
    // Defined by JSON RPC
    export const ParseError: number = -32700;
    export const InvalidRequest: number = -32600;
    export const MethodNotFound: number = -32601;
    export const InvalidParams: number = -32602;
    export const InternalError: number = -32603;
    export const serverErrorStart: number = -32099;
    export const serverErrorEnd: number = -32000;
    export const ServerNotInitialized: number = -32002;
    export const UnknownErrorCode: number = -32001;

    // Defined by the protocol.
    export const RequestCancelled: number = -32800;
    export const ContentModified: number = -32801;
}

Notification Message

A notification message. A processed notification message must not send a response back. They work like events.

interface NotificationMessage extends Message {
    /**
     * The method to be invoked.
     */
    method: string;

    /**
     * The notification's params.
     */
    params?: array | object;
}

$ Notifications and Requests

Notification and requests whose methods start with $/ are messages which are protocol implementation dependent and might not be implementable in all clients or servers. For example if the server implementation uses a single threaded synchronous programming language then there is little a server can do to react to a $/cancelRequest notification. If a server or client receives notifications starting with $/ it is free to ignore the notification. If a server or client receives a requests starting with $/ it must error the request with error code MethodNotFound (e.g. -32601).

Cancellation Support

The base protocol offers support for request cancellation. To cancel a request, a notification message with the following properties is sent:

Notification:

  • method: $/cancelRequest
  • params: CancelParams defined as follows:
interface CancelParams {
    /**
     * The request id to cancel.
     */
    id: number | string;
}

A request that got canceled still needs to return from the server and send a response back. It can not be left open/hanging. This is in line with the JSON RPC protocol that requires that every request sends a response back. In addition it allows for returning partial results on cancel. If the request returns an error response on cancellation it is advised to set the error code to ErrorCodes.RequestCancelled.

Progress Support

The base protocol offers also support to report progress in a generic fashion. This mechanism can be used to report any kind of progress including work done progress (usually used to report progress in the user interface using a progress bar) and partial result progress to support streaming of results.

A progress notification has the following properties:

Notification:

  • method: $/progress
  • params: ProgressParams defined as follows:
type ProgressToken = number | string;
interface ProgressParams<T> {
    /**
     * The progress token provided by the client or server.
     */
    token: ProgressToken;

    /**
     * The progress data.
     */
    value: T;
}

Progress is reported against a token. The token is different than the request ID which allows to report progress out of band and also for notification.

Proof Obligation Generation

Besides specialised initialisation entries, the following messages are related to the POG feature in the protocol:

  • Generate request
  • Specification Updated notification

Initialisation

Client Capability

  • property name (optional): experimental.proofObligationGeneration
  • property type: boolean

Server Capability

  • property name (optional): experimental.proofObligationProvider
  • property type: boolean

Generate Request

The generate proof obligations request is sent from the client to the server to request generation of proof obligations for a document or folder.

Request:

  • method: slsp/POG/generate
  • params: GeneratePOParams defined as follows:
export interface GeneratePOParams {
    /**
     * Uri to the file/folder for which proof obligations
     * should be generated.
     */
    uri: DocumentUri;
}

Response:

  • result: ProofObligation[] | null
  • error: code and message set in case an exception happens during the generate request.
/**
 * Parameters describing a Proof Obligation (PO) and meta data.
 */
export interface ProofObligation {
    /**
     * Unique identifier of the PO.
     */
    id: number;
    /**
     * Type of the PO.
     */
    kind: string;
    /**
     * Name of the PO.
     * Array describe the hieracy of the name,
     * e.g. ["classA", "function1"].
     */
    name: string[];
    /**
     * Location where the PO applies.
     */
    location: Location;
    /**
     * Source code of the PO.
     * String array can be used to provide visual formatting
     * information, e.g. the PO view can put a "\n\t" between
     * each string in the array.
     */
    source: string | string[];
    /**
     * An optional status of the PO, e.g., "Unproved" or "Proved".
     */
    status?: string;
}

Specification Updated Notification

The updated notification is sent from the server to the client to notify that the specification has been updated. Meaning that the PO that has been sent to the client before this notification are now out-of-sync with the specification.

Notification:

  • method: slsp/POG/updated
  • params: POGUpdatedParams defined as follows:
export interface POGUpdatedParams {
    /**
     * Describes the state of the specification. 
     * True if POG is possible.
     * False otherwise, e.g. the specification is not type-correct.
     */
    successful: boolean;
}

Combinatorial Testing

Besides specialised initialisation entries, the following messages are related to the CT feature in the protocol:

  • Traces request
  • Generate request
  • Execute request

Initialisation

Client Capability

  • property name (optional): experimental.combinatorialTesting
  • property type: boolean

Server Capability

  • property name (optional): experimental.combinatorialTestProvider
  • property type: boolean | CombinatorialTestOptions where CombinatorialTestOptions is defined as follows:
export interface CombinatorialTestOptions extends WorkDoneProgressOptions {}

Trace Request

The trace request is sent from the client to the server to request an outline of the traces available in a given specification.

Request:

  • method: slsp/CT/traces
  • params: CTTracesParameters defined as follows:
export interface CTTracesParameters {
    /**
     * An optional uri to the file/folder for which Traces should be found.
     */
    uri?: URI;
}

Response:

  • result: CTSymbol[] | null
  • error: code and message set in case an exception happens during the traces request.
/**
 * Describes a grouping of traces, e.g. a class, classA, may 
 * have multiple traces which are all combined in a CTSymbol.
 */
export interface CTSymbol {
    /**
     * Name of Trace group, e.g. "classA".
     */
    name: string;
    /**
     * Traces in the group.
     */
    traces: CTTrace[];
}

/**
 * Overview information about a trace
 */
export interface CTTrace {
    /**
     * Fully qualified name of the trace.
     */
    name: string;
    /**
     * Location in the source code of the trace.
     */
    location: Location;
    /**
     * An optional combined verdict of all the tests from the trace.
     */
    verdict?: VerdictKind;
}

/**
 * Kinds of test case verdicts.
 */
export enum VerdictKind {
    Passed = 1,
    Failed = 2,
    Inconclusive = 3,
    Filtered = 4,
}

Generate Request

The generate request is sent from the client to the server to request generation of tests from a trace.

Request:

  • method: slsp/CT/generate
  • params: CTGenerateParameters defined as follows:
export interface CTGenerateParameters 
    extends WorkDoneProgressParams {
    /**
     * Fully qualified name of the trace, which test cases should be 
     * generated based on.
     */
    name: string;
}

Response:

  • result: CTGenerateResponse | null
  • error: code and message set in case an exception happens during the generate request.
export interface CTGenerateResponse {
    /**
     * The number of tests that is generated from the trace.
     */
    numberOfTests: number
}

%

Execute Request

The execute request is sent from the client to the server to request execution of tests from a trace using optional filtering options.

Request:

  • method: slsp/CT/execute
  • params: CTExecuteParameters defined as follows:
export interface CTExecuteParameters 
    extends WorkDoneProgressParams, PartialResultParams {
    /**
     * Fully qualified name of the trace, which test cases should be 
     * executed from.
     */
    name: string;
    /**
     * Optional filters that should be applied to the exectution. 
     * If omitted the server should use default settings.
     */
    filter?: CTFilterOption[];
    /**
     * An optional range of tests that should be executed. 
     * If omitted all tests for the trace are executed.
     */
    range?: NumberRange;
}

/**
 * Mapping type for filter options for the execution of CTs. 
 */
export interface CTFilterOption {
    /**
     * Name of the option. E.g. "reduction", "seed" or "limit".
     */
    key: string;
    /**
     * Value of the option. E.g. "random", 999, 100.
     */
    value: string | number | boolean;
}

/**
 * Describes a range of numbers, e.g. 1-10.
 */
export interface NumberRange {
    /**
     * Start number, if omitted 'end' should be considered as
     * the absolute number of tests that must be returned
     */
    start?: number;
    /**
     * End number, if omitted tests from 'start' to last 
     * should be returned.
     */
    end?: number;
}

Response:

  • result: CTTestCase[] | null
  • partial result: CTTestCase[]
  • error: code and message set in case an exception happens during the execute request.
/**
 * Test case information.
 */
export interface CTTestCase {
    /**
     * ID of the test case.
     */
    id: number;
    /**
     * Test case verdict
     */
    verdict: VerdictKind;
    /**
     * Test case execution sequence and result.
     */
    sequence: CTResultPair[];
}

/**
 * Kinds of test case verdicts.
 */
export enum VerdictKind {
    Passed = 1,
    Failed = 2,
    Inconclusive = 3,
    Filtered = 4,
}

/**
 * Test sequence result pair. 
 */
export interface CTResultPair {
    /**
     * The opration/function that was executed.
     */
    case: string;
    /**
     * The result of the operation/function. Null if no result.
     */
    result: string | null;
}

Translation

Besides specialised initialisation entries, the following message is related to the translate feature in the protocol:

  • Translate Request

Initialisation

Client Capability

  • property name (optional): experimental.translate
  • property type: boolean

Server Capability

  • property name (optional): experimental.translateProvider
  • property type: boolean | TranslateOptions where TranslateOptions is defined as follows:
export interface TranslateOptions extends WorkDoneProgressOptions {
    /**
     * language id as a string. See the LSP specification for valid ids.
     */
    languageId: string | string[];
}

Translate Request

The translate request is sent from the client to the server to request translation of a specification.

Request:

  • method: slsp/TR/translate
  • params: TranslateParams defined as follows:
export interface TranslateParams {
    /**
     * Uri specifying the root of the project to translate.
     */
    uri?: URI;
    /**
     * Language id as a string. 
     * See the LSP specification for valid ids.
     */
    languageId: string;
    /**
     * Uri specifying the location of the resulting 
     * translation. This should be an existing empty folder.
     */
    saveUri: DocumentUri;
    /**
     * Options that the command handler should be invoked with.
     */
    options?: any;
}

Response:

  • result: TranslateResponse defined as follows:
export interface TranslateResponse {
    /**
     * URI specifying the "main" file of the resulting translation 
     * If multiple files are generated, this is the uri to where 
     * "main" is.
     */
    uri: DocumentUri;
}

Theorem Proving

Besides specialised initialisation entries, the following messages in the protocol is related to the theorem proving feature:

  • Lemmas Request
  • Begin Proof Request
  • Prove Request
  • Get Commands Request
  • Command Request
  • Undo Request

Initialisation

Client Capability

  • property name (optional): experimental.theoremProving
  • property type: boolean

Server Capability

  • property name (optional): experimental.theoremProvingProvider
  • property type: boolean

Lemmas Request

The lemmas request is sent from the client to the server to get an exhaustive list of Lemma in the specification.

Request:

  • method: slsp/TP/lemmas
  • params: LemmasParams defined as follows:
interface TPLemmasParams {
    /**
     * The scope of the project files.
     */
    projectUri?: DocumentUri
}

Response:

  • result: Lemma[] defined as follows:
/**
 * Parameters describing a Lemma and meta data.
 */
interface Lemma {
    /**
     * Unique name of the lemma.
     */
    name: string,
    /**
     * Name of the theory that the lemma belongs to.
     */
    theory: string,
    /**
     * Identifies the location of the lemma.
     */
    location: Location,
    /**
     * Theorem, Lemma, corollary etc.
     */
    kind: string,
    /**
     * Status of the proof of the lemma
     */
    status: ProofStatus
}

Where ProofStatus is defined as follows:

/**
 * Type describing the status of a proof
 */
type ProofStatus = "proved" | "disproved" | "untried" | "unfinished" | "timeout" | "unchecked";

Begin Proof Request

The begin proof request is sent from the client to the server to initialise a proof session for a Lemma.

Request:

  • method: slsp/TP/beginProof
  • params: TPBeginProofParams defined as follows:
interface TPBeginProofParams {
    /**
     * Name of the lemma that is to be proved.
     */
    name: string
}

Response:

  • result: ProofState defined as follows:
/**
 * Parameters describing the state of a proof and meta data.
 */
interface ProofState {
    /**
     * Proof step id.
     */
    id: number,
    /**
     * Status of the proof. 
     */
    status: ProofStatus | string,
    /**
     * Subgoals, empty if proved.
     */
    subgoals: string[],
    /**
     * Rules used for this step.
     */
    rules?: string[]
}

Prove Request

The prove request is sent from the client to the server to request the theorem prover to automatically prove a Lemma.

Request:

  • method: slsp/TP/prove
  • params: TPProveParams defined as follows:
interface TPProveParams {
    /**
     * Name of the lemma that is to be proved. 
     * If proof in progress that lemma is assumed.
     */
    name?: string
}

Response:

  • result: TPProveResponse defined as follows:
interface TPProveResponse {
    /**
     * Status of the proof. 
     */
    status: ProofStatus,
    /**
     * Processing time in milliseconds
     */
    time?: number,
    /**
     * Suggested commands to apply
     */
    command?: string[],
    /**
     * Humans-readable description of:
     * Counter example, proof steps, etc.
     */
    description?: string
}

Get Commands Request

The get commands request is sent from the client to the server to request a list of commands that can be applied to a proof.

Request:

  • method: slsp/TP/getCommands
  • params: null.

Response:

  • result: TPCommand defined as follows:
/**
 * Parameters describing a theorem proving command.
 */
interface TPCommand {
    /**
     * Command name.
     */
    name: string,
    /**
     * Description of the command.
     */
    description: string
}

Command Request

The command request is sent from the client to the server to apply a command to the current step of a proof.

Request:

  • method: slsp/TP/command
  • params: TPCommandParams defined as follows:
interface TPCommandParams {
    /**
     * The command and arguments identified by a string.
     */
    command: string
}

Response:

  • result: TPCommandResponse defined as follows:
interface TPCommandResponse {
    /**
     * Description of the result of the command, 
     * e.g. accepted, error, no change.
     */
    description: string,
    /**
     * State of the proof after the command.
     */
    state: ProofState
}

Undo Request

The undo request is sent from the client to the server to undo a proof step.

Request:

  • method: slsp/TP/undo
  • params: TPUndoParams defined as follows:
interface TPUndoParams {
    /**
     * Id of the step that must be undone.
     * If empty, undo last step.
     */
    id?: number
}

Response:

  • result: ProofState.