External Format Guide

You mentioned external formats when we were talking about the User Guide. So I assume the External Format Guide tells us more about that?

Yes. If you remember, the idea was that you could embed a VDM specification, or parts of one, in a document - perhaps an appendix in a Word document, or as part of a paper written in LaTeX.

Right, that's an interesting idea.

It means that the specification is a testable artifact. And you only have one official source for the specification, which avoids the pitfall of having an updated document but an out of date model file.

We've all been there.

Quite. So out of the box, VDMJ supports various formats - we call them 'external' formats. You can embed VDM in Word, LaTeX, ODF, markdown or AsciiDoc.

What's ODF?

The OpenDocument format. That's used by LibreOffice and various other tools.

Ah okay. So why do we need an External Format Guide?

The guide is really about how to write new external format readers. I would have called it the External Format Reader Writer's Guide, but...

...yeah...

It's very simple. You just have to implement a Java interface, which includes a single method to "getText" the VDM source from the file. To start using your class, you set a Java resource or property that associates your class with a given filename extension, like *.pdf.

Sounds easy?

Yes, it should be. The more interesting thing is what you can use external readers for.

Reading more external formats?

Well, that yes. But you can also do much more interesting things, and there are some ideas listed in the guide.

Intriguing. Can you give us a hint?

For example, you could create an external reader for *.database files, then use the content of that file to open a database connection, query a few tables and suck out the data that you want, then return those results formatted as VDM values.

Woah! OK, I see, that's much more than simply extracting VDM from a document.

That's right. It's really a way of generating arbitrary VDM source from another data source. That means that you can link a model with genuine data sources for simulations, rather than trying to "convert" data and possibly making errors.

I get it. That's really quite a powerful feature!