User Guide

So there's a User Guide for VDMJ?

Yes. It's just over 50 pages.

That's way too long to read, unless it's really useful. So who should bother reading this?

Well, I take your point. It's long, but there is a lot to say. It's intended for people who want to work with the command line version of VDMJ. So it doesn't include anything about the IDEs, Eclipse or VSCode, or editors.

I imagine IDEs and editors are much easier to use though. So who would ever want to use the command line anyway?

The command line is lightweight, in terms of the load on your machine. The core functionality comes in a single 2.4Mb Java jar. That's really small and fast, so if you already have a specification, it is often the easiest way to run ad-hoc simulations. And of course you can run it from other scripts, which may also be useful.

OK, I see. So obviously I could read the User Guide for the details, but roughly what does the document tell me?

It starts by telling you about how to install the distribution ZIP.

But you said it was a single jar?

The ZIP contains that jar, yes. But it also contains libraries and documents and a useful script called vdmj.sh for running the tool as well. So you just unzip this somewhere, put that folder on your $PATH, and you're ready to go.

Ah, okay. Then the Guide shows me how to use it?

Right. So after the installation section, it shows you all the command line options, for running the tool. Some are mandatory, like the dialect of VDM to use; others are optional, like whether you want to start the interpreter or suppress warnings and so on. You can see a list of options by using the help option, like java -jar vdmj-4.n.n.jar -help.

And presumably I should pass the names of the specification source files that I want to use too?

Normally, yes. Though if you don't have any sources yet, you can still start an interpreter and evaluate expressions, which is useful when you first start writing VDM.

Okay. And VDM specification files are just plain text?

That's the default, yes. Though VDMJ can also extract VDM source from other formats, like LaTeX or Word documents.

That sounds strange. Why would anyone do that?

Imagine you had a Word document that described a project in plain English, with an Appendix that had a formal definition of various aspects, written in VDM. You could give people the document to read as normal, but you could also pass the same document to VDMJ and run simulations using the appendix directly. So the document becomes a testable artifact.

Oh yes, nice. And this is described in the User Guide?

Briefly, yes. Six 'external' formats are supported out of the box, but the tool can be extended to add more, easily. There's another document about that.

Okay, we can look at that later. But back to the User Guide. What else does it cover?

It explains that syntax and type checking happens automatically, and that there are a few options for those phases, like choosing a language version, strict parsing or suppressing warnings.

Okay.

Then it shows you what options are available if you enter the interpreter.

Enter?

If you use the -i command line option, and there are no syntax or type errors, it will start an interactive session where you can evaluate expressions using the interpreter. So if you ask it to print 1 + 1 it will say = 2. When you've finished your session, you use quit to leave the tool.

Can I ask it to evaluate one expression without using an interactive prompt - say from a script?

Yes, you can pass any expression with the -e <exp> option, instead of -i. That is equivalent to using print <exp> followed by quit. You can run any single command like this using -cmd <command>. So -e <exp> is equivalent to -cmd "print <exp>".

Okay, good. But usually you wouldn't just be doing basic arithmetic like 1 + 1?

No, with a loaded specification you would typically run a test function, like print runLifecycle(). The print command is the simplest way to start an evaluation. There are lots of other commands you can use from the interpreter prompt though.

So, without all the details, what sorts of other things can you do at the interpreter prompt?

Well, a help command lists them all. But you can list the loaded files and modules; you can run traces; you can check files of assertions; you can run scripts of other commands; you can look at the environment and state data; you can re-initialize the specification; you can manage breakpoints; you can see how much of the specification has been covered by executions; you can generate proof obligations; you can reload a changed specification; or you can quit.

Wow! That's a lot. You said that from memory?

No, I read the User Guide :-P

Okay, fair enough. So does the User Guide cover anything else?

Yeah, after the section about the interpreter, it describes how to use the debugger.

Okay, you mentioned this before. You can debug a specification, a bit like a normal program?

Yes, though remember a VDM evaluation is more complicated than running a simple program: lots of things are being checked for you along the way.

These are the pre/postconditions and other things?

That's right. We usually talk about "model constraints". These are checked all the time as functions are evaluated.

But I can still stop at a breakpoint in the usual way?

Roughly, yes. But when you step forward you may see unusual things happening. So if you try to call a function with a precondition, it will jump there first, then enter the function; if you try to create a value of a type with an invariant, its value will be checked; if you have state invariants, then changing state values will jump to those checks, and so on.

It sounds very confusing!

At first, perhaps. Wait till you try to debug a specification with multiple threads! But it is a fundamental part of what the specification is doing for you: checking that everything is consistent.

You can define threads in VDM?

In the VDM++ and VDM-RT dialects, yes.

So that raises a lot of questions... but let's stick to the User Guide for now. What comes after the debugging section?

It briefly describes "sessions", which is the intuitive idea that the state of a specification evolves as you call successive functions, rather than starting from scratch for each print. It's only mentioned because it gets more subtle if you have threads running.

Yeah, I bet. But let's stick to the Guide. Is there any more?

It describes how to interrupt and debug evaluations that seem to be looping. That's obviously useful, if things seem to be stuck.

Okay.

Then it describes the three standard libraries that you can use.

Right, hold on. How can a specification use a library? It specifies my own system, not a "standard" one, surely?

Yeah, it is slightly odd. But for example, quite a lot of specifications find that they want to do mathematical operations that are not built into the language. You can do the obvious arithmetic operations on numbers, but you cannot calculate a square root in pure VDM, for example. So there is a MATH library with a function called sqrt.

Ah! Okay, I get it, that makes more sense.

Right. Then there is a section on JUnit testing.

But... you've lost me again. JUnit is for Java code testing, it's got nothing to do with VDM?

True. But there is a feature of VDMJ that allows you to evaluate VDM functions from within a JUnit test. So, for example, you could write JUnit tests within a Maven framework, define VDM tests in a Word document, and have those automatically executed to test your VDM model as part of the build of your system.

So hold on... the real system is written in Java. The specification is written in VDM. The tests are written in Word, with embedded VDM. And I can run JUnit tests using the Word document as well as the real system, all from the same Maven POMs?

Yes, using the feature described in the User Guide, though I admit this would be for more sophisticated users. The really interesting idea is to try to compare the results of the VDM tests with the equivalent tests in the real system.

But they're different things?

Well, yes and no. The specification describes the system; the system implements the specification. So it ought to be possible to compare the behaviour of the model with the real system automatically. Of course, you would have to interpret the abstract results of the VDM to compare them with the real results.

But doesn't that mean that the continuous integration build would keep failing, if the system didn't ...

Yeah, you've got it. It means you can't check in code that doesn't match the formal specification. Cool huh?

That's... interesting! But again, let's stick to the User Guide for now. Is there more?

Yup. Combinatorial Testing is described next.

So what's that?

Read the Guide! But seriously, you can add "traces" to a specification, which allows you to generate thousands or millions of tests. The section describes how to write, execute and debug generated tests. But it's really just an overview. There is a much more detailed Combinatorial Testing Guide available.

Okay, my head is spinning a bit now. Is there anything else in the User Guide?

There's a section that introduces annotations, but there is a more detailed Annotation Guide that covers those too.

So quickly, what's an annotation?

They're a way to add functionality to a specification without changing what the specification means. So for example you can use an @Warning annotation to suppress particular warnings, if you are sure they are harmless.

Okay, is there anything else?

The final section covers internationalization. There are command line options to allow specifications to be written in different character encodings, so the tool can be used by Japanese or Greek users, say.

And that's all?

A couple of appendixes, one explaining VDMJ's Java properties, but yes, that's all.

Phew! So there's a lot in the User Guide. Thanks for explaining it all.