Package com.tnsai.invariants

Annotation Interface InvariantCheck

@Retention(RUNTIME) @Target({TYPE,METHOD}) public @interface InvariantCheck
Enables automatic invariant checking on a class or method.

When applied to a class or action method, ActionExecutor asks the optional invariant provider to validate @State field invariants after execution. Planner expressions declared by @ActionSpec.precondition/postcondition are never runtime gates; use @Contract for dispatch-time contracts.

When applied to a method, only that action enables the state-invariant check.

Usage


 @InvariantCheck
 public class MyRole extends Role {

     @ActionSpec
     public void doSomething() {
         // @State field invariants are checked after execution
     }
 }

Or on specific methods: 


 public class MyRole extends Role {

     @InvariantCheck
     @ActionSpec
     public void increment() {
         count++;
     }
 }
Author:
TnsAI Team
See Also:

  • Optional Element Summary

    Optional Elements
    Modifier and Type
    Optional Element
    Description
    boolean
    checkInvariants
    Advisory switch for custom invariant integrations that perform general before/after checks.
    boolean
    checkPostconditions
    Advisory switch for custom invariant integrations that inspect this annotation.
    boolean
    checkPreconditions
    Advisory switch for custom invariant integrations that inspect this annotation.
    boolean
    checkStateInvariants
    Whether to check @State field invariants after method execution.
    boolean
    strict
    Whether to throw exceptions on violation.

  • Element Details

    • strict

      boolean strict
      Whether to throw exceptions on violation. If false, violations are only logged as warnings.
      Returns:
      true for strict mode (default)
      Default:
      true

    • checkPreconditions

      boolean checkPreconditions
      Advisory switch for custom invariant integrations that inspect this annotation. ActionExecutor does not evaluate planner preconditions; use @Contract for a runtime gate.
      Returns:
      true to check preconditions (default)
      Default:
      true

    • checkPostconditions

      boolean checkPostconditions
      Advisory switch for custom invariant integrations that inspect this annotation. ActionExecutor does not evaluate planner postconditions; use @Contract for a runtime gate.
      Returns:
      true to check postconditions (default)
      Default:
      true

    • checkInvariants

      boolean checkInvariants
      Advisory switch for custom invariant integrations that perform general before/after checks. ActionExecutor uses checkStateInvariants() for its explicit post-execution state validation.
      Returns:
      true to check invariants (default)
      Default:
      true

    • checkStateInvariants

      boolean checkStateInvariants
      Whether to check @State field invariants after method execution.
      Returns:
      true to check state invariants (default)
      Default:
      true