VDMJ Overview

So VDMJ is a tool for working with VDM specifications?

Yes, that's right.

What can it do?

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

That's pretty basic though?

Yes, sure. But it's a good start! After that, we can typecheck the specification.

Typecheck?

Yes. A VDM specification is a set of functions or operations that act on data of a given type. You can only do certain things with values of certain types. So, for example, you can add numbers but you can't add strings or sets; you can lookup a key value in a map, and the result will be that of the range of the map. 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 specification can have simulations run or tests generated and executed by an interpreter.

So that's just like a normal language 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 it allows you to look at the state of the specification and its variables.

Which sounds like a debugger?

Yes, 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 or operations, checking all of the constraints that the model identifies as it goes along.

So it's really slow?

It always surprises me when I see how fast it actually is! But yes, compared to the final implementation, the VDM model simulations are slow.

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.