VDMJ Plugin Architecture

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

Sure, it's a very important part of how VDMJ has evolved.

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

Well, firstly, we want VDMJ to be as useful as possible, so therefore it needs to be easy to develop and extend. Secondly, we want the process of extending the tool to require a minimum of fiddly configuration for users. 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?

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 users just pop that on their VDMJ classpath. After that, the new extension features will become available in the tool.

Just add 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 users 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 has to have some VDMJ-defined Java resources available to "advertise" what it does. But those are built into the jar, so once the developers have got them right, nothing needs configuration by users.

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

Okay, a single VDMJ extension can include any or all of the following:

• It can add new annotations
• It can add an Analysis Plugin, which in turn can add:
  • new analys(es) of the VDM specification
  • new actions on lifecycle events, like type checking
  • new command-line switches to influence the new analys(es)
  • new commands for the console
  • new code lenses (in VDM-VSCode)
  • new LSP or DAP protocol extensions (in VDM-VSCode)
• It can add new external format readers to access other data sources
• It can add new global commands
• It can add new libraries, including native code
• It can add new strategies for the QuickCheck tool
• It can completely change the VDMJ lifecycle

That's quite a lot! You mean, you could write an extension that added all of those things, all in one jar?

Yes, though I admit that would be quite a complex extension.

So I'm hoping there's more information somewhere about how to do all of these things?

Of course: there are "Guides" for writing annotations, libraries, analysis plugins and external formats, and there are some examples of all of these cases in the VDMJ repository. Best of all, VDMJ uses the same architecture for its own components, which are all built into a single jar, of course. So it acts as its own example, in a sense.

So something like VDMJ's type checker or PO generator... those are just normal plugins?

Yes. So the reason there is a -i command-line switch and a print console command is because the interpreter plugin provides those things. In principle, you could replace this plugin with a user-provided version that offered different options, but fitted into the same lifecycle.

And... dare I ask what a "lifecycle" is?

A lifecycle is the thing that controls what VDMJ does, fundamentally. So when Java's "main" starts, it just creates a Lifecycle object and calls its "run" method. The Lifecycle is responsible for loading the plugins, parsing command-line switches, parsing and checking the specification, starting the console and so on. It does this by raising events that the plugins respond to. The plugins do all the work, but the lifecycle decides what order things happen in; the Lifecycle does not know what the plugins do.

Would anyone want to change the lifecycle?

It's very unlikely. But if you really wanted to do so, you could.

So you could put your own lifecycle in the same extension jar?

Yup.

But wouldn't that confuse the other extension plugins, or even the plugins built into VDMJ?

It might well do, yes, so I would urge caution! But the point is, if you want to make a subtle change, perhaps just overriding one method in the standard lifecycle to achieve some subtle effect that you can't achieve otherwise, you can do it.

Okay, I think I get the idea. So this architecture sounds very flexible indeed!