Package com.tnsai.annotations

Annotation Interface Contract

@Documented @Retention(RUNTIME) @Target({METHOD,TYPE}) public @interface Contract
Defines behavioral contracts for actions using Design by Contract principles.

Contracts specify preconditions, postconditions, and invariants that must hold for correct action execution. These are validated at runtime and can be used for formal verification.

Usage


 @ActionSpec(type = ActionType.LOCAL, description = "Transfer funds")
 @Contract(
     preconditions = {
         "amount > 0",
         "sourceAccount.balance >= amount"
     },
     postconditions = {
         "sourceAccount.balance == old(sourceAccount.balance) - amount",
         "targetAccount.balance == old(targetAccount.balance) + amount"
     },
     invariants = {
         "totalMoney == old(totalMoney)"
     }
 )
 public TransferResult transfer(Account source, Account target, double amount) {
     ...
 }

Expression Language

  • old(expr) - Value of expression before execution
  • result - Return value (in postconditions)
  • Standard Java expressions with parameter names

The annotated method must also carry @ActionSpec. Discovery fails if @Contract is present without it — the clause would otherwise never be evaluated.

Author:
TnsAI Team
See Also:

  • Nested Class Summary

    Nested Classes
    Modifier and Type
    Class
    Description
    static enum 
    Contract.InheritanceMode
    Defines how contracts are inherited.

  • Optional Element Summary

    Optional Elements
    Modifier and Type
    Optional Element
    Description
    Contract.InheritanceMode
    inheritance
    Contract inheritance mode.
    String[]
    invariants
    Invariants that must hold before and after execution.
    String
    message
    Custom message for contract violations.
    String[]
    postconditions
    Postconditions that must be true after action execution.
    String[]
    preconditions
    Preconditions that must be true before action execution.
    boolean
    strict
    Whether to throw exception on contract violation.
    boolean
    validate
    Whether to validate contracts at runtime.

  • Element Details

    • preconditions

      String[] preconditions
      Preconditions that must be true before action execution.

      Expressions use method parameter names.

      Returns:
      precondition expressions
      Default:
      {}

    • postconditions

      String[] postconditions
      Postconditions that must be true after action execution.

      Can use result to refer to return value and old(expr) to refer to pre-execution values.

      Returns:
      postcondition expressions
      Default:
      {}

    • invariants

      String[] invariants
      Invariants that must hold before and after execution.

      Typically used for class-level consistency constraints.

      Returns:
      invariant expressions
      Default:
      {}

    • validate

      boolean validate
      Whether to validate contracts at runtime.

      When false, contracts are documentation only.

      Returns:
      true to validate at runtime
      Default:
      true

    • strict

      boolean strict
      Whether to throw exception on contract violation.

      When false, violations are logged but execution continues.

      Returns:
      true to throw on violation
      Default:
      true

    • message

      String message
      Custom message for contract violations.
      Returns:
      violation message template
      Default:
      ""

    • inheritance

      Contract.InheritanceMode inheritance
      Contract inheritance mode.
      Default:
      STRENGTHEN