A Formal Reference for SCOOP - Empirical Software Engineering and Verification - page 95

3.1 Syntax

The following EBNF grammar defines the set of all considered programs:

program = class declaration * root procedure declaration ;
root procedure declaration =

{ class name } . routine name ;

class declaration =
[ ”expanded” ] ”class” class name
”inherit” class name
[ ”create” routine name { ”,” routine name } ]

”feature” [ ” { ” class name { ”,” class name } ” } ” ] { feature declaration }

[ ”invariant” expression ]
”end” ;

feature declaration = routine declaration | attribute declaration ;

routine declaration =
routine name [ ”(” entity declaration { ”,” entity declaration } ”)” ][ ”:” type ]

[ ”require” expression ]
[ ”local” entity declaration

{ entity declaration } ]

( ”do” ”once” )

instruction

|

{ ”;” instruction }

[ ”ensure” expression ]
”end” ;
attribute declaration = entity declaration ;
entity declaration = entity name ”:” type ;

instruction =
entity name ”:=” expression |

expression ”.” feature name [ ”(” expression

{ ”,” expression } ”)” ] |

”create” entity name ”.” routine name [ ”(” expression { , expression } ”)” ] |

”if” expression ”then” instruction { ”;” instruction } ”else” instruction { ”;”

|
”until” expression ”loop” instruction

instruction } ”end”

{ }

”;” instruction ”end” ;

expression =
literal |

entity name

|
expression ”.” feature name [ ”(” expression { , expression } ”)” ];

literal = boolean literal | integer literal | character literal | void literal ;

boolean literal = ”True” | ”False” ;

integer literal =[ ” − ” ]( ”0” | ... | ”9” ) { ”0” | ... | ”9” } ;

character literal = ” ' ””a” | ... | ”z” | ”A” | ... | ”Z” | ”0” | ... | ”9” ” ' ” ;

void literal = ”Void” ;

type =
[ detachable tag ]