Annotations Guide Annotation
User Manual:
Open the PDF directly: View PDF 
.
Page Count: 7
| Download | |
| Open PDF In Browser | View PDF |
VDMJ Annotations Guide Date: 15/02/19 VDMJ Annotations Guide 0. Table of Contents 1. Overview...................................................................................................................................... 1 2. Syntax.......................................................................................................................................... 1 3. Location....................................................................................................................................... 2 4. Tool Effects.................................................................................................................................. 2 5. Loading and Checking................................................................................................................. 2 6. Standard Annotations.................................................................................................................. 4 6.1. @Override........................................................................................................................... 5 6.2. @Trace................................................................................................................................ 5 6.3. @NoPOG............................................................................................................................ 5 6.4. @Printf................................................................................................................................ 5 7. Creating New Annotations........................................................................................................... 6 1. Overview 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. 2. Syntax Annotations are added to a specification as comments, either block comments or one-line comments. This is so that other VDM tools will not be affected by the addition of annotations, and emphasises the idea that annotations do not alter the meaning of a specification. An annotation must be present at the start of a comment, and has the following default syntax: ‘@’, identifier, [ ‘(‘, expression list, ‘)’ ] So for example, an operation in a VDM++ class could be annotated as follows: class A operations -- @Override public add: nat * nat ==> nat add(a, b) == ... Or the value of variables can be traced during execution as follows: functions add: nat * nat +> nat add(a, b) == /* @Trace(a, b) */ a + b; Copyright © Nick Battle 2018 Page 1 of 7 VDMJ Annotations Guide 3. Date: 15/02/19 Location Annotations are always located next to another syntactic category, even if they do not affect the behaviour or meaning of that construct. In the examples above, the @Override annotation applies to the definition of the add operation, and the @Trace annotation applies to the expression a+b. Specific annotations may limit where they can be applied (for example, @Override only makes sense for operations and functions in VDM++ specifications), but in general annotations can be applied to the following: • To classes or modules. • To definitions within a class or module. • To expressions within a definition. • To statements within an operation body. In each case, the annotation must appear in a comment, by itself, before the construct concerned. Multiple annotations can be applied to the same construct, and may be interleaved with other textual comments, but each annotation must appear in its own comment. 4. Tool Effects Annotations can be used to affect the following aspects of VDMJ's operation: • The parser (for example) to enable or disable new language features. • The type checker (for example) to check for overrides or suppress warnings • The interpreter (for example) to trace the execution path or variables' values • The PO generator to (for example) skip obligations for an area of specification. Note that none of these examples affect the meaning of the specification, only the operation of the tool. Although it would be possible to create an annotation to affect a specification's behaviour, this is strongly discouraged. 5. Loading and Checking A global flag can be set by an "-annotations" command line argument, or the "set" command. This flag controls whether the comments in a specification are parsed for annotations. It defaults to false, so unless the command line switch or set command is used, no annotation processing will be performed. If the set command is used from within VDMJ, the specification must be reloaded to parse the comments: > set Preconditions are enabled Postconditions are enabled Invariants are enabled Dynamic type checks are enabled Pre/post/inv exceptions are disabled Measure checks are enabled Annotations are disabled > set annotations on Specification must now be re-parsed (reload) > reload > ... When annotations are enabled, comments are processed as follows by the parser: Copyright © Nick Battle 2018 Page 2 of 7 VDMJ Annotations Guide Date: 15/02/19 • All comments that precede class/modules, definitions, expressions and statements are collected by the lexical analyser and added to the corresponding AST node by the parser. • The parser checks the comments in an annotated node, looking for those that start with @. • Each comment that looks like an annotation is used to attempt to load a Java class called AST Annotation from a configurable classpath. If the class cannot be found, the comment containing the annotation is silently assumed to coincidentally contain something that is a valid annotation syntax, but which is not actually an annotation - like using @NickBattle to refer to a person by their Twitter handle. • For the annotation classes that load successfully, the parser instantiates each annotation, and calls it to parse the rest of the comment. By default, this will parse an optional list of expressions between brackets, but each annotation can override the "parse" method to handle its own argument syntax. • An "astBefore" method on the annotations is called, passing the SyntaxReader that is currently processing the specification. This allows the annotation to affect the parse of the syntactic element that follows the annotation. • The parser parses the element following the comments using the SyntaxReader. • The parser calls an "astAfter" method on the annotations after the parse of the element, passing the SyntaxReader and the parsed AST node, to allow the annotation to affect the result of the parse or undo any changes it made to the SyntaxReader. • The parse then continues as normal. Note that so far there has been no checking of the annotation itself, other than its syntax. If VDMJ correctly parses an entire specification, it next performs type checking. This is done by converting the tree of AST objects into an equivalent tree of TC objects. This includes annotations that are attached to AST nodes - AST Annotation objects are converted to TC Annotation objects, loaded from the same classpath, which contain code to type check the annotation itself as well as code which may affect the type check of the annotated element. Type checking proceeds as follows: • When the TC tree is created, AST Annotation objects from the parse are converted to TC Annotation objects. • When the type checker starts, it calls a static "doInit" method on all loaded TC annotations. This allows them to reset or set up any persistent data that they require. • Before the type check of an annotated element, the type checker calls the "tcBefore" method of annotations attached to the node, passing the TC node of the element and the Environment list. • The type check of the annotated element then proceeds as normal. • After the type check, the "tcAfter" method of the annotations is called, passing the TC node and Environment as before, but also passing the TCType of the checked node. The annotation typically uses the "tcBefore" method to type check its arguments (if necessary) and check anything it needs to check about the annotated TC node. For example, the @Trace annotation checks that its arguments are simple variable identifiers that are in scope; and the @Override annotation checks that there are no arguments, that the dialect is VDM++, that the definition annotated is an operation or function and that there is a superclass that has a definition which is being overridden by the annotated element. After the type checking phase, if there are no errors, VDMJ will normally create a tree for the Copyright © Nick Battle 2018 Page 3 of 7 VDMJ Annotations Guide Date: 15/02/19 interpreter: TC classes are converted to IN classes, and this includes annotations. Annotations which apply to classes/modules and definitions do not affect the interpreter, but those that apply to statements and expressions do (since these elements are "executed"). Execution proceeds as follows: • When the IN tree is created, TC Annotation objects are converted to IN Annotation objects. • When the interpreter is initialised, it calls a static "doInit" method in all loaded IN annotations. This allows them to reset or set up any persistent data that they require. • When an annotated INStatement or INExpression is executed, the evaluation first calls the "inBefore" method of the annotations, passing the statement or expression and the runtime Context stack. • The statement or expression is then evaluated as normal. • The evaluation then calls an "inAfter" method on the annotations, passing the statement or expression, the runtime Context and the Value from the execution. The annotation cannot affect the return value. • Finally the return value is returned as usual and the overall evaluation proceeds as normal. The inBefore and inAfter methods allow annotations that affect the interpreter to either intervene before the annotated element is evaluated or to look at the result after its execution (or both). If PO generation is required, the TC tree is used to generate a tree of PO objects, including PO Annotation classes. Proof obligation generation then proceeds as follows: • When the PO tree is created, TC Annotation objects are converted to PO Annotation objects. • When PO generation starts, it calls a static "doInit" method in all loaded PO annotations. This allows them to reset or set up any persistent data that they require. • Before any annotated class/module, definition, statement or expression is processed by the PO generator, the "poBefore" method of the annotations is called, being passed the POContextStack and the PO node concerned. • PO generation of the PO node then proceeds as normal. • After the PO generation, the "poAfter" method of the annotations is called, passing the POContextStack, the PO node and the ProofObligationList generated by the node. These can be modified by the "poAfter" method - for example, the @NoPOG annotation clears the obligation list. Note that the same annotation (that is, one @Name comment in the source) can affect all four areas of VDMJ operation, though to do so it needs to define code in the AST, TC, IN and PO trees. If an annotation affects the type checker, but not (say) the interpreter, the TC-IN mapping for the annotation should map TC Annotation to INNullAnnotation, which does nothing. The same principle applies to other unused analysis mappings; all annotations must define AST Annotation. 6. Standard Annotations VDMJ includes some standard annotations. They are provided in a separate jar file which needs to be on the classpath when VDMJ is started. If the jar is not on the classpath, annotations will be silently ignored. The standard annotations perform the following processing: Copyright © Nick Battle 2018 Page 4 of 7 VDMJ Annotations Guide 6.1. Date: 15/02/19 @Override This is very similar to the Java @Override annotation, which is used to verify that a Java method overrides a superclass method, raising an error if not. In VDMJ, the override applies to operations or functions in a VDM++ class. The typecheck of the annotation (in the TCOverrideAnnotation "tcBefore" methods) verifies that the dialect is VDM++, that the annotation has no arguments, and that it is applied to either an operation or a function definition. Lastly, if there is no "inherited" definition that this definition overrides, an error is raised. Error 3363: Definition does not @Override superclass in 'A' (test.vpp) at line 3:9 The annotation has no effect on the interpreter or the PO generator. 6.2. @Trace The @Trace annotation is intended to trace the flow of control in the interpreter, either to note that a particular point in the execution has been reached, or to log the values of variables at that location. The typechecker checks (in the TCTraceAnnotation "tcBefore" methods) that the annotation is applied to a statement or an expression only. The check also makes sure that any arguments supplied are simple variable names and refer to variables that are in scope. When the interpreter is running, the INTraceAnnotation "inBefore" method either just prints out the current location to stderr, or it prints the location and " = " for each argument (ie. each variable name traced). For example, the specification in section 2 produces the following: > p add(1,2) Trace: in 'A' (test.vdm) at line 9:13, A`a = 1 Trace: in 'A' (test.vdm) at line 9:13, A`b = 2 = 3 Executed in 0.007 secs. The annotation has no effect on the execution values or the PO generator. 6.3. @NoPOG The @NoPOG annotation is intended to suppress PO generation over a region of the specification. It can be applied to a class/module, a definition, a statement or an expression. The typechecker (the TCNoPOGAnnotation "tcBefore" methods) just checks that the annotation has no arguments passed. Error 3361: @NoPOG has no arguments in 'A' (test.vdm) at line 9:13 The PO generator (the PONoPOGAnnotation "poAfter" methods) clear the list of proof obligations generated for the annotated element (class/module, definition, statement or expression). The annotation has no effect on the interpreter. 6.4. @Printf The @Printf annotation is almost identical to the IO`printf library operation, except that as an annotation it can be used in functions as well as operations, and the arguments do not have to be presented as a sequence literal. Copyright © Nick Battle 2018 Page 5 of 7 VDMJ Annotations Guide Date: 15/02/19 The typecheck (the TCPrintfAnnotation "tcBefore" methods) checks that the annotation has a string as its first argument. Execution of the annotation (the INPrintfAnnotation "inBefore" methods) evaluate the arguments and then pass the Values generated to System.out.printf. Note that, as with IO`printf, the format string can only contain %s converters, even if the values being printed are numeric. 7. Creating New Annotations Creating new user annotations is a matter of doing the following: • Write a new AST Annotation class that extends ASTAnnotation. Annotations that don't affect the parse do not have to implement any methods; there are "astBefore" and "astAfter" methods that will be called during the parse, if required (see above). • Write TC, IN and/or PO Annotation classes that extend TCAnnotation etc. and add the checking and functionality that you require in the before/after methods. • Create the mapping file lines that map the new classes for AST-TC, TC-IN and TC-PO. For example to add two new annotations called @Notice and @Classic, produce an asttc.mappings file like this: package annotations.ast to annotations.tc; map ASTNoticeAnnotation{name, args} to TCNoticeAnnotation(name, args); map ASTClassicAnnotation{name, args} to TCClassicAnnotation(name, args); • Put the new classes and the necessary mapping files on the classpath when VDMJ is executed. This is easily done by putting them in a jar file, with the mapping file(s) at the top level. Use the property vdmj.annotations to set the classpath for the annotation classes, unless you use the standard annotations.ast package for them. • Add @Name comments to your specification :-) Note that VDMJ is issued with @Override, @Trace and @NoPOG annotations in a separate "annotations" jar. This contains the classes and mapping file extracts required for the standard annotations. The source (in GitHub) may be a useful resource for producing new annotations. The layout of the jar is as follows: Copyright © Nick Battle 2018 Page 6 of 7 VDMJ Annotations Guide Date: 15/02/19 Copyright © Nick Battle 2018 Page 7 of 7
Source Exif Data:
File Type : PDF File Type Extension : pdf MIME Type : application/pdf PDF Version : 1.5 Linearized : No Page Count : 7 Language : en-GB Title : Annotations Guide Creator : Writer Producer : LibreOffice 6.1 Create Date : 2019:02:15 12:36:48ZEXIF Metadata provided by EXIF.tools