Annotation Guide

So there's an Annotation Guide. What's that about?

It describes the standard VDMJ annotations and explains how to write your own.

Okay, can you quickly describe what an annotation is?

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