Annotations

Annotations attach metadata to declarations. They do not change behavior directly but are read by the Semantifyr toolchain (for example, to identify verification cases or to record traces).

Using an Annotation

The @ prefix attaches an annotation to the immediately following declaration.

@VerificationCase
class Reaches10 {
  contains counter: Counter

  prop {
    return AG counter.value < 100
  }
}

@Control
var value: int := 0

With Arguments

Annotation arguments use named-argument syntax (name = value).

@VerificationCase(summary = "Reaches the limit")
class Reaches10 {
}

@Tag(category = "slow")
class LargeTest {
}

Stacking Annotations

Multiple annotations may be applied to a single declaration. Each starts on its own @.

@VerificationCase
@Tag(category = "slow")
class LargeTest {
}

Declaring Custom Annotations

Without parameters:

annotation Important

With parameters:

annotation Description(text: string)

A custom annotation may then be applied like any built-in:

@Description(text = "Increments the counter by one")
tran increment() {
  value := value + 1
}

Standard Annotations

See the Standard Library for full details.

Annotation	Purpose
@VerificationCase	Marks a class as a verification target
@Tag	Categorizes verification cases
@Control	Marks a variable as important to track
@Shared	Marks containment feature instances as shared across instances
@Trace	Marks transitions for counterexample tracing