Annotations

Annotations were introduced in VDMJ version 4.3.0 as a means to allow a specifier to affect the tool’s behaviour without affecting the meaning of the specification. The idea is similar to the notion of annotations in Java, which can be used to affect the Java compiler but do not alter the runtime behaviour of a program. VDMJ provides some standard annotations, but the intent is that specifiers can create new annotations and add them to the VDMJ system easily. For more information on annotations, find the documentation here.

Output from the annotations is printed to the standard IO which can be found in the output view (View > Output) under a tab related to the workspace using the name sceme: "VDM: ", e.g. "VDM: AlarmPP".

You can choose to deactivate the stdio output view by setting: "vdm-vscode.server.stdio.activateStdoutLogging": false. This can speed up the execution of your specification if you have many print annotations in the specification. You can also choose to write the output to a file instead of to the output by specifying a path in the setting vdm-vscode.server.stdio.stdioLogPath.