Petra BNF (with lower-case terms)

3. PETRA: ABSTRACT SYNTAX

obj ::= A{β* φ* δ*}
β ::= x_i : A_i
φ ::= p = e
δ ::= m = {c}
e ::= x_i.p | e & e | e ∨ e | e + e | !e | (e)
d ::= d + d | p
c ::= c + c | [pre] s [post]
pre, post ::= d
s ::= z | skip | assume
z ::= z ∥ z | q
q ::= q ; q | x_i.m

2. PETRA: CONTROLLED ENGLISH

obj ::= A HAS β*, AND IS IN ONE OF P_φ STATES,
WHERE φ*, AND HAS ACTIONS δ*.
β ::= A x_i WHICH IS SOME A_i,
φ ::= p MEANS e,
δ ::= m WHERE c,
e ::= x_i P | e AND e | e OR e | e EITHER e | NOT e | (e)
d ::= d, or d | p
c ::= c, or c | IF ONLY pre, WHEN s COMPLETES, THEN post
pre, post ::= d
s ::= z | DO NOTHING | ASSUMED OPERATION
z ::= z SEPARATELY WITH z | q
q ::= q before q | m x_i

3. PETRA-JAVA: CONCRETE SYNTAX

obj ::= A{β* φ* δ*}
β ::= private final A_i x_i = new A_i();
φ ::= boolean p(){ return e; }
δ ::= void m(){ return c }
e ::= x_i.p | e && e | e || e | e ^ e | !e | (e)
d ::= d ^ d | p
c ::= c else c | if(pre){ s; assert(post); }
pre, post ::= d
s ::= sep(z) | seq(z) | par(z) | ; | assume
z ::= z , z | () -> {q;}
q ::= q ; q | x_i.m()