APPENDIX A

Syntax Summary

Specifications

specification ::=

module_decl-string

module_decl ::=

scheme_decl |object_decl

Declarations

decl ::=

scheme_decl |object_decl |

type_decl |value_decl |

variable_decl |channel_decl |

axiom_decl

Scheme Declarations

scheme_decl ::=

scheme scheme_def-list

scheme_def ::=

opt-comment-string

id opt-formal_scheme_parameter = class_expr

formal_scheme_parameter ::=

( formal_scheme_argument-list )

formal_scheme_argument ::=

object_def

Object Declarations

object_decl ::=

object object_def-list

object_def ::=

opt-comment-string

id opt-formal_array_parameter : class_expr

formal_array_parameter ::=

[ typing-list ]

Type Declarations

type_decl ::=

type type_def-list

type_def ::=

sort_def |

variant_def |

union_def |

short_record_def |

abbreviation_def

Sort Definitions

sort_def ::=

opt-comment-string id

Variant Definitions

variant_def ::=

opt-comment-string id == variant-choice

variant ::=

constructor |

record_variant

record_variant ::=

constructor ( component_kind-list )

component_kind ::=

opt-destructor type_expr opt-reconstructor

constructor ::=

id_or_op |



destructor ::=

id_or_op :

reconstructor ::=

 id_or_op

Union Definitions

union_def ::=

opt-comment-string

id = name_or_wildcard-cholce2

name_or_wildcard ::=

type-name |



Short Record Definitions

short_record _def ::=

opt-comment-string

id :: component_kind-string

Abbreviation Definitions

abbreviation_def ::=

opt-comment-string id = type_expr

Value Declarations

value_decl ::=

value value_def-list

value_def ::=

commented_typing |

explicit_value_def |

implicit_value_def |

explicit_function_def |

implicit_function_def

Explicit Value Definitions

explicit_value_def ::=

opt-comment-string

single_typing = pure-value_expr

Implicit Value Definitions

implicit_value_def ::=

opt-comment-string

single_typing pure-restriction

Explicit Function Definitions

explicit_function_def ::=

opt-comment-string single_typing

formal_function_application  value_expr

opt-pre_condition

formal_function_application ::=

id_application |

prefix_application |

infix_application

id_application ::=

value-id formal_function_parameter-string

formal_function_parameter ::=

( opt-binding-list )

prefix_application ::=

prefix_op id

infix_application ::=

id infix_op id

Implicit Function Definitions

implicit_function_def ::=

opt-comment-string

single_typing formal_function_application

post_condition opt-pre_condition

Variable Declarations

variable_decl ::=

variable variable_def-list

variable_def ::=

single_variable_def |

multiple_variable_def

single_variable_def ::=

opt-comment-string

id : type_expr opt-initialisation

initialisation ::=

:= pure-value_expr

multiple_variable_def ::=

opt-comment-string id-list2 : type_expr

Channel Declarations

channel_decl ::=

channel channel_def-list

channel_def ::=

single_channel_def |

multiple_channel_def

single_channel_def ::=

opt-comment-string id : type_expr

multiple_channel_def ::=

opt-comment-string id-list2 : type_expr

Axiom Declarations

axiom_decl ::=

axiom opt-axiom_quantification

axiom_def-list

axiom_quantification ::=

forall typing-list 

axiom_def ::=

opt-comment-string opt-axiom_naming

readonly_logical-value_expr

axiom_naming ::=

[ id ]

Class Expressions

class_expr ::=

basic_class_expr |

extending_class_expr |

hiding_class_expr |

renayming_class_expr |

scheme_instantiation

Basic Class Expressions

basic_class_expr ::=

class opt-decl-string end

Extending Class Expressions

extending_class_expr ::=

extend class_expr with class_expr

Hiding Class Expressions

hiding_class_expr ::=

hide defined_item-list in class_expr

Renaming Class Expressions

renaming_class_expr ::=

use rename_pair-list in class_expr

Scheme Instantiations

scheme_instantiation ::=

scheme-name opt-actual_scheme_parameter

actual_scheme_parameter ::=

( object_expr-list )

Rename Pairs

rename_pair ::=

defined_item for defined_item

Defined Items

defined_item ::=

id_or_op |

disambiguated_item

disambiguated_item ::=

id_or_op : type_expr

Object Expressions

object_expr ::=

object-name |

element_object_expr |

array_object_expr |

fitting_object_expr

Element Object Expressions

element_object_expr ::=

array-object_expr actual_array_parameter

actual_array_parameter :: =

[ pure-value_expr-list ]

Array Object Expressions

array_object_expr ::=

[| typing-list  element-object_expr |]

Fitting Object Expressions

fitting_object_expr ::=

object_expr { rename_pair-list }

Type Expressions

type_expr ::=

type_literal |

type-name |

product_type_expr |

set_type_expr |

list_type_expr |

map_type_expr |

function_type_expr |

subtype_expr |

bracketed_type_expr

Type Literals

type_literal ::=

Unit |Bool |lnt |Nat |Real |Text |

Char

Product Type Expressions

product_type_expr ::=

type_expr-product2

Set Type Expressions

set_type_expr ::=

finite_set_type_expr |

infinite_set_type_expr

finite_set_type_expr ::=

type_expr-set

infinite_set_type_expr :: =

type_expr-infset

List Type Expressions

list_type_expr ::=

finite_list_type_expr |

infinite_list_type_expr

finite_list_type_expr ::=

type_expr*

infinite_list_type_expr ::=

type_expr*

Map Type Expressions

map_type_expr ::=

type_expr * type_expr

Function Type Expressions

function_type_expr ::=

type_expr function_arrow result_desc

function_arrow ::=

 | |

result_desc ::=

opt-access_desc-string type_expr

Subtype Expressions

subtype_expr ::=

{| single_typing pure-restriction |}

Bracketed Type Expressions

bracketed_type_expr ::=

( type_expr )

Access Descriptions

access_desc ::=

access_mode access-list

access_mode ::=

read |write |in |out

access ::=

variable_or_channel-name |

enumerated_access |

completed_access |

comprehended_access

enumerated_access ::=

{ opt-access-list }

completed_access ::=

opt-qualification any

comprehended_access ::=

{ access | pure-set_limitation }

Value Expressions

value_expr ::=

value_literal |

value_or_variable-name |

pre_name |

basic_expr |

product_expr |

set_expr |

list_expr |

map_expr |

function _expr |

application_expr |

quantified_expr |

equivalence_expr |

post_expr |

disambiguation_expr |

bracketed_expr |

infix_expr |

prefix_expr |

comprehended_expr |

initialise_expr |

assign ment_expr |

input_expr |

output_expr |

structured_expr

Value Literals

value_literal ::=

unit_literal |

bool_literal |

int_literal |

real_literal |

text_literal |

char_literal

unit_literal ::=

( )

bool_literal ::=

true |false

Pre Names

pre_name ::=

variable-name

Basic Expressions

basic_expr ::=

chaos |skip |stop |swap

Product Expressions

product_expr ::=

( value_expr-list2 )

Set Expressions

set_expr ::=

ranged_set_expr |

enumerated_set_expr |

comprehended_set_expr

Ranged Set Expressions

ranged_set_expr ::=

{ readonly_integer-value_expr ..

readonly_integer-value_expr }

Enumerated Set Expressions

enumerated_set_expr ::=

{ readonly-opt-value_expr-list }

Comprehended Set Expressions

comprehended_set_expr ::=

{ readonly-value_expr | set_limitation }

set_limitation ::=

typing-list opt-restriction

restriction ::=

 readonly_logical-value_expr

List Expressions

list_expr ::=

ranged_list_expr |

enumerated_list_expr |

comprehended_list_expr

Ranged List Expressions

ranged_list_expr ::=

 integer-value_expr .. integer-value_expr 

Enumerated List Expressions

enumerated_list_expr ::=

 opt-value_expr-list 

Comprehended List Expressions

comprehended_list_expr ::=

 value_expr | list_limitation 

list_limitation ::=

binding in readonly_list-value_expr

opt-restriction

Map Expressions

map_expr ::=

enumerated_map_expr |

comprehended_map_expr

Enumerated Map Expressions

enumerated_map_expr ::=

[ opt-value_expr_pair-list ]

value_expr_pair ::=

readonly-value_expr  readonly-value_expr

Comprehended Map Expressions

comprehended_map_expr ::=

[ value_expr_pair | set_limitation ]

Function Expressions

function_expr ::=

 lambda_parameter  value_expr

lambda_parameter ::=

lambda_typing |

single_typing

lambda_typing ::=

( opt-typing-list )

Application Expressions

application_expr ::=

list_or_map_or_function-value_expr actual_function_parameter-string

actual_function_parameter ( opt-value_expr-list )

Quantified Expressions

quantified_expr ::=

quantifier typing-list restriction

quantifier ::=

 | |

Equivalence Expressions

equivalence_expr ::=

value_expr  value_expr opt-pre_condition

pre_condition ::=

pre readonly_logical-value_expr

Post Expressions

post_expr ::=

value_expr post_condition opt-pre_condition

post_condition ::=

opt-result_naming post readonly_logical-value_expr

result_naming ::=

as binding

Disambiguation Expressions

disambiguation_expr ::=

value_expr : type_expr

Bracketed Expressions

bracketed_expr ::=

( value_expr )

Infix Expressions

infix_expr ::=

stmt_infix_expr |

axiom_infix_expr |

value_infix_expr

Statement Infix Expressions

stmt_infix_expr ::=

value_expr infix_combinator value_expr

Axiom Infix Expressions

axiom_infix_expr ::=

logical-value-expr infix-connective

logical-value_expr

Value Infix Expressions

value_infix_expr ::=

value_expr infix_op value_expr

Prefix Expressions

prefix_expr ::=

axiom_prefix_expr |

universal_prefix_expr |

value_prefix_expr

Axiom Prefix Expressions

axiom_prefix_expr ::=

prefix_connective logical-value_expr

Universal Prefix Expressions

universal_prefix_expr ::=

 readonly_logical-value_expr

Value Prefix Expressions

value_prefix_expr ::=

prefix_op value_expr

Comprehended Expressions

comprehended_expr ::=

associative_commutative-infix_combinator

{ value_expr | set_limitation }

Initialise Expressions

initialise_expr ::=

opt-qualification initialise

Assignment Expressions

assignment_expr ::=

variable-name := value_expr

Input Expressions

input_expr ::=

channel-name ?

Output Expressions

output_expr ::=

channel-name ! value_expr

Structured Expressions

structured_expr ::=

local_expr |let_expr |

if_expr |case_expr |

while_expr |until_expr |