D. Complete SpecL Syntax
start:
top_level_items
|
top_level_items top_level_item
top_level_item:
declaration
|
top_level_expression
declaration:
module
|
object ';'
|
operation ';'
|
value ';'
|
variable ';'
|
axiom ';'
|
theorem ';'
|
attribute ';'
|
rule ';'
|
include ';'
module:
module_heading declarations END optional_name ';'
|
module_heading END optional_name ';'
module_heading:
MODULE name optional_semicolon
|
MODULE name optional_semicolon imports
|
MODULE name optional_semicolon exports
|
MODULE name optional_semicolon imports exports
imports:
import
|
import imports
import:
IMPORT import_items ';'
|
IMPORT qualified_name '.' '*' ';'
|
IMPORT qualified_name '.' '*' EXCEPT names ';'
import_items:
import_item
|
export exports
export:
EXPORT names ';'
|
EXPORT '*' ';'
|
EXPORT '*' EXCEPT names ';'
declarations:
declaration
|
declarations declaration
object:
simple_object_declaration
|
simple_object_declaration END optional_name
|
simple_object_declaration object_attributes END optional_name
simple_object_declaration:
object_heading
|
object_heading '=' components_expression
|
object_heading IS components_expression
|
object_heading extends_symbol qualified_names
|
object_heading extends_symbol qualified_names '=' components_expression
|
object_heading '=' components_expression extends_symbol qualified_names
object_heading:
object_symbol name
|
object_symbol name '(' object_parameters ')'
object_symbol:
OBJECT
|
OBJ
object_parameters:
object_parameter
|
object_parameters ',' object_parameter
object_parameter:
name
|
question_mark_name
object_attributes:
object_attribute
|
object_attributes object_attribute
object_attribute:
components ';'
|
parents
|
where
|
operations
|
equations
|
user_defined_attribute
components:
components_symbol ':' components_expression
parents:
PARENTS ':' qualified_names ';'
components_symbol:
COMPONENTS
|
PARTS
extends_symbol:
EXTENDS
|
'<'
components_expression:
|
components_expression component_and_op components_expression
|
components_expression component_or_op components_expression
|
components_expression component_list_op
|
component_operation_heading operation_signature
|
components_base_element
components_base_element:
component_type_designator
|
component_type_designator '=' expression
|
literal
|
'(' components_expression ')'
|
name ':' component_type_designator
|
name ':' component_type_designator '=' expression
|
name ':' literal
|
name ':' '(' components_expression ')'
|
component_and_op:
AND
|
','
component_or_op:
OR
|
'|'
component_list_op:
'*'
component_operation_heading:
operation_symbol
where:
WHERE ':' where_list ';'
where_list:
|
where_item
|
where_list semicolon_or_comma where_item
where_item:
where_eq
where_eq:
name '=' name
operations:
operations_symbol ':' operation_names_optional_signatures ';'
operations_symbol:
OPERATIONS
|
OPS
operation_names_optional_signatures:
|
operation_name_optional_signature
|
operation_names_optional_signatures semicolon_or_comma
operation_name_optional_signature
operation_name_optional_signature:
name
|
operation_name operation_signature
operation_name:
name
equations:
equations_symbol ':' equation_sequence ';'
|
equations_symbol ':' simple_variables ';' equation_sequence ';'
equations_symbol:
EQUATIONS
simple_variables:
simple_variable
|
simple_variables ';' simple_variable
simple_variable:
variable_symbol names ':' type_designator
|
variable_symbol names ':' type_designator '=' expression
variable_symbol:
VARIABLE
|
VAR
equation_sequence:
|
equation
|
equation_sequence ';' equation
equation:
invocation EQEQ expression
user_defined_attribute:
attribute_name attribute_colon ';'
|
attribute_name attribute_colon ATTRIBUTE_TEXT ';'
|
attribute_name ':' qualified_names ';'
|
attribute_name ':' expression ';'
attribute_colon:
':'
operation:
simple_operation_declaration
|
simple_operation_declaration END optional_name
|
simple_operation_declaration operation_attributes END optional_name
simple_operation_declaration:
operation_symbol operation_heading
|
operation_symbol operation_heading '=' expression
operation_symbol:
OPERATION
|
OP
|
FUNCTION
|
FUNC
operation_heading:
operation_name
|
operation_name operation_signature
operation_signature:
'(' operation_parameters ')'
|
'(' operation_parameters ')' ARROW operation_output
|
'(' operation_parameters ')' ARROW
'(' operation_outputs ')'
operation_parameters:
|
operation_parameter
|
operation_parameters component_and_op operation_parameters
operation_outputs:
|
operation_output
|
operation_outputs component_and_op operation_outputs
operation_parameter:
variable_type_designator
|
variable_type_designator '=' expression
|
name ':' variable_type_designator
|
name ':' variable_type_designator '=' expression
operation_output:
variable_type_designator
|
name ':' variable_type_designator
operation_attributes:
operation_attribute
|
operation_attributes operation_attribute
operation_attribute:
components ';'
|
inputs_symbol ':' operation_parameters ';'
|
outputs_symbol ':' operation_parameters ';'
|
precondition_symbol ':' condition ';'
|
postcondition_symbol ':' condition ';'
|
DATAFLOW ':' connections ';'
|
BODY ':' expression ';'
|
user_defined_attribute
inputs_symbol:
INPUTS
|
IN
outputs_symbol:
OUTPUTS
|
OUT
precondition_symbol:
PRECONDITION
|
PRE
postcondition_symbol:
POSTCONDITION
|
POST
condition:
|
expression
connections:
connection
|
connections ',' connection
connection:
connection_expression ARROW connection_expression
connection_expression:
expression
|
'?'
value:
value_symbol name '=' expression optional_attributes
|
value_symbol name ':' type_designator '=' expression optional_attributes
value_symbol:
VALUE
|
VAL
variable:
variable_symbol names ':' type_designator optional_attributes
|
variable_symbol names ':' type_designator '=' expression
optional_attributes
|
variable_symbol names '=' expression optional_attributes
axiom:
axiom_symbol axiom_name '=' expression optional_attributes
axiom_name:
name
axiom_symbol:
AXIOM
|
AX
theorem:
theorem_symbol theorem_name '=' expression optional_attributes
theorem_name:
name
theorem_symbol:
THEOREM
|
THM
attribute:
untyped_attribute
|
untyped_attribute ':' components_expression
untyped_attribute:
DEFINE OBJECT ATTRIBUTE names
|
DEFINE OPERATION ATTRIBUTE names
|
DEFINE ATTRIBUTE names
rule:
rule_heading '=' rule_rhs optional_attributes
|
rule_heading '=' optional_attributes
|
rule_heading
rule_heading:
RULE name
rule_rhs:
rule_alternative
|
rule_alternative '{' actions '}'
rule_alternative:
|
rule_element
|
rule_rhs '|' rule_rhs
rule_element:
rule_terminal
|
rule_terminal component_list_op
|
rule_element rule_element
rule_terminal:
name
|
name ':' name
|
STRING_LITERAL
|
name ':' STRING_LITERAL
actions:
action
|
actions ';' action
action:
|
action_lhs '=' action_rhs
action_lhs:
name ATTRIBUTE_SELECT attribute_name
|
name '.' attribute_name
|
name
action_rhs:
expression
optional_attributes:
|
END optional_name
|
user_defined_attributes END optional_name
user_defined_attributes:
user_defined_attribute
|
user_defined_attributes user_defined_attribute
include:
INCLUDE STRING_LITERAL
top_level_expression:
expression ';'
|
'>' expression ';'
expression:
boolean_expression
|
arithmetic_expression
|
callable_expression
boolean_expression:
expression AND expression
|
expression OR expression
|
NOT expression
|
expression XOR expression
|
expression IMPLIES expression
|
expression IFF expression
|
IF expression THEN expression
|
IF expression THEN expression ELSE expression
|
relational_expression
|
quantifier_expression
relational_expression:
expression relational_op expression
|
name almost_eq_op expression EXCEPT except_item
|
name almost_eq_op expression EXCEPT '(' except_items ')'
quantifier_expression:
forall_symbol '(' names ':' type_name ')' expression
|
forall_symbol '(' names IN expression ')' expression
|
forall_symbol '(' names ':' type_name '|' expression ')'
expression
|
exists_symbol '(' names ':' type_name ')' expression
|
exists_symbol '(' names IN expression ')' expression
|
exists_symbol '(' names ':' type_name '|' expression ')'
expression
forall_symbol:
FORALL
exists_symbol:
EXISTS
arithmetic_expression:
expression add_op expression
|
expression mult_op expression
|
expression exp_op expression
|
arithmetic_prefix_op expression
|
length_op expression
relational_op:
'='
|
'<'
|
'>'
|
NEQ
|
LEQ
|
GEQ
|
IN
almost_eq_op:
AEQ
except_items:
except_item
|
except_items ',' except_item
|
except_items AND except_item
except_item:
name '.' name '=' expression
|
name '.' INTEGER_LITERAL '=' expression
add_op:
'+'
|
'-'
mult_op:
'*'
|
'/'
|
DIV
|
MOD
exp_op:
'^'
length_op:
'#'
arithmetic_prefix_op:
'+'
|
'-'
callable_expression:
constructor_expression
|
selector_expression
|
index_expression
|
let
|
set
|
invocation
|
validation_invocation
|
lambda
|
name
|
literal
|
'(' expression_sequence ')'
constructor_expression:
'[' expression DOTDOT expression ']'
|
'[' expression_list ']'
|
'{' expression_list_with_empties '}'
selector_expression:
callable_expression select_op name
|
callable_expression '.' INTEGER_LITERAL
|
callable_expression ATTRIBUTE_SELECT attribute_name
select_op:
'.'
|
CHECK_UNION
|
GET_INSTANCE
|
CHECK_INSTANCE
index_expression:
callable_expression '[' expression ']'
|
callable_expression '[' expression DOTDOT expression ']'
let:
LET names '=' expression
|
LET names ':' type_designator '=' expression
set:
SET storage_designator '=' expression
storage_designator:
name
|
selector_expression
|
index_expression
|
dereference_expression
dereference_expression:
'@' callable_expression
invocation:
callable_expression '(' actual_parameters ')'
validation_invocation:
callable_expression '(' actual_parameters ')' QARROW actual_parameter
|
callable_expression '(' actual_parameters ')' QARROW
'(' actual_parameters ')'
actual_parameters:
|
actual_parameter
|
actual_parameters ',' actual_parameter
actual_parameter:
expression
|
'?'
lambda:
LAMBDA operation_signature expression
expression_list:
|
expression_list_element
|
expression_list ',' expression_list_element
expression_list_element:
expression
expression_list_with_empties:
expression_possibly_empty
|
expression_list_with_empties ',' expression_possibly_empty
expression_possibly_empty:
|
expression
expression_sequence:
expression_sequence_element
|
expression_sequence ';' expression_sequence_element
expression_sequence_element:
|
expression
|
simple_variable
qualified_names:
qualified_name
|
qualified_names ',' qualified_name
qualified_name:
name
|
qualified_name '.' name
names:
name
|
names ',' name
name:
IDENTIFIER
attribute_name:
ATTRIBUTE_IDENTIFIER
optional_name:
|
name
component_type_designator:
type_name_or_variable
|
type_name_or_variable '(' type_names ')'
variable_type_designator:
type_name_or_variable
|
type_name_or_variable component_list_op
|
type_name_or_variable '(' type_names_or_variables ')'
|
type_name_or_variable '(' type_names_or_variables ')' component_list_op
type_designator:
type_name
|
type_name component_list_op
|
type_name '(' type_names ')'
|
type_name '(' type_names ')' component_list_op
type_names:
type_name
|
type_names ',' type_name
type_name:
qualified_name
type_name_or_variable:
qualified_name
|
question_mark_name
type_names_or_variables:
type_name_or_variable
|
type_names_or_variables ',' type_name_or_variable
question_mark_name:
QUESTION_MARK_IDENTIFIER
literal:
STRING_LITERAL
|
INTEGER_LITERAL
|
REAL_LITERAL
|
NIL_LITERAL
semicolon_or_comma:
';'
|
','
optional_semicolon:
|
';'