VDMJ High Level Design

I can probably guess what the VDMJ High Level Design is for, but can you explain it anyway?

It's a document that tries to explain the internal structure of the VDMJ tool, at a high level. So it describes the various Java packages and what they do, and it shows how the various parts fit together. But it doesn't describe lines of code, except for a few examples.

It sounds like this is only for people who want to work with the internals or to change VDMJ in some way?

Mostly, yes. There are a few areas discussed that would be useful to people writing extensions for VDMJ, but most of it is concerned with how VDMJ is written and why it was done that way.

So can you give us a quick overview of the sections?

Sure. There are three main sections. The first one has an overview of the Java package structure. That will help you to navigate around the sources. Hopefully the packages are fairly intuitive: vdmj.lex does lexical analysis; vdmj.syntax does syntax analysis; vdmj.typechecker does type checking, and so on.

Presumably it's not as easy as that?

Well, there are complications, yes. But it's not a fundamentally complicated system. I hope the document brings that out.

Okay, so what comes after the package overview?

The first section also describes something called "class mapping". It's an important part of the system and quite unusual. In a nutshell, it means that the parser creates classes under vdmj.ast, but these are mapped into classes under vdmj.tc to perform type checking, and those in turn are mapped into classes under vdmj.in to run the interpreter, and so on for other analyses.

That is unusual. There must be a good reason to do that?

Yes, it's based on what we learned from the Overture project. They took the original VDMJ version 3 sources and tried to implement the same thing using "visitors". That was a sensible thing to do - it means things are nicely separated - but it can also get very ugly when you can have a large number of AST classes. So class mapping was introduced in VDMJ version 4 to try to solve those problems.

And did it work?

Yes, very nicely as it happens. There's a paper describing the principles and comparative measurements (see [9] in the design).

Intriguing. Okay, I'll have a look at that. But what else is covered in the design document?

Section 2 goes through each of the packages mention in the overview, and describes them in a bit more detail. The most important classes in each package are explained and so on. Each section also has a "Comments" subheading, where I've added thoughts or reasons for unusual choices, or things we might do in future.

Right. So if I wanted to know about the interpreter, I could just go to that section?

That's an interesting case, because the interpreter involves the vdmj.runtime, vdmj.scheduler, vdmj.values and vdmj.in packages. But yes, in principle you can start with the major package for what you are interested in.

So section 2 just covers packages?

Yes, though there is an important subsection that covers all the "Analysis Packages". These are the packages that are involves with class mapping that I mentioned. These are covered in one subsection, because they all have the same "shape", with different versions for the parser, the typechecker and so on.

Okay, that that sounds important. Anything else we should know about in section 2?

Yes, the "Analysis Packages" subsection also describes the VDMJ visitor framework. That's quite important too.

Hold on, I thought you said that VDMJ uses class mapping instead of visitors?

It does for the main analyses. But visitors are still useful for small tasks, so there is a framework to support that.

Ah, okay. Anything else?

No, that's the important parts of section 2.

So what's in the final section 3?

Section 3 is very small and describes the way that VDMJ can call "out" to native Java code, and how a VDMJ interpreter can be created and controlled from a Java program, rather than from the command line.

So is that how libraries are implemented?

Often, yes. Though not all libraries make native Java calls.

Okay. And why would someone be interested in a Java program running the VDMJ interpreter?

Well, for example, this would allow you to create a GUI simulation in Java, with buttons and controls that look like the final environment of your system. But when you click on those GUI controls, you make VDM function calls to a model and get results back that tell you how to update the GUI. So it's about being able to put a friendly front-end on a model, which would allow end-users to try it out without special skills.

Oh, I see. That's quite useful then?

Only a few projects have used this feature, but yes, in principle it can be very useful to link Java and VDM systems at runtime.

Anything else I should know about the design doc?

No, that's about it.

Cool, thanks!