VDMJ Overview

So VDMJ is a tool for working with VDM specifications?

Yes, that's right.

Why the 'J'?

It just indicates that the tool is written in Java.

And I think I read somewhere that it's a command line tool?

It has a command line interface built-in, yes. But you can also use it via an IDE, like Eclipse or VSCode. You can also use it with some editors, like Kate and Neovim.

OK, sounds good. So what can it do?

The simplest thing it can do is to check the syntax of what you've written.

Hold on, I haven't written anything yet. Doesn't it let me do that?

The command line assumes that you have a complete VDM specification already written. But obviously an IDE or editor will allow you to write one on the fly.

Okay, but that's pretty basic though? A syntax check, I mean?

Yes, sure. But it's an important start. After that, it will typecheck the specification.

Typecheck?

Yes. A VDM specification is a collection of functions that act on data of particular types. You can only do certain things with values of certain types.

You mean types like numbers and strings?

Right. So, for example, you can add numbers together but you can't add strings or sets in the same way; arguments that you pass to a function have to be a particular type and so on. You can analyse the entire specification for its type use and show that all of the actions will have data of the correct type when they are executed.

That sounds like the checking that a normal compiler does.

Yes, it's very similar.

And then?

After a successful typecheck, the tool can run simulations or generate tests to be executed by an interpreter.

So that's like a normal language interpreter running a program?

It's similar, but remember that there are a lot of constraints that have to be checked as a VDM specification is executed. So if any preconditions or postconditions are violated, or any state or type invariants are violated, the evaluation will stop and allow you to look at where you are and see the variables, to find out why you broke a rule.

Which sounds like a debugger?

Again, it's similar, but this isn't a program.

It's something that will become a program?

That's a good way to put it, yes. It's an abstract model of a system that we intend to build. The interpreter calculates values and calls functions, checking all of the constraints that the model identifies as it goes along.

That sounds really slow?

It always surprises me when I see how fast it actually is. But yes, compared to the final program implementation, model simulations are really slow. But that doesn't matter: we only want to know that the flow of logic is valid.

Hmm. So if all of the test simulations pass, you know that the specification of the system is valid, in some sense?

Yes. It means that if you implement what was specified, and the inputs meet all of the preconditions you defined, the system will behave in a way that meets all of the postconditions you defined, without violating any of the constraints. That's a very strong position to be in, when you start implementing something.

Yeah, I can see that! So, is there anything else VDMJ can do?

Lots of things, yes. But we're really creeping into what is covered in the User Guide now.

Okay, let's talk about that next.