VDMJ Formal Verification

So you've explained that I can write a specification in a VDM dialect and then I can verify that formally in some way?

That's right. Formal verification gives you the highest level of confidence in your specification.

Are you suggesting you get some confidence without this step?

Yes, definitely! The simple act of writing your specification in VDM gives you some confidence, because you probably had to think of a lot more aspects than you realised, and your syntax will have been checked. Then if the typechecker has verified it, that gives you some extra confidence, because it means the types of everything are consistent, and so on.

And so on...?

Well, after the typechecker, you could partially check the runtime semantics by using the interpreter. That will give you yet more confidence that the operations and functions you specified are as you intended, and honour their constraints. Similarly, you can use combinatorial testing to automatically generate large numbers of tests -- perhaps millions -- that will be verified by the interpreter.

But this still isn't proof?

Exactly. No matter how many ad-hoc or combinatorial tests you perform, there could be some corner cases that you didn't think of that violate the constraints. If those cases are encountered when you go into production, the system could crash or produce invalid results.

Whether that's important is a different question...

Right, I mean sometimes I really don't care that much, surely?

Sometimes not, I agree. It just depends on your application and the true cost of any errors you make. But if you're using a formal specification, there's a good chance that you really care about the correctness of your design.

Yeah, about that...

About what?

You said "correctness". What does that mean, exactly?

Okay, I'm glad you're thinking about this. It's important to understand what we mean when we say a specification is correct or that its implementation has been 'proved to be correct'.

I'm assuming VDMJ can't read my mind, for example.

Sadly not. So we have to decide who or what is going to be the judge of correctness. In fact this point is so confusing that it's better to talk about proof of "internal consistency", rather than proof of "correctness", which includes the implementation.

Okay, but that just moves the goalposts... what does internal consistency mean?

It means your specification will always do what you said it should do, without reference to anything outside itself. That implies at least one implementation is possible, because the specification is self-consistent.

Hmmm... okay. But a normal program will always do what I said it should do, even if that's garbage in, garbage out?

Good point. But remember we were talking about the VDM method and specifying "what" rather than "how"? A program tells a computer how to calculate something or process some data or events or whatever, but that assumes this program is doing what we want. A formal specification is about defining what should be done by the implementation. If it's well written, it should be full of constraints that help us to understand what the final program should always/never do.

So internal consistency is about constraints?

Well, not really, but they help to define what a spec means. Consistency is about knowing that whatever we throw at the specification, if it meets the initial preconditions, then it will always produce a result which meets the final postconditions, without violating any state invariants, type invariants, loop invariants, recursive measures or internal preconditions along the way.

Without constraints, your specification is limited to the few implicit constraints that you get for free -- for example from the type system, limiting what values certain things can have. But explicit constraints help you to describe what your system must do in clear terms. For example, a state invariant helps to describe all of the state data in your model, by saying what must always or never be true about it, regardless of what operations you perform. You can define this using rules with sensible names, to make it explicit. It's the same with preconditions, postconditions and so on.

Okay, so suppose I write a specification and fill it with helpful constraints, and I've run it through the type checker and written tests and that all looks fine. What then?

You need to find out what has to be proved, in order to know that it will never violate its constraints.

And how do I do that?

You ask VDMJ to generate "proof obligations" (POs).

So obligations sound like something I have to do?

Yes. POs are small boolean expressions that describe what your specification must always do, or must never do. If all these expressions are always true, then your specification is internally consistent.

So what do I do with them?

You try to prove they are always true!

Sounds simple!! (Just kidding, it sounds quite hard?)

It can be, yes. It depends on your specification. VDMJ can help though.

You mean it can do these proofs for me?

Ah no, that requires a proof assistant. But VDMJ can sometimes disprove things very quickly, usually when you've made some very obvious mistakes.

But it doesn't help me prove these POs?

It may be able to show you that some obligations look easily provable. That's useful, because it tells you how healthy your specification is. But ultimately, you need to use a proof assistant to discharge proof obligations.

So it sounds like VDMJ will help you get yourself into a position where proof looks possible, but not actually complete those proofs for you?

That's about right. To do the final step, you would translate your specification and its obligations into another formalism and use its proof assistant. VDMJ can help with the translation, but not with the proof process after that.

But, hold on. If I have to translate it in order to prove it, why not just write the specification in this other formalism to begin with, if it has better proof support?

Okay, that's a good point. The problem is that the formalisms which have strong automated proof support have specification languages which are very terse and not very expressive. They have to be like that to enable the proof support. But that means if you want to specify something very complicated, it can mean a lot of very hard work to write it in the method's language.

But translating things is awkward too, surely?

Yes, it's not ideal. But the idea is that it's easier to write your specification in an expressive formalism, like VDM, and translate that automatically into a very complicated (but provable) version in another language. So you have the convenience of writing VDM, and the automatic translator has the problem of translating that into Isabelle/HOL or Lean or whatever.

Okay, I get the idea. So if I want to go through this process, where should I start?

I think it's best to start by looking at QuickCheck.