Skip to content

LSP High Level Design

Nick Battle edited this page Jan 17, 2023 · 12 revisions

I imagine the LSP High Level Design is like the VDMJ HLD, but for something called LSP?

Exactly.

So you'd better explain what LSP is all about.

It stands for the Language Server Protocol. It's a way for IDE front ends to communicate with a "server" that does all of the language processing, leaving the front end to worry about presenting a GUI without worrying about all the language details.

So this supports the IDEs, Eclipse and VSCode?

Just VSCode. Eclipse uses a different protocol called the Debug Protocol (DBGp), which comes from XDebug.

Is there a DBGp HLD somewhere?

There are a couple of documents you can look at for that, but really this is now a legacy protocol. There's a short design and a guide for how to test it via the command line.

So LSP is much more important?

Yes, at the moment, LSP and DAP are the preferred way to use an IDE with VDMJ.

DAP?

That's a complementary protocol to LSP, called the Debug Adapter Protocol. That allows you to run and debug "programs" that are managed by the server. In our case they are VDM specifications, of course. LSP handles things like syntax and type checking.

So is there a DAP server too?

In a sense, but LSP and DAP are threads of the same server component and covered in the same design.

Okay, so we're trying to keep this short, but can you tell us about what is in the LSP HLD?

Well, there are three main sections. The first gives an overview of the Java packages and describes what LSP and DAP are and how they fit into the VDMJ architecture. The old DBGp components are shown there too.

Because DBGp and LSP/DAP do the same thing?

Roughly, yes. The point is, the architecture separates the communication with an IDE from the language services that check and execute specifications. So in future, we should be able to add yet more protocol adapters without changing much.

OK, that makes sense. So then section 2 is the package detail?

Quite right. So this is the same format as the main VDMJ HLD, with each package explained and the main classes shown and discussed. It also explains what analysis plugins are all about.

I'll probably have questions about that too, but let's stick with this document for now. What's in the last section?

That has a set of walk-throughs of various common scenarios, discussed in terms of how the flow of control moves through the components and which messages and events are sent. It's trying to make it more "practical".

Nice idea! Anything else we need to mention?

Just to add that most sections have a "Comments" subsection at the end, where I make my excuses and explain why things are done the way that they are.

History will thank you!

(Yeah, right)

Clone this wiki locally