Annotation Guide

So there's also an Annotation Guide. What's that about and who should read it?

It describes the standard VDMJ annotations and explains how to write your own. It would be useful for anyone wanting to use standard annotations, and it is essential reading for people who want to write them.

Okay, can you quickly describe what an annotation is?

They are comments in a VDM specification that prefix something else, like a function or an expression. They look similar to annotations in Java, with a default syntax like @SomeName(arg1, arg2) or just @OtherName. When VDMJ is processing whatever has been annotated, it can be influenced by the presence of the annotation.

For example?

You could add -- @Warning(5000) before a definition to suppress warning 5000 ("definition is not used").

Ah, okay, so that one is affecting the type checker?

Yes, in that case. You can affect the parser, the type checker, the interpreter, PO generator or any other user supplied analyses. And the annotations themselves can be type checked too. So in this example, the @Warning annotation takes a list of error numbers as arguments, and that is checked.

You said that you can write your own annotations?

Yes, and the way to do that is described in the document. You can also look at the source of the standard annotations, of course. Typically they are very small pieces of code. To use them, you add a jar with your code to the classpath of VDMJ.

And then you can just start adding them to your spec?

You have to enable annotations as well, either by passing -annotations to the command line, or using set annotations on at the interpreter prompt, which will prompt you to reload the specification. If you don't do this, annotations are ignored as harmless comments.

Okay, I think I get the idea, thanks!