This page describes the CASM syntax by describing the complete Extended Backus–Naur Form (EBNF) grammar rules.
Specification ::= Header Definitions
Every CASM specification consists of a header and definitions part.
Header ::= Attributes "CASM"
| "CASM"
In the header part the keyword CASM required to denote the start of a CASM specification. Optional attributes can be specified as well.
Definitions ::= Definitions AttributedDefinition
| AttributedDefinition
Definitions consist of one or more attributed definition.
AttributedDefinition ::= Attributes Definition
| Definition
An attributed definition consists of a definition with optionally Attributes assigned to it.
Definition ::= InitDefinition
| EnumerationDefinition
| DerivedDefinition
| RuleDefinition
| FunctionDefinition
| UsingDefinition
| UsingPathDefinition
| InvariantDefinition
| ImportDefinition
The Definition grammar rule defines all possible CASM definition sections.
InitDefinition ::= "init" IdentifierPath
| "init" "{" Initializers "}"
An init definition is used to specify and control the initialization phase of the ASM agents during a run of an CASM specification.
The possible initialization variants are:
IdentifierPath.Initializers which are surrounded by curly brackets.0.2.0.
It was indirectly present in version 0.1.0 by now it has its own dedicated AST representation.
EnumerationDefinition ::= "enumeration" Identifier "=" "{" Enumerators "}"
An enumeration definition allows to declare user-defined enumeration
types (domains) in a CASM specification.
Every enumeration is identified by its Identifier and creates with
the same name a namespace in the specification for all of its Enumerators.
0.1.0.
DerivedDefinition ::= "derived" Identifier "->" Type "=" Term
| "derived" Identifier "(" Parameters ")" "->" Type "=" Term
A derived definition enables to specify derived functions
which are identified by its Identifier name.
If a derived has parameters, the function signature has to be fully typed.
By default a derived Term is side-effect free in the sense that it does
not produce any updates to modify the ASM in any way.
Additionally a derived function can be attributed by pure to indicate
that the result of the defined Term can be statically computed at compile-time.
0.1.0.
RuleDefinition ::= "rule" Identifier "=" Rule
| "rule" Identifier "->" Type "=" Rule
| "rule" Identifier "(" Parameters ")" "=" Rule
| "rule" Identifier "(" Parameters ")" "->" Type "=" Rule
A rule definition defines a named rule which is identified by its Identifier name and an assigned Rule to it. Every rule definition can have zero, one, or multiple typed Parameters and an optionally return Type.
0.1.0.
Void.
The following two examples of the rule foo and bar have the same type relation representation:
rule foo( x : Integer, y : String ) = skip rule bar( x : Integer, y : String ) -> Void = skip
Type (not Void) of a rule will be supported in version 0.5.0.
For now every rule is defined as n-ary function relation type with result type Void.
FunctionDefinition ::= "function" Identifier ":" MaybeFunctionParameters "->" Type MaybeDefined MaybeInitially
A function definition enables the creation of global ASM state functions with a defined type relation. Additionally every function initial state can be specified through MaybeInitially.
Furthermore, due to the fact that ASM functions are by default undef (undefined) over the whole value domain, the MaybeDefined optionally enables the definition of a defined default value.
0.1.0.
In order to evaluate a CASM function as symbolic in the symbolic/concolic execution and include it in the TPTP trace, the function has to set the attribute symbolic
symbolic is introduced in version 0.6.0.
EnumeratorDefinition ::= Identifier
| Attributes Identifier
An enumerator definition are Identifier with optionally Attributes assigned to them.
0.1.0.
Enumerators ::= Enumerators "," EnumeratorDefinition
| EnumeratorDefinition
Consist of one or more EnumeratorDefinition which are separated by a comma character.
UsingDefinition ::= "using" Identifier "=" Type
A using definition enables to define type aliases which are identified by its Identifier and assigned to a certain Type.
Integer named MyType:
using MyType = Integer
0.1.0.
UsingPathDefinition ::= "using" IdentifierPath
| "using" IdentifierPath "::" "*"
A using path definition makes symbols of imported module determined by its IdentifierPath visible in the current specification.
If the symbol path ends with an star (*), then all symbols of the specified module path are made visible in the current specification.
0.5.0.
InvariantDefinition ::= "invariant" Identifier "=" Term
An invariant definition allows to globally specify a condition (constrain) which has to be fulfilled during the whole ASM run.
Therefore, the invariant identified by its Identifier name gets checked of the current ASM state during all ASM steps.
If an invariant does violate the defined condition (constrain) an exception is raised.
0.2.0.
ImportDefinition ::= "import" IdentifierPath
| "import" IdentifierPath "as" Identifier
Through the import definition it is possible to load external specifications and modules into the specification.
The provided identifier path is used to search inside the specification base path for the requested specification.
If the imported specification does belong to an external module, the import has to be defined externally via a CASM project YAML file.
By default, if no import renaming (as identifier) is specified, the last identifier in the given import path is used.
0.4.0.
Rules ::= Rules Rule
| Rule
Consists of one or more Rule grammar rules.
Rule ::= SkipRule
| ConditionalRule
| CaseRule
| LetRule
| LocalRule
| ForallRule
| ChooseRule
| IterateRule
| BlockRule
| SequenceRule
| UpdateRule
| CallRule
| WhileRule
The Rule grammar rule defines all possible CASM rules.
SkipRule ::= "skip"
The skip rule defines that no operation or rule shall be performed
at this position in a CASM specification.
0.1.0.
ConditionalRule ::= "if" Term "then" Rule
| "if" Term "then" Rule "else" Rule
The conditional rule provides a branching facility to evaluate a certain sub-rule if the guarding Term is true.
Additionally an else rule can be specified to be evaluated if the condition is not fulfilled.
0.1.0.
CaseRule ::= "case" Term "of" "{" CaseLabels "}"
A case rule allows to define multiple cases through CaseLabels which are evaluated if the given Term matches the specified CaseLabel.
0.1.0.
CaseLabels ::= CaseLabels CaseLabel
| CaseLabel
Consist of one or more CaseLabel grammar rules.
CaseLabel ::= "default" ":" Rule
| "_" ":" Rule
| Term ":" Rule
A case label defines the matching Term and the Rule to be evaluated if the case expression matches.
To specify a default case and Rule to be evaluated if no match is found, the keyword default or the underline (_) character can be used.
LetRule ::= "let" VariableBindings "in" Rule
A let rule defines a new scope where the defined VariableBindings are used
for the evaluation in the sub-rule Rule.
0.1.0.
LocalRule ::= "local" LocalFunctionDefinitions "in" Rule
The local rule defines a function definition in the current rule scope.
Therefore, it represents a local state inside a given rule.
0.5.0.
ForallRule ::= "forall" AttributedVariables "in" Term "do" Rule
| "forall" AttributedVariables "in" Term "with" Term "do" Rule
A forall rule defines AttriubtedVariables which range in a given domain Term to evaluate (do) a specified Rule in parallel.
Additionally a filter condition can be specified by with.
0.1.0.
ChooseRule ::= "choose" AttributedVariables "in" Term "do" Rule
A choose rule allows to specify a selection of AttributedVariables to be chosen in a given Term one value per variable to evaluate a given rule.
0.1.0.
IterateRule ::= "iterate" Rule
A iterate rule specifies that a certain Rule gets iterated as long as it
does not produce any more updates.
0.1.0.
BlockRule ::= "{" Rules "}"
| "par" Rules "endpar"
The block rule specifies that given Rules shall be evaluated with a parallel execution semantics.
0.1.0.
SequenceRule ::= "{|" Rules "|}"
| "seq" Rules "endseq"
The sequence rule specifies that given Rules shall be evaluated
with a sequential execution semantics.
0.1.0.
UpdateRule ::= DirectCallExpression ":=" Term
The update rule specifies the producing of changes to the
ASM global state by assigning a Term to a function symbol.
0.1.0.
CallRule ::= CallExpression
A call rule allows to invoke other named rules (RuleDefinition).
0.1.0.
WhileRule ::= "while" Term "do" Rule
The while rule is a CASM syntactical sugar for an iterate rule , conditional rule, and skip rule.
while rule as:
iterate
if not <Term> then
skip
else
<Rule>
0.1.0.
Terms ::= Terms "," Term
| Term
Consist of one or multiple Term grammar rules separated by comma characters.
Term ::= SimpleOrClaspedTerm
| TypeCastingExpression
| OperatorExpression
| LetExpression
| ConditionalExpression
| ChooseExpression
| UniversalQuantifierExpression
| ExistentialQuantifierExpression
| CardinalityExpression
The term grammar rule defines all possible term expressions which are available in the CASM specification language.
SimpleOrClaspedTerm ::= "(" Term ")"
| CallExpression
| LiteralCallExpression
| Literal
| "+" SimpleOrClaspedTerm
| "-" SimpleOrClaspedTerm
This grammar rule combines simple expressions like Literal as well as embraced Term expressions surrounded by parentheses. Furthermore the rule defines the unary plus and minus operator expression.
OperatorExpression ::= Term "+" Term
| Term "-" Term
| Term "*" Term
| Term "/" Term
| Term "%" Term
| Term "^" Term
| Term "!=" Term
| Term "=" Term
| Term "<" Term
| Term ">" Term
| Term "<=" Term
| Term ">=" Term
| Term "or" Term
| Term "xor" Term
| Term "and" Term
| Term "=>" Term
| Term "implies" Term
| "not" Term
The operator expression grammar rule defines all possible binary operator expressions ranging from arithmetic, comparing, and to logical ones.
0.1.0.
CallExpression ::= DirectCallExpression
| MethodCallExpression
| IndirectCallExpression
A call expression enables to invoke function and derived value
retrievals.
DirectCallExpression ::= IdentifierPath
| IdentifierPath "(" ")"
| IdentifierPath "(" Terms ")"
In a direct call expressions an IdentifierPath can be called with zero,
one, or multiple parameter Terms supprounded by parentheses.
0.1.0.
MethodCallExpression ::= SimpleOrClaspedTerm "." Identifier
| SimpleOrClaspedTerm "." Identifier "(" ")"
| SimpleOrClaspedTerm "." Identifier "(" Terms ")"
The method call expression invokes a method which is known
to the SimpleOrClaspedTerm type with zero, one, or
multiple parameter Terms surrounded by parentheses.
0.1.0.
LiteralCallExpression ::= SimpleOrClaspedTerm "." IntegerLiteral
A literal call expression can access of a certain index
identified by its IntegerLiteral of the
given SimpleOrClaspedTerm type.
0.1.0.
IndirectCallExpression ::= CallExpression "(" ")"
| CallExpression "(" Terms ")"
An indirect call expression can invoke function or derived return
value retrieval over an reference value.
0.1.0.
TypeCastingExpression ::= SimpleOrClaspedTerm "as" Type
The type casting expression enables to specify type conversions
of an SimpleOrClaspedTerm to (as) a given Type.
0.1.0.
LetExpression ::= "let" VariableBindings "in" Term
A let expression defines a new scope where the
defined VariableBindings are used for the
evaluation in the sub-expression Term.
0.1.0.
ConditionalExpression ::= "if" Term "then" Term "else" Term
The conditional rule provides a branching facility to evaluate
a certain sub-expression Term if the guarding Term is true.
Furthermore an else Term is specified to be evaluated if
the condition is not fulfilled. The resulting types of both
paths shall be of the same type.
0.1.0.
ChooseExpression ::= "choose" AttributedVariables "in" Term "do" Term
A choose expression allows to specify a selection
of AttributedVariables to be chosen in a given Term
one value per variable to evaluate a given Term.
0.1.0.
UniversalQuantifierExpression ::= "forall" AttributedVariables "in" Term "holds" Term
The universal quantifier expression checks forall AttriubtedVariables which
range in a given domain Term that a Term is satisfied (holds).
0.1.0.
ExistentialQuantifierExpression ::= "exists" AttributedVariables "in" Term "with" Term
The existential quantifier expression checks that there exists
for given AttributedVariables which range in a given
domain Term that a certain condition Term is satisfied (with).
0.1.0.
CardinalityExpression ::= "|" SimpleOrClaspedTerm "|"
The cardinality expression enables to retrieve the number of elements of a given set.
0.2.0.
Literal ::= UndefinedLiteral
| BooleanLiteral
| IntegerLiteral
| RationalLiteral
| DecimalLiteral
| BinaryLiteral
| StringLiteral
| ReferenceLiteral
| ListLiteral
| RangeLiteral
| TupleLiteral
| RecordLiteral
The literal grammar rule defines all possible literals in the CASM specification language.
UndefinedLiteral ::= "undef"
The undef (undefined) literal is used for all possible types to represent an undefined value.
BooleanLiteral ::= "true"
| "false"
The Boolean literal represents all defined values of the Boolean type.
IntegerLiteral ::= "[0-9][0-9']*[0-9]*"
The Integer literal defines all possible defined values of the Integer type. This literal supports user-defined digit grouping though the apostrophe character.
RationalLiteral ::= "0[rR][0-9][0-9']*[0-9]*(/[0-9][0-9']*[0-9]*)?"
The rational literal defines all possible defined values of the Rational type to represent fraction values. This literal supports user-defined digit grouping though the apostrophe character for the nominator and denominator.
DecimalLiteral ::= "[0-9]+.[0-9]+([eE][+-]?[0-9]+)?"
The decimal literal defines all possible defined values of the Decimal type.
BinaryLiteral ::= "0[bB][01][01']*[01]*"
| "0[xX][0-9a-fA-F][0-9a-fA-F']*[0-9a-fA-F]*"
The binary literal defines all possible defined values of the Binary type. It can be defined in binary notation (prefixed 0b) or hexadecimal notation (prefixed 0x).
StringLiteral ::= '"'.*'"'
The string literal defines all possible defined values of the String type.
ReferenceLiteral ::= "@" IdentifierPath
The reference literal defines a defined reference value of a given symbol identified by IdentifierPath. The at (@) character denotes that a reference literal shall be constructed of the given symbol name.
ListLiteral ::= "[" "]"
| "[" Terms "]"
The list literal defines a new defined list value.
It can construct an empty list or a list with predefined Terms.
The list element type is inferred from the provided Terms.
In case of an empty list, the usage of the empty list has to provide a type context to infer the correct inner list element type.
RangeLiteral ::= "[" Term ".." Term "]"
The range literal is used to construct value ranges of a certain type domain. The range type is inferred from the given start and end Term.
TupleLiteral ::= "(" Terms "," Term ")"
The tuple literal is used to construct tuple values of two or more Term elements.
RecordLiteral ::= "(" Assignments ")"
The record literal is used to construct record values and the inner record elements are addressed by their name through Assignments.
Assignments ::= Assignments "," Assignment
| Assignment
Consists of one or more Assignment grammar rules.
Assignment ::= Identifier ":" Term
An assignment binds a Term to a given symbol name identified by its Identifier.
Types ::= Types "," Type
| Type
Consists of one or more Type grammar rules separated by a comma character.
Type ::= BasicType
| TupleType
| RecordType
| TemplateType
| RelationType
| FixedSizedType
The Type grammar rule defines all possible CASM type constructs.
BasicType ::= IdentifierPath
A basic type symbol name is defined and identified by its IdentifierPath.
TupleType ::= "(" Types "," Type ")"
A tuple type can be defined by two or more inner Type separated by a comma character and surrounded with parentheses.
RecordType ::= "(" TypedVariables "," TypedVariable ")"
A record type can be defined by two or more inner TypedVariable separated by a comma character and surrounded with parentheses.
TemplateType ::= IdentifierPath "<" Types ">"
A template type can be defined by one or more inner template Types surrounded by angle brackets and identified by its IdentifierPath.
RelationType ::= IdentifierPath "<" MaybeFunctionParameters "->" Type ">"
A relation type is defined through a symbol name identified by its IdentifierPath, some optional n-ary MaybeFunctionParameters, and a return (result) Type domain separated by an arrow (→) token and surrounded by angle brackets.
FixedSizedType ::= IdentifierPath "'" Term
This grammar rule allows to restrict certain types which is specified by the given Term e.g. to a pre-defined size, length, or range.
FunctionParameters ::= FunctionParameters "*" Type
| Type
Function parameters are constructed through one or more Type separated by an asterix (*) character.
MaybeFunctionParameters ::= FunctionParameters
| null
Consists optionally of some FunctionParameters.
Parameters ::= Parameters "," TypedAttributedVariable
| TypedAttributedVariable
Parameters are constructed through one or more TypedAttributedVariable separated by a comma character.
MaybeDefined ::= "defined" "{" Term "}"
| null
This grammar rule is used in FunctionDefinition to optionally set a defined value of the resulting type domain of a function to a given Term.
MaybeInitially ::= "=" "{" Initializers "}"
| null
This grammar rule is used in FunctionDefinition to optionally set a initially value given as Initializers.
Initializers ::= Initializers "," Initializer
| Initializer
Initializers are constructed through one or more Initializer which are separated by an comma character.
Initializer ::= Term
| "(" Term ")" "->" Term
| TupleLiteral "->" Term
An initializer is used to define function value initialization over a n-ary function location.
Identifier ::= "([a-ZA-Z_]|UTF8){([a-zA-Z_0-9]|UTF8)}*"
| "in"
Represents a symbol (function, derived etc.) in a CASM specification.
IdentifierPath ::= IdentifierPath "::" Identifier
| Identifier
An identifier path is constructed through one or more Idenitifer which are separated by an double colon (::) token.
Variable ::= TypedVariable
| Identifier
A variable can either be a in typed or non-typed form. If just an Identifier is provided as variable name, a compiler analyze pass will infer the correct type of the variable.
AttributedVariables ::= AttributedVariables "," AttributedVariable
| AttributedVariable
Certain expression statements like ForallExpression or ChooseExpression require one or multiple attributed variables which shall be separated by a comma character.
TypedVariables ::= TypedVariables "," TypedVariable
| TypedVariable
Multiple typed variables are separated by a comma character.
TypedVariable ::= Identifier ":" Type
A typed variable consists of an Identifier and an associated Type which are separated by a colon character.
AttributedVariable ::= Attributes Variable
| Variable
An attributed variable are variables which can have optionally Attributes associated to them.
TypedAttributedVariable ::= Attributes TypedVariable
| TypedVariable
A typed attributed variable are typed variables which can have optionally Attributes associated to them.
VariableBindings ::= VariableBindings "," VariableBinding
| VariableBinding
The let rule and expression can have one or multiple variable bindings. Those are separated by a comma character.
VariableBinding ::= AttributedVariable "=" Term
A variable binding assigns (binds) an AttributedVariable to a given Term.
LocalFunctionDefinitions ::= LocalFunctionDefinitions "," AttributedLocalFunctionDefinition
| AttributedLocalFunctionDefinition
LocalFunctionDefinitions consist of one or more attributed LocalFunctionDefintions.
AttributedLocalFunctionDefinition ::= Attributes LocalFunctionDefinition
| LocalFunctionDefinition
An attributed local function definition which can have optionally Attributes.
LocalFunctionDefinition ::= Identifier ":" MaybeFunctionParameters "->" Type MaybeDefined MaybeInitially
The same as a traditional FunctionDefinition without a function keyword.
0.5.0.
Attributes ::= Attributes Attribute
| Attribute
Certain elements like definitions or variables in a CASM specification can have none, one, or multiple attributes associated to them.
Attribute ::= "[" BasicAttribute "]"
| "[" ExpressionAttribute "]"
An attribute can have two manifestations - a basic-based or a expression-based attribute. Every attribute has to be surrounded by a square brackets.
BasicAttribute ::= Identifier
A basic attributed is just represented by a simple Identifier.
The possible names for basic attributes are checked in an compiler analyze pass.
static attribute for a function definition:
[ static ] function C_of_CASM : -> String initially { "Corinthian" }
ExpressionAttribute ::= Identifier Term
In contrast to a BasicAttribute the expression attribute allows to define a full expression Term which is identified by its Identifier.