<> <> <<>> Notation: Terminals are SMALL CAPS, underlined, or punctuation other than bold ? ( ) | ,.. ;.. ( ) are terminal only in lhs, interval, element, id | is terminal only in default item | item choose one ?item zero or one item ( | item ) -- comment notation item ,.. one or more items, separated by "," ( item | item , item | item , item , item | ... ) item ;.. one or more items, separated by ";" ( item | item ; item | item ; item ; item | ... ) module::= ?directory n : ?CEDAR ( defsHead tilde defsBody | implHead tilde implBody ) . directory::= DIRECTORY ?( include ,.. ) ; include::= n ?( : TYPE ?n | : FROM string ) ?( USING [ ?( n ,.. ) ] ) defsHead::= DEFINITIONS ?locks ?imports ?shares implHead::= ?safety ( PROGRAM | MONITOR ) arguments ?locks ?imports ?exports ?shares defsBody::= ?access { ?open definition ;.. ?; } | ?access BEGIN ?open definition ;.. ?; END implBody::= ?access ?checking block locks::= LOCKS primary ?( USING n : t ) imports::= IMPORTS ?( ( n | n : n ) ,.. ) exports::= EXPORTS ?( ( n | n : n ) ,.. ) shares::= SHARES n ,.. access::= PUBLIC | PRIVATE safety::= SAFE | UNSAFE checking::= CHECKED | TRUSTED | UNCHECKED binding::= n ,.. : ?access ?entry t tilde initVal | n ,.. : ?access TYPE tilde ?access t ?default definition::= binding | n ,.. : ?access ?READONLY t | n ,.. : ?access TYPE ?( [ e ] ) declaration::= binding | n ,.. : ?access t ?( _ initVal ) entry::= ENTRY | INTERNAL tilde::= ~ | = initVal::= e | trash | CODE | ?checking ?INLINE block | ?checking MACHINE CODE machineCode machineCode::= { ?( ( e ,.. ) ;.. ?; ) } | BEGIN ?( ( e ,.. ) ;.. ?; ) END default::= _ e | _ trash | _ | _ e | trash -- note the terminal "|" -- trash::= TRASH | NULL statement, s::= NULL | lhs | lhs _ e | [ argList ] _ e | ERROR | ERROR lhs | RETURN WITH ERROR lhs | SIGNAL lhs | WAIT lhs | NOTIFY lhs | BROADCAST lhs | JOIN lhs | EXIT | LOOP | GOTO n | GO TO n | RETURN | RETURN [ argList ] | RETURN lhs | CONTINUE | RETRY | REJECT | RESUME | RESUME [ argList ] | RESUME lhs | ?checking block | ?for ?while DO scope ?repeat ENDLOOP | IF e THEN s ?( ELSE s ) | SELECT e FROM ?( ( test ,.. => s ) ;.. ?; ) ENDCASE ?( => s ) | WITH e SELECT FROM ?( ( n : t => s ) ;.. ?; ) ENDCASE ?( => s ) | WITH openItem SELECT ?e FROM ?( ( e ,.. => s ) ;.. ?; ) ENDCASE ?( => s ) | ?( lhs . ) FREE [ e ?catch ] | lhs _ STATE | STATE _ e | STOP | START lhs | RESTART lhs | TRANSFER WITH lhs | RETURN WITH lhs block::= { scope ?exits } | BEGIN scope ?exits END scope::= ?open ?enable ?( declaration ;.. ; ) ?( s ;.. ?; ) open::= OPEN openItem ,.. ; openItem::= e | n : e | n ~~ e enable::= ENABLE ( lastCatch | { ?( catchList ?; ) } | BEGIN ?( catchList ?; ) END ) ; catchItem::= lhs ,.. => s lastCatch::= catchItem | ANY => s catchList::= catchItem ; catchList | lastCatch exits::= EXITS ?( exit ;.. ?; ) exit::= n ,.. => s for::= FOR n ?( : t ) _ e , e | FOR n ?( : t ) ?DECREASING IN range | THROUGH range while::= WHILE e | UNTIL e repeat::= REPEAT ?( exit ;.. ?; ) ?( FINISHED => s ?; ) test::= e | relationTail expression, e::= lhs _ e | [ argList ] _ e | disjunct | IF e THEN e ELSE e | SELECT e FROM ?( ( test ,.. => e ) ,.. ?, ) ENDCASE => e | WITH e SELECT FROM ?( ( n : t => e ) ,.. ?, ) ENDCASE => e | WITH openItem SELECT ?e FROM ?( ( e ,.. => e ) ,.. ?, ) ENDCASE => e | ERROR | ERROR lhs | SIGNAL lhs | FORK lhs | JOIN lhs | NEW lhs | START lhs argList::= arg ,.. | ( n ~ arg | n : arg ) ,.. arg::= e | | trash disjunct::= ?( disjunct OR ) conjunct conjunct::= ?( conjunct AND ) negation negation::= ?( NOT | ~ ) relation relation::= sum ?relationTail relationTail::= ?NOT ( = | # | < | <= | > | >= | ~< | ~> | ~= ) sum | ?NOT IN range range::= ?typeName interval | typeName sum::= ?( sum ( + | - ) ) product product::= ?( product ( * | / | MOD ) ) factor factor::= ?( + | - ) primary primary::= NIL | lhs | [ argList ] | prefixOp [ arg ,.. ] | ALL [ arg ] | VAL [ arg ] | ISTYPE [ e , t ] | typeOp [ t ] | SIZE [ t , e ] | ?( lhs . ) NEW [ t ?( _ initVal | tilde initVal ) ?catch ] | ?( lhs . ) CONS [ argList ?catch ] | ?( lhs . ) LIST [ argList ] | DESCRIPTOR [ e ?( , e ?( , t ) ) ] | @ lhs lhs::= literal | n | ( e ) | lhs [ argList ?catch ] | lhs . n | lhs . prefixOp | lhs . typeOp | lhs ^ | APPLY [ e , e ?catch ] | NARROW [ e ?( , t ) ?catch ] | LOOPHOLE [ e ?( , t ) ] catch::= ! ?( catchList ?; ) prefixOp::= LONG | PRED | SUCC | ORD | ABS | MIN | MAX | BASE | LENGTH typeOp::= FIRST | LAST | NIL | SIZE | CODE type, t::= typeName | typeConstructor typeName::= qualifiedName | n typeName qualifiedName::= ?( qualifiedName . ) n typeConstructor::= typeApplication | LONG t | VAR t | ?UNCOUNTED ZONE | ?typeName interval | ?( MACHINE DEPENDENT ) { ?( element ,.. ) } | ?( MACHINE DEPENDENT ) ?MONITORED RECORD fields | ?PACKED ARRAY ?t OF t | ?safety ( PROCEDURE | PROC | SIGNAL | ERROR | PROCESS | PROGRAM | PORT ) arguments | REF ?READONLY t | REF ?READONLY ANY | REF | LIST OF ?READONLY t | typeName PAINTED t | typeName RELATIVE t | DESCRIPTOR FOR ?READONLY t | ?ORDERED ?BASE POINTER ?interval ?( TO ?READONLY t ) | FRAME [ n ] typeApplication::= typeApplication . n | typeName [ e ] | typeApplication [ e ] interval::= [ e .. e ] | [ e .. e ) | ( e .. e ] | ( e .. e ) element::= n | n ( e ) | ( e ) id::= n | n ( e ) | n ( e : e .. e ) field::= t ?default nfield::= id ,.. : ?access field variant::= ( union | sequence ) ?default nvariant::= id : ?access variant fields::= NULL | [ ] | [ nfield ,.. ] | [ ?( nfield ,.. , ) nvariant ] | [ field ,.. ] | [ variant ] union::= SELECT tag FROM ( n ,.. => fields ) ,.. ?, ENDCASE tag::= ( id : ?access | COMPUTED | OVERLAID ) ( t | * ) sequence::= ?PACKED SEQUENCE ( id : ?access | COMPUTED ) t OF t params::= [ ] | [ nfield ,.. ] | [ field ,.. ] | ANY arguments::= ?params ?( RETURNS params ) name, n::= letter | n ( letter | digit ) -- no spaces in this or following rules literal::= num ?( ( D | d | B | b ) ?num ) | hex ( H | h ) ?num | num exponent | num . ?exponent | ?num . num ?exponent | string | ' extendedChar | num C | $ n num::= digit | num digit hex::= digit | hex ( digit | A | B | C | D | E | F ) exponent::= ( E | e ) ?( + | - ) num string::= " extendedChar ... " -- quotes enclose zero or more characters (other than ") extendedChar::= char | \ escapeCode -- char is any character other than \ escapeCode::= n | N | r | R | t | T | b | B | f | F | l | L | ' | " | \ | digit digit digit