ADR-004: Syntax for Java-like annotations in TLA+ comments

authorrevision
Igor Konnov2

This ADR documents our decision on using Java-like annotations in comments. Our main motivation to have annotations is to simplify type annotations, as presented in ADR-002. Hence, in the following text, we are using examples for type annotations. However, the annotations framework is not restricted to types. Similar to Java and Scala, we can use annotations to decorate operators with hints, which may aid the model checker.

1. What can be annotated

Annotations should be written in comments that are written in front of a declaration. The following declarations are supported:

  1. Constant declarations, e.g., CONSTANT N.
  2. Variable declarations, e.g., VARIABLE x.
  3. Operator declarations, including:
  4. Top-level operator declarations, e.g., Foo(x) == e.
  5. Operators defined via LET-IN, e.g., Foo(x) == LET Inner(y) == e IN f.
  6. Recursive operators, e.g., RECURSIVE Fact(_) Fact(n) == ...
  7. Recursive and non-recursive functions including:
  8. Top-level functions, e.g., foo[i \in Int] == e.
  9. Functions defined via LET-IN, e.g.,Foo == LET foo[i \in Int] == e IN f

For an example, see Section 3.

2. Annotations syntax

An annotation is a string that follows the grammar (question mark denotes optional rules):

Annotation  ::= '@' tlaIdentifier ( '(' ArgList? ')' | ':' inlineArg ';' )?
ArgList     ::= (Arg) ( ',' Arg )*
Arg         ::= (string | integer | boolean | tlaIdentifier)
string      ::= '"' <char sequence> '"'
integer     ::= '-'? [0-9]+
boolean     ::= ('false' | 'true')
inlineArg   ::= <char sequence excluding ';' and '@'>

The sequence <char sequence> is a sequence of characters admitted by the TLA+ parser:

  • Any ASCII character except double quotes, control characters or backslash \
  • A backslash followed by another backslash, a single or double quote, or one of the letters f, n, r or t.

Examples. The following strings are examples of syntactically correct annotations:

  1. @tailrec
  2. @type("(Int, Int) => Int")
  3. @require(Init)
  4. @type: (Int, Int) => Int ;
  5. @random(true)
  6. @deprecated("Use operator Foo instead")
  7. @range(0, 100)

The above examples are just syntactically correct. Their meaning, if there is any, is defined by the tool that is reading these annotations. Note that the example 3 is not following the syntax of Java annotations. We have introduced this format for one-argument annotations, especially, for type annotations. Its purpose is to reduce the visual clutter in annotations that accept a string as their only argument.

Currently, annotations are written in comments that precede a definition (see the explanation below). String arguments can span over multiple lines. For instance, the following examples demonstrate valid annotations inside TLA+ comments:

(*
  @type: Int
            => Int
  ;
 *)

\* @type: Int
\*           => Int
\* ;

\* @hal_msg("Sorry,
\*           I
\*           CAN
\*           do that,
\*           Dave")

3. An annotated specification

The following specification shows how to write annotations, so they can be correctly parsed by the SANY parser and Apalache. Note the location of comments in front of: local operators, LET-definitions, and recursive operators. Although these locations may seem to be suboptimal, this is how the SANY parser locates comments that precede declarations.

-------------------------- MODULE Annotations ---------------------------------
EXTENDS Integers

CONSTANT
  \* @type: Int;
  N

VARIABLE
  \* the single-argument annotation
  \* @type: Set(Int);
  set

\* @pure
\* using the Java annotations, a bit verbose:
\* @type(" Int => Int ")
Inc(n) == n + 1

\* @type: Int => Int;
LOCAL LocalInc(x) == x + 1

A(n) ==
  LET \* @pure
      \* @type: Int => Int;
      Dec(x) == x + 1
  IN
  Dec(n)

RECURSIVE Fact(_)
\* @tailrec
\* @type: Int => Int;
Fact(n) ==
  IF n <= 1 THEN 1 ELSE n * Fact(n - 1)

\* @tailrec
\* @type: Int -> Int;
FactFun[n \in Int] ==
  IF n <= 1 THEN 1 ELSE n * FactFun[n - 1]

===============================================================================

4. Implementation

The implementation of the annotation parser can be found in the class at.forsyte.apalache.io.annotations.AnnotationParser of the module tla-io, see AnnotationParser.

5. Discussion

Most likely, this topic does not deserve much discussion, as we are using the pretty standard syntax of Java annotations. So we are following the principle of the least surprise.

We also support the concise syntax for the annotations that accept a string as a simple argument. For these annotations, we had to add the end marker ';'. This is done because the SANY parser is pruning the linefeed character \n, so it would be otherwise impossible to find the end of an annotation.