Syntax

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:

The first variant is used in an single execution agent environment to set for an agent the starting top-level rule to the given rule specified through the IdentifierPath.

The second variant is used in a multiple execution agent environment to set for one or multiple agents the starting top-level rule over a agent relation type specified through Initializers which are surrounded by curly brackets.

This definition is introduced in version 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.

This definition is introduced in version 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.

This definition is introduced in version 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.

This definition is introduced in version 0.1.0.

Every rule without a specified return type equals to a return type 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

The return 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.

This definition is introduced in version 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

The attribute symbolic is introduced in version 0.6.0.

EnumeratorDefinition ::= Identifier
                       | Attributes Identifier

An enumerator definition are Identifier with optionally Attributes assigned to them.

This definition is introduced in version 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.

The following example defines a type alias for Integer named MyType:

using MyType = Integer

This definition is introduced in version 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.

This definition is introduced in version 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.

This definition is introduced in version 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.

This definition is introduced in version 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.

This rule is introduced in version 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.

This rule is introduced in version 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.

This rule is introduced in version 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.

This rule is introduced in version 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.

This definition is introduced in version 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.

This rule is introduced in version 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.

This rule is introduced in version 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.

This rule is introduced in version 0.1.0.

BlockRule ::= "{" Rules "}"
            | "par" Rules "endpar"

The block rule specifies that given Rules shall be evaluated with a parallel execution semantics.

This rule is introduced in version 0.1.0.

SequenceRule ::= "{|" Rules "|}"
               | "seq" Rules "endseq"

The sequence rule specifies that given Rules shall be evaluated with a sequential execution semantics.

This rule is introduced in version 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.

This rule is introduced in version 0.1.0.

CallRule ::= CallExpression

A call rule allows to invoke other named rules (RuleDefinition).

This rule is introduced in version 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.

The following snipped defines the semantics of the while rule as:

iterate
    if not <Term> then
	skip
    else
	<Rule>

This rule is introduced in version 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.

This expression is introduced in version 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.

This expression is introduced in version 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.

This expression is introduced in version 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.

This expression is introduced in version 0.1.0.

IndirectCallExpression ::= CallExpression "(" ")"
                         | CallExpression "(" Terms ")"

An indirect call expression can invoke function or derived return value retrieval over an reference value.

This expression is introduced in version 0.1.0.

TypeCastingExpression ::= SimpleOrClaspedTerm "as" Type

The type casting expression enables to specify type conversions of an SimpleOrClaspedTerm to (as) a given Type.

This expression is introduced in version 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.

This expression is introduced in version 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.

This expression is introduced in version 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.

This expression is introduced in version 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).

This expression is introduced in version 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).

This expression is introduced in version 0.1.0.

CardinalityExpression ::= "|" SimpleOrClaspedTerm "|"

The cardinality expression enables to retrieve the number of elements of a given set.

This expression is introduced in version 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.

This definition is introduced in version 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.

The following example shows its usage by setting the 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.