ホーア論理、ホーア式については何度か触れたことがあります（例えば、「デュアルプログラミングとエクソシストゲーム」、「極小プログラミング言語とホーア論理」）。ホーア式（ホーア論理における論理文）を記述する構文と実行フレームワークがあると便利そうです。ホーア式というと、その用途として単体テスト／振る舞い記述が思い浮かびますが、その他の用途でも意外に広く適用できるような気がしてきました。
まず構文ですが、JavaScriptやJSON構文を参考にした簡単なものにします。構文上は、明確なデータ型はありません。
字句 -- 文字と名前：
nameStartChar ::= [_a-zA-Z] // 英字とアンダスコア
nameChar ::= [_a-zA-Z0-9] // 英数字とアンダスコア
name ::= nameStartChar nameChar* // 予約語は除く
nmToken ::= nameChar+
名前は、変数名、関数名、定数名に使われます。名前トークンnmTokenはラベル（ルール名）として（それだけに）使用します。字句解析段階でnameとnmTokenの区別は曖昧なので（name⊆nmTokenだから）、字句としてはnmTokenだけでいいかもしれません。
字句 -- リテラル：
integer ::= {JSONと同じ}
decimal ::= {JSONと同じ}
number ::= integer | decimal
string ::= {JSONと同じ}
boolean ::= 'true' | 'false'
null ::= 'null'
/* true, false, nullは予約語となる*/
JavaScriptでいうところのオブジェクト／配列のリテラルは当面は入れません（いつか入れる可能性はある）。ここから先のBNFでは、空白と区切り記号で字句に切り分けた後の構文を記述します。
変数と関数：
variable ::= name
function ::= name '(' args ')'
値を表す式：
value ::= number | string | boolean | null | variable | function
関数の引数：
args ::= EMPTY | arg (',' arg)*
arg ::= value
さて、構文的には関数呼び出し（function）なのですが、意味的な区別として、述語とコマンドがあります。
precicate ::= boolean | function
command ::= function
条件式（論理式）：
condition ::= predicate | andExp | orExp | notExp | '(' condition ')'
andExp ::= condition '&&' condition
orExp ::= condition '||' condition
notExp ::= '!' condition
文とアクション（複文）：
statement ::= EMPTY | command | variable '=' function
action ::= '{' statement (';' statement)* '}'
ルール：
label ::= '[' nmToken ']'
preCondition ::= '(' condition ')'
postCondition ::= '(' condition ')'
rule ::= label preCondition action postCondition ';'
注意：セミコロンの使い方
アクション（複文）のなかで、セミコロンは文の終端記号ではなくて分離記号です。しかし、空文があるので{foo();}は{foo();＜空文＞}と解釈でき、終端記号として使っても問題ありません。{}も{;}もOKです。
一方、ルール（ホーア式全体）ではセミコロンが終端記号になっています。空ルールを認めれば、セミコロンを分離記号扱いでもいいのですが、とりあえずこれでいくことにします。（アンバランスさには目をつむる。）
拡張や変更をするかも
- '&&', '||', '!' 以外の演算子はいれてません。'=='とかはあったほうがいいかもしれません。
- 事前条件やアクションの省略を許したほうが書きやすいかもしれません。
- パーズ結果のデータ・モデルは定義するもつもりです。
実装上の問題
条件式（論理式）には演算子が入っているので、パージングのとき、演算子の優先順位／結合性、それと括弧の影響を考慮しないとキチンとしたパーズ・ツリーが作れないでしょう。そのへんのところって、パーザー・ジェネレータがやってくれるんだっけ？
