CMLGrammar

Note: the only parametrisation qualifier allowed in a process declaration is val. (Omitting a parametrisation qualifier defaults to val, and is permitted as well.)

parametrisation →

[ parametrisation qualifier ], identifier, { ,, identifier }, :, type

;

parametrisation qualifier →

val | res | vres

;

action declarations →

actions, { action definition }

;

action definition →

identifier, =, [ parametrisation, { ,, parametrisation }, @ ], action

;

chanset expression →

identifier

| {, [ identifier, { ,, identifier } ], }

| {|, [ identifier, { ,, identifier } ], |}

| {|, identifier, { ., expression }, | bind list, [ @, expression ], |}

| chanset expression, union, chanset expression

| chanset expression, inter, chanset expression

| chanset expression, \, chanset expression

;

nameset expression →

chanset expression

;

Classes

class declaration →

class, identifier, [ extends, identifier ], =, begin, { class paragraph }, end

;

class paragraph →

type declarations

| value declarations

| function declarations

| operation declarations

| state declarations

| initial, operation definition

;

Processes

process →

action process

| process, ;, process

| process, [], process

| process, |~|, process

| process, [|, chanset expression, |], process

| process, [, chanset expression, ||, chanset expression, ], process

| process, |||, process

| process, /_\, process

| process, /_, expression, _\, process

| process, [_>, process

| process, [_, expression, _>, process

| process, \\, chanset expression

| process, startsby, expression

| process, endsby, expression

| (, parametrisation, { ,, parametrisation }, @, process, ), (, expression, { ,, expression }, )

| identifier, [ (, [ expression, { ,, expression } ], ) ]

| process, renaming expression

| replicated process

| (, process, )

;

action process →

begin, { action paragraph }, @, action, end

;

replicated process →

;, replication declarations, @, process

| [], replication declarations, @, process

| |~|, replication declarations, @, process

| |||, replication declarations, @, process

| [|, chanset expression, |], replication declarations, @, process

| ||, replication declarations, @, [, [ chanset expression ], ], process

;

action paragraph →

type declarations

| value declarations

| function declarations

| operation declarations

| action declarations

| nameset declarations

| state declarations

;

renaming expression →

[[``, |renaming pair|_, { ``,``, |renaming pair|_ }, ``]]

| [[``, |renaming pair|_, ``|`` |bind list|_, [ ``@``, |expression|_ ], ``]]

;

Note that the current parser only supports a single expression after an identifier in a renaming pair; this will be corrected in a future release.

renaming pair →

identifier, { ., expression }, <-, identifier, { ., expression }

;

replication declarations →

replication declaration, { ,, replication declaration }

;

replication declaration →

identifier, { ,, identifier }, :, type

| identifier, { ,, identifier }, in set, expression

;

Actions

action →

identifier

| Skip

| Stop

| Diverge

| Wait expression

| communication, ->, action

| [, expression, ], &, action

| action, ;, action

| action, [], action

| action, |~|, action

| action, /_\, action

| action, /_, expression, _\, action

| action, [_>, action

| action, [_, expression, _>, action

| action, \\, chanset expression

| action, startsby, expression

| action, endsby, expression

| action, renaming expression

| mu, identifier, { , identifier }, @, (, action, { , action }, )

| parallel action

| parametrised action

| (, action, )

| instantiated action

| replicated action

| statement

;

communication →

identifier, { communication parameter }

;

communication parameter →

?, bindable pattern, [ :, (, expression, ) ]

| !, parameter

| ., parameter

;

parameter →

identifier

| ( expression )

| symbolic literal

| tuple expression

| record expression

;

parallel action →

action, |||, action

| action, [||, nameset expression, |, nameset expression, ||], action

| action, [, chanset expression, ||, chanset expression, ], action

| action, [, nameset expression, |, chanset expression, ||, chanset expression, |, nameset expression, ], action

| action, [|, chanset expression, |], action

;

parametrised action →

( parametrisation, { ,, parametrisation }, @, action, )

;

instantiated action →

parametrised action, (, expression, { ,, expression }, )

;

replicated action →

;, replication declarations, @, action

| [], replication declarations, @, action

| |~|, replication declarations, @, action

| |||, replication declarations, @, [, [ nameset expression ], ], action

| [|, chanset expression |], replication declarations, @, [ , [ nameset expression ], ], action

| ||, replication declarations, @, [, [ nameset expression ], |, [ chanset expression ], ], action

;

Statements

statement →

let, local definition, { ,, local definition }, in, action

| (, [ dcl, assignment definition, { ,, assignment definition }, @ ], action, )

| cases statement

| if statement

| if non-deterministic alt, { |, non-deterministic alt }, end

| do non-deterministic alt, { |, non-deterministic alt }, end

| while, expression, do, action

| for, bindable pattern, [ :, type ] in, expression, do, action

| for, all, bindable pattern, in set, expression, do, action

| for, identifier, =, expression, to, expression, [ by, expression ], do, action

| [, [ frame ], [ pre, expression ], post, expression, ]

| return, [ expression ]

| assign statement

| multiple assign statement

| call statement

| new statement

;

local definition →

value definition

| function definition

;

non-deterministic alt →

expression, ->, action

;

if statement →

if, expression, then, action, { elseif statement }, [ else, action ]

;

elseif statement →

elseif, expression, then, action

;

cases statement →

cases, expression, :, cases statement alt, { ,, cases statement alt }, [ ,, others statement ], end

;

cases statement alt →

pattern list, ->, action

;

others statement →

others, ->, action

;

assign statement →

assignable expression, :=, expression

;

multiple assign statement →

atomic, (, assign statement, ;, assign statement, { ;, assign statement }, )

;

call statement →

name, (, [ expression, { ,, expression } ], )

| assignable expression, :=, name, (, [ expression, { ,, expression } ], )

;

new statement →

assignable expression, :=, new, name, (, [ expression, { ,, expression } ], )

;

Types

type declarations →

types, [ type definition, { ;, type definition } ]

;

type definition →

[ qualifier ], identifier, =, type, [ type invariant ]

| [ qualifier ], identifier, ::, { field }, [ type invariant ] }

;

type →

(, type, )

| basic type

| quote literal

| compose, identifier, of, { field }, end

| type, |, type, { |, type }

| type, *, type, { *, type }

| [, type, ]

| set of, type

| seq of, type

| seq1 of, type

| map, type, to, type

| inmap, type, to, type

| function type

| name

;

basic type →

bool | nat | nat1 | int | rat | real | char | token

;

field →

type

| identifier, :, type

| identifier, :-, type

;

function type →

discretionary type, +>, type

| discretionary type, ->, type

;

discretionary type →

type | ()

;

type invariant →

inv, pattern, ==, expression

;

Operations

Operations do not include reactive constructs; while the parser will accept any action in an operation body, the typechecker will only allow statements, the ; sequential composition operator, and the constant action Skip. In essence, operation bodies in CML allow only what is allowed in VDM operation bodies.

operation declarations →

operations, { operation definition }

;

operation definition →

explicit operation definition

| implicit operation definition

;

explicit operation definition →

[ qualifier ], identifier, :, operation type, identifier, parameters, ==, operation body, [ pre, expression ], [ post, expression ]

;

operation type →

discretionary type, ==>, discretionary type

;

operation body →

action

| is subclass responsibility

| is not yet specified

;

implicit operation definition →

[ qualifier ], identifier, parameter types, [ identifier type pair list ], [ frame ], [ pre, expression ], post, expression

;

frame →

frame, var information, { var information }

;

var information →

rd, name, { ,, name }, [ :, type ]

| wr, name, { ,, name }, [ :, type ]

;

Functions

function declarations →

functions, { function definition }

;

function definition →

explicit function definition

| implicit function definition

;

explicit function definition →

[ qualifier ], identifier, :, function type, identifier, parameters list, ==, function body, [ pre, expression ], [ post, expression ], [ measure, name ]

;

parameters list →

parameters, { parameters }

;

parameters →

(, [ pattern list ], )

;

implicit function definition →

[ qualifier ], identifier, parameter types, identifier type pair list, [ pre, expression ], post, expression

;

parameter types →

(, [ pattern list, :, type, { ,, pattern list, :, type } ], ) }

;

identifier type pair list →

identifier, :, type, { ,, identifier, :, type }

;

function body →

expression

| is not yet specified

| is subclass responsibility

;

Expressions

expression →

self

| name

| old name

| symbolic literal

| (, expression, )

| unary operator, expression

| expression, binary operator, expression

| let, local definition, { ,, local definition }, in, expression

| forall, bind list, @, expression

| exists, bind list, @, expression

| exists1, bind, @, expression

| iota, bind, @, expression

| lambda, type bind list, @, expression

| is_, (, expression, ,, type, )

| is_, basic type, (, expression, )

| is_, name, (, expression, )

| pre_, (, expression, { ,, expression }, )

| isofclass, (, name, expression, )

| tuple expression

| record expression

| set expression

| sequence expression

| subsequence

| map expression

| if expression

| cases expression

| apply

| field select

| tuple select

;

name →

identifier, [ ., identifier ]

;

old name →

identifier, ~

;

unary operator →

+ | - | abs | floor | not | card | power | dunion | dinter | hd | tl | len | elems | inds | reverse | conc | dom | rng | merge | inverse

;

binary operator →

+ | - | * | / | div | rem | mod | < | <= | > | >= | = | <> | or | and | => | <=> | in set | not in set | subset | psubset | union | \ | inter | ^ | ++ | munion | <: | <-: | :> | :-> | comp | **

;

tuple expression →

mk_, (, expression, ,, expression, { ,, expression }, )

;

record expression →

mk_, token, (, expression, )

| mk_, name, (, [ expression, { ,, expression } ], )

;

set expression →

{, [ expression, { ,, expression } ], }

| {, expression, |, bind list, [ @, expression ], }

| {, expression, ,, ..., ,, expression, }

;

sequence expression →

[, [ expression, { ,, expression } ], ]

| [, expression, |, set bind, [ @, expression ], ]

;

subsequence →

expression, (, expression, ,, ..., ,, expression, )

;

map expression →

{, |->, }

| {, maplet, { ,, maplet }, }

| {, maplet, |, bind list, [ @, expression ], }

;

maplet →

expression, |->, expression

;

apply →

expression, (, [ expression, { ,, expression } ], )

;

field select →

expression, ., identifier

;

tuple select →

expression, .#, numeral

;

if expression →

if, expression, then, expression, { elseif expression }, else, expression

;

elseif expression →

elseif, expression, then, expression

;

cases expression →

cases, expression, :, cases expression alternatives, [ ,, others -> expression ], end

;

cases expression alternatives →

pattern list, ->, expression, { ,, pattern list, ->, expression }

;

assignable expression →

self { selector }

| identifier { selector }

;

selector →

(, [ expression, { ,, expression } ], )

| (, expression, ..., expression, )

| .#, numeral

| ., identifier

;

Patterns

pattern →

bindable pattern

| match value

;

bindable pattern →

-

| identifier

| mk_, (, pattern, ,, pattern list, )

| mk_, name, (, [ pattern list ], )

;

match value →

(, expression, )

| symbolic literal

;

pattern list →

pattern, { ,, pattern }

;

bind →

set bind

| type bind

;

set bind →

pattern, in set, expression

;

type bind →

pattern, :, type

;

bind list →

multiple bind, { ,, multiple bind }

;

multiple bind →

pattern list, in set, expression

| pattern list, :, type

;

type bind list →

type bind, { ,, type bind }

;

Lexical Specification

[ Please note: the parser's implementation of this is still incomplete. For now it's probably best to stick within the ASCII character set. ]

Unlike the rest of this specification, the rules in this section are sensitive to whitespace; as such, whitespace may not implicity separate any pair of components in a rule here.

Note that the unicode character categories can be found online at http://www.fileformat.info/info/unicode/category/index.htm. The present release of the tool only supports characters below U+0100; support for characters outside of the extended ASCII subset of unicode is planned for a future release.

initial letter →: if codepoint < U+0100 then Any character in categories Ll, Lm, Lo, Lt, Lu, or the character U+0024 (\$) else Any character, excluding categories Cc, Zl, Zp, Zs, Cs, Cn, Nd, Pc. ;

following letter →: if codepoint < U+0100 then Any character in categories Ll, Lm, Lo, Lt, Lu, Nd, or the characters U+0024 (\$), U+0027 ('), and U+005F (_) else Any character, excluding categories Cc, Zl, Zp, Zs, Cs, Cn. ;

ascii letter →: Any character in the ranges [U+0041,U+005A] and [U+0061, U+007A] --- A-Z and a-z, respectively. ;

character →: Is left underdefined, except to note that it may be any unicode character except those that conflict with the lexical rule that uses the character class. For example, character does not include \ in the character literal rule. ;

identifier →

initial letter, { following letter }

;

digit →

0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9

;

hex digit →