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. Who should read 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.

I imagine IDEs are much easier to use! So who would ever want to use the command line anyway?

The command line is very lightweight, in terms of the load on your machine. Everything comes in a single Java jar, which is about 2.4Mb. That's really small and fast, so if you already have a specification, it is often the easiest way to run simulations. And of course you can include it in 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?

So it starts by showing you how to use the command line options, for starting 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.

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

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

Okay. And the sources are just text files?

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

That sounds strange. Why would I 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. So you could print the document to read as normal, but you could also pass the same document to VDMJ and run simulations.

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

Briefly, yes. Seven formats are supported, but the tool can be extended to add more, easily.

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

It explains that typechecking happens automatically, and that there are no options for that phase.

Okay.

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