VDMJ Plugin Architecture

You've mentioned this a few times, but you explain some more about VDMJ's plugin architecture?

Yes, it's quite an important part of how VDMJ is designed, and it allows other developers to easily extend it.

Right. So what's the basic idea behind this?

Firstly, we want VDMJ to be as useful as possible, so therefore it needs to be easy to develop with and extend. Secondly, we want the process of extending the tool to require a minimum of fiddly configuration. And ideally, we want other groups to be able to easily package their extensions, so that everyone can potentially share them and use them to extend their own installations.

Sounds sensible. But it also sounds like a tall order! How can you do all that easily?

Well, it's not too hard as long as extension writers follow some simple patterns. If they do this, then they can package their work into a single Java jar file and pop that on the VDMJ classpath. After that, their new feature or whatever will become available in the tool.

Just a jar file, nothing else?

That's the idea, yes. There might be properties to tweak to fine tune an extension, but by default it should "just work" if you put the jar on the classpath.

Hmmm. There's got to be something more going on in the jar then, I can't see how it works otherwise?

Yes, that's true. An extension jar file (or files) has to have some VDMJ-defined Java resources available to "advertize" what it does. But those are built into the jar, so once the developers have got them right, nothing needs changing by users.

Maybe it would be clearer if you gave me an example. What sort of things can you put inside a jar?

A single extension can include any or all of the following:

• You can add new annotations
• You can add an Analysis Plugin, which can add: a new analysis of a VDM specification new commands to execute new code lenses (in VDM-VSCode)
• You can add new external format readers to access other data sources