Expand description
Abstract Syntax Tree for the Specl specification language.
Structs§
- Action
Body - Action body with requires and effects.
- Action
Decl action NAME(params) { body }- Binding
- A variable binding
x in S. - Const
Decl const NAME: Typeorconst NAME: value- Expr
- An expression.
- Fairness
Constraint - A fairness constraint.
- Fairness
Decl fairness { constraints }- Func
Decl func NAME(params) { body }User-defined helper function for reuse (like TLA+ operator definitions). Functions are pure and are inlined at call sites during compilation.- Func
Param - A function parameter (untyped - types are inferred).
- Ident
- An identifier with its source span.
- Init
Decl init { expr }- Invariant
Decl invariant NAME { expr }- Module
- A Specl module (top-level compilation unit).
- Param
- A parameter declaration.
- Property
Decl property NAME { expr }- Type
Decl type NAME = Type- UseDecl
use ModuleName- VarDecl
var NAME: Type
Enums§
- BinOp
- Binary operator.
- Const
Value - The value of a constant declaration.
- Decl
- A top-level declaration.
- Expr
Kind - The kind of expression.
- Fairness
Kind - Kind of fairness constraint.
- Quantifier
Kind - Quantifier kind.
- Record
Field Update - A record field update.
- Type
Expr - A type expression.
- UnaryOp
- Unary operator.