VDMJ Overview

OK, so what is this thing all about?

VDMJ you mean?

That's why we're here, yeah.

Right. Well, do you know what VDM is - the Vienna Development Method?

Something about Austria? LOL, okay I have some idea, it's something to do with formal development?

That's right. It was originally developed at the IBM Laboratories in Vienna in the 1970s. It's a way to formally specify computer systems.

Sounds ancient.

I suppose so, yes. But the theory that underpins it is still sound. And it's quite easy to learn and use.

Ah, right, so I could learn about formal specification quickly with VDM and then move on to something else?

Exactly.

So lots of places teach VDM for that reason?

I don't know about lots, but it's definitely used for teaching at Aarhus University in Denmark and Newcastle in the UK. There are others.

Okay, so if I understand this, I can use VDM to write a specification of a system in a special language?

Yes.

And then do what with it? I mean, why would I bother?

So the first thing to understand is that your specification will be a lot smaller than the final system that you write your programs in.

Yeah, okay, so it must be condensed somehow, or not cover everything?

Yes. We call it an abstract model: it describes some aspect of your system, but not every little detail.

Still not seeing why that helps?

Well, by writing down how you intend it to work, that forces you to think carefully about what you really mean. Then the tools will help you to check that what you say is consistent, and ultimately allow you to run simulations of the final system.

Before it's written?

Yes, ideally. Sometimes you might write models in parallel with the development, or to help unpick something that has been developed. But ideally you want to produce the model first.

Doesn't that just slow everything down? Time is money.

It's time well spent. If you stumble into a development without understanding something fundamental about what you need to do, there is a good chance that you will have to throw away a lot of code. The later that happens, the more expensive it is. Formal modelling gives you confidence that you are building something that does what you want, without nasty surprises.

That sounds too good to be true!

You can still get things wrong, or spend too much time modelling. It's not foolproof. But it's a technique that is there to help.