Petra BNF (with capitalized 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) | ; | EDGE
Z ::= Z , Z | () -> {Q;}
Q ::= Q ; Q | x_i.M()