Guide

Grammar

⟨bexpr⟩::=  ⟨aexpr⟩⟨rel-op⟩⟨aexpr⟩∣    "true"  ∣    "false"  ∣    "!"  ⟨bexpr⟩∣    "("  ⟨bexpr⟩  ")"  ∣  ⟨bexpr⟩  "&"  ⟨bexpr⟩∣  ⟨bexpr⟩  "|"  ⟨bexpr⟩⟨rel-op⟩::=    "<"  ∣    ">"  ∣    "<="  ∣    ">="  ∣    "="  ∣    "!="  ⟨var⟩::=    r"[_a-zA-Z][_a-zA-Z0-9]*"  ⟨command⟩::=  ⟨predicate-block⟩∗⟨command-kind⟩⟨predicate-block⟩∗⟨command-kind⟩::=  ⟨var⟩  ":="  ⟨aexpr⟩∣    "skip"  ∣    "if"  ⟨guard⟩  "fi"  ∣    "do"  ⟨predicate-inv⟩⟨guard⟩  "od"  ∣  ⟨command⟩  "[]"  ⟨command⟩⟨guard⟩::=  ⟨bexpr⟩  "->"  ⟨command⟩∣  ⟨guard⟩  "[]"  ⟨guard⟩⟨predicate-block⟩::=    "{"  ⟨predicate⟩  "}"  ⟨predicate-inv⟩::=    "["  ⟨predicate⟩  "]"  ⟨predicate⟩::=  ⟨aexpr⟩⟨rel-op⟩⟨aexpr⟩∣    "true"  ∣    "false"  ∣    "!"  ⟨predicate⟩∣    "("  ⟨predicate⟩  ")"  ∣  ⟨predicate⟩  "&"  ⟨predicate⟩∣  ⟨predicate⟩  "|"  ⟨predicate⟩∣  ⟨predicate⟩  "==>"  ⟨predicate⟩∣  ⟨quantifier⟩⟨var⟩  "::"  ⟨predicate⟩⟨quantifier⟩::=    "exists"  ∣    "forall"  ⟨aexpr⟩::=  ⟨int⟩∣  ⟨var⟩∣    "old("  ⟨var⟩  ")"  ∣    "-"  ⟨<aexpr>⟩∣    "("  ⟨<aexpr>⟩  ")"  ∣  ⟨aexpr⟩  "*"  ⟨aexpr⟩∣  ⟨aexpr⟩  "/"  ⟨aexpr⟩∣  ⟨aexpr⟩  "+"  ⟨aexpr⟩∣  ⟨aexpr⟩  "-"  ⟨aexpr⟩∣  ⟨function⟩⟨function⟩::=    "division"    "("  ⟨aexpr⟩  ","  ⟨aexpr⟩  ")"  ∣    "min"    "("  ⟨aexpr⟩  ","  ⟨aexpr⟩  ")"  ∣    "max"    "("  ⟨aexpr⟩  ","  ⟨aexpr⟩  ")"  ∣    "fac"    "("  ⟨aexpr⟩  ")"  ∣    "fib"    "("  ⟨aexpr⟩  ")"  ∣    "exp"    "("  ⟨aexpr⟩  ","  ⟨aexpr⟩  ")"   \begin{aligned} \langle \textit{bexpr} \rangle ::= & \;\langle \textit{aexpr} \rangle \langle \textit{rel-op} \rangle \langle \textit{aexpr} \rangle \\ \mid & \;\;\texttt{"true"}\; \\ \mid & \;\;\texttt{"false"}\; \\ \mid & \;\;\texttt{"!"}\; \langle \textit{bexpr} \rangle \\ \mid & \;\;\texttt{"("}\; \langle \textit{bexpr} \rangle \;\texttt{")"}\; \\ \mid & \;\langle \textit{bexpr} \rangle \;\texttt{"\&"}\; \langle \textit{bexpr} \rangle \\ \mid & \;\langle \textit{bexpr} \rangle \;\texttt{"|"}\; \langle \textit{bexpr} \rangle \\\langle \textit{rel-op} \rangle ::= & \;\;\texttt{"<"}\; \mid \;\;\texttt{">"}\; \mid \;\;\texttt{"<="}\; \mid \;\;\texttt{">="}\; \mid \;\;\texttt{"="}\; \mid \;\;\texttt{"!="}\; \\\langle \textit{var} \rangle ::= & \;\;\texttt{r"[\_a-zA-Z][\_a-zA-Z0-9]*"}\; \\\langle \textit{command} \rangle ::= & \;\langle \textit{predicate-block} \rangle ^* \langle \textit{command-kind} \rangle \langle \textit{predicate-block} \rangle ^* \\\langle \textit{command-kind} \rangle ::= & \;\langle \textit{var} \rangle \;\texttt{":="}\; \langle \textit{aexpr} \rangle \\ \mid & \;\;\texttt{"skip"}\; \\ \mid & \;\;\texttt{"if"}\; \langle \textit{guard} \rangle \;\texttt{"fi"}\; \\ \mid & \;\;\texttt{"do"}\; \langle \textit{predicate-inv} \rangle \langle \textit{guard} \rangle \;\texttt{"od"}\; \\ \mid & \;\langle \textit{command} \rangle \;\texttt{"[]"}\; \langle \textit{command} \rangle \\\langle \textit{guard} \rangle ::= & \;\langle \textit{bexpr} \rangle \;\texttt{"->"}\; \langle \textit{command} \rangle \\ \mid & \;\langle \textit{guard} \rangle \;\texttt{"[]"}\; \langle \textit{guard} \rangle \\\langle \textit{predicate-block} \rangle ::= & \;\;\texttt{"\{"}\; \langle \textit{predicate} \rangle \;\texttt{"\}"}\; \\\langle \textit{predicate-inv} \rangle ::= & \;\;\texttt{"["}\; \langle \textit{predicate} \rangle \;\texttt{"]"}\; \\\langle \textit{predicate} \rangle ::= & \;\langle \textit{aexpr} \rangle \langle \textit{rel-op} \rangle \langle \textit{aexpr} \rangle \\ \mid & \;\;\texttt{"true"}\; \\ \mid & \;\;\texttt{"false"}\; \\ \mid & \;\;\texttt{"!"}\; \langle \textit{predicate} \rangle \\ \mid & \;\;\texttt{"("}\; \langle \textit{predicate} \rangle \;\texttt{")"}\; \\ \mid & \;\langle \textit{predicate} \rangle \;\texttt{"\&"}\; \langle \textit{predicate} \rangle \\ \mid & \;\langle \textit{predicate} \rangle \;\texttt{"|"}\; \langle \textit{predicate} \rangle \\ \mid & \;\langle \textit{predicate} \rangle \;\texttt{"==>"}\; \langle \textit{predicate} \rangle \\ \mid & \;\langle \textit{quantifier} \rangle \langle \textit{var} \rangle \;\texttt{"::"}\; \langle \textit{predicate} \rangle \\\langle \textit{quantifier} \rangle ::= & \;\;\texttt{"exists"}\; \mid \;\;\texttt{"forall"}\; \\\langle \textit{aexpr} \rangle ::= & \;\langle \textit{int} \rangle \\ \mid & \;\langle \textit{var} \rangle \\ \mid & \;\;\texttt{"old("}\; \langle \textit{var} \rangle \;\texttt{")"}\; \\ \mid & \;\;\texttt{"-"}\; \langle \textit{<aexpr>} \rangle \\ \mid & \;\;\texttt{"("}\; \langle \textit{<aexpr>} \rangle \;\texttt{")"}\; \\ \mid & \;\langle \textit{aexpr} \rangle \;\texttt{"*"}\; \langle \textit{aexpr} \rangle \\ \mid & \;\langle \textit{aexpr} \rangle \;\texttt{"/"}\; \langle \textit{aexpr} \rangle \\ \mid & \;\langle \textit{aexpr} \rangle \;\texttt{"+"}\; \langle \textit{aexpr} \rangle \\ \mid & \;\langle \textit{aexpr} \rangle \;\texttt{"-"}\; \langle \textit{aexpr} \rangle \\ \mid & \;\langle \textit{function} \rangle \\\langle \textit{function} \rangle ::= & \;\;\texttt{"division"}\; \;\texttt{"("}\; \langle \textit{aexpr} \rangle \;\texttt{","}\; \langle \textit{aexpr} \rangle \;\texttt{")"}\; \\ \mid & \;\;\texttt{"min"}\; \;\texttt{"("}\; \langle \textit{aexpr} \rangle \;\texttt{","}\; \langle \textit{aexpr} \rangle \;\texttt{")"}\; \\ \mid & \;\;\texttt{"max"}\; \;\texttt{"("}\; \langle \textit{aexpr} \rangle \;\texttt{","}\; \langle \textit{aexpr} \rangle \;\texttt{")"}\; \\ \mid & \;\;\texttt{"fac"}\; \;\texttt{"("}\; \langle \textit{aexpr} \rangle \;\texttt{")"}\; \\ \mid & \;\;\texttt{"fib"}\; \;\texttt{"("}\; \langle \textit{aexpr} \rangle \;\texttt{")"}\; \\ \mid & \;\;\texttt{"exp"}\; \;\texttt{"("}\; \langle \textit{aexpr} \rangle \;\texttt{","}\; \langle \textit{aexpr} \rangle \;\texttt{")"}\; \\ \end{aligned}