このブログは、旧・はてなダイアリー「檜山正幸のキマイラ飼育記 メモ編」（http://d.hatena.ne.jp/m-hiyama-memo/）のデータを移行・保存したものであり、今後（2019年1月以降）更新の予定はありません。

今後の更新は、新しいブログ http://m-hiyama-memo.hatenablog.com/ で行います。

HoareRules

プログラム意味論 雑記 説明

かつて、次のURLsで書いた短い記事群をまとめてみた。文章はそのまま。

HoareRules 記述構文

ホーア論理、ホーア式については何度か触れたことがあります（例えば、「デュアルプログラミングとエクソシストゲーム」、「極小プログラミング言語とホーア論理」）。ホーア式（ホーア論理における論理文）を記述する構文と実行フレームワークがあると便利そうです。ホーア式というと、その用途として単体テスト／振る舞い記述が思い浮かびますが、その他の用途でも意外に広く適用できるような気がしてきました。

まず構文ですが、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です。

一方、ルール（ホーア式全体）ではセミコロンが終端記号になっています。空ルールを認めれば、セミコロンを分離記号扱いでもいいのですが、とりあえずこれでいくことにします。（アンバランスさには目をつむる。）

拡張や変更をするかも

  • '&&', '||', '!' 以外の演算子はいれてません。'=='とかはあったほうがいいかもしれません。
  • 事前条件やアクションの省略を許したほうが書きやすいかもしれません。
  • パーズ結果のデータ・モデルは定義するもつもりです。

実装上の問題

条件式（論理式）には演算子が入っているので、パージングのとき、演算子の優先順位／結合性、それと括弧の影響を考慮しないとキチンとしたパーズ・ツリーが作れないでしょう。そのへんのところって、パーザー・ジェネレータがやってくれるんだっけ？

HoareRulesのラベル

nmTokenをああいう定義にすると、name⊂nmToken、integer⊂nmTokenになってしまって、どうも気持ち悪いですね。

しかし、たいていのレクサー・ジェネレータは文脈により字句解析規則を切り替えることができるだろうから、ラベルの認識は別な文脈にすることにしましょう。つまり：



/* ルール全体のトップレベルでのみ認識される字句 */

labelChar ::= [-._a-zA-Z0-9] // ハイフンとピリオドも許すことにした

labelToken ::= labelChar+
/* ルール全体の構文定義 */

rule ::= '[' labelToken ']' preCondition action postCondition ';'

labelTokenの定義はルール・トップレベルの、'['から']'のあいだだけで有効。nameやnumberは別な文脈で認識されるので、かぶることはなくなります。

HoareRulesの関数構文、その意味的区別

構文的には関数呼び出しであっても、用途／役割、あるいは型（タイプ）により、次の3種に分類されます。

  1. 述語 -- 戻り値はboolean、副作用なし。
  2. （狭義の）関数 -- 戻り値の型は任意、値を必ず戻す。副作用なし。
  3. コマンド -- 戻り値の型は任意、値がなくてもよい(void戻り値）。副作用があってもよい。

使い方と制限は：

  1. 条件式のトップレベルに出現できるのは述語だけ。
  2. 条件式の述語引数内に出現できるのは（狭義の）関数だけ。ただし、述語も関数の一種とみなす。
  3. アクション（複文の）のトップレベルに出現できるのはコマンドだけ。
  4. アクションのコマンド引数内には何でも出現できるが、値を返さないコマンドはまずい。

以後、混乱を避けるために、関数呼び出し構文に対応する実体をコーラブルと呼び、狭義の（副作用なし、値を戻す）関数を単に関数と呼びましょう。原理的には、関数をコマンドとして使っても何の問題もないのですが、ここでは関数とコマンドは排他的概念としておきます。まとめると：

  • 述語⊂関数⊂コーラブル
  • コマンド⊂コーラブル
  • 関数∩コマンド = 空 （互いに排他的）
  • コーラブル = 関数∪コマンド

HoareRulesの実行フレームワーク

構文だけを示しても実感がないでしょうから、どのように実行されるかを記述します。実装言語はJavaということにします。

コーラブルの実装方式

コーラブル（述語、関数、コマンド）に組み込みのものは存在しません。すべてユーザー定義です。次のようなインターフェースの実装クラスとしてコーラブルを定義します。



public interface Callable {

 public Object call(Object[] args) throws Exception;

}



public interface Function extends Callable {

}



public interface Predicate extends Function {

 Boolean call(Object[] args) throws Exception;

}



public interface Command extends Callable {

}

コーラブルの名前は、getName()を設けるとかアノテーションで書くとかの方法もありますが、ここでは素朴に“設定ファイル”を使うことにします。設定ファイルの1行は、「種別 名前 クラス名」とでもしておきましょう。例えば：



predicate empty org.example.hoge.Empty

predicate less org.example.hoge.Less

function add org.example.hoge.Add

command doUpdate com.example.foo.DoUpdate

この方式では次の点を注意する必要があります。

  1. 設定ファイルには引数・戻り値の情報がないので、引数の個数・型のチェックはコーラブル実装側の責任になる。
  2. ==, <, + などの基本的演算子もないので、コーラブルとして実装する必要がある。
  3. コーラブルが所属する名前空間はフラットなので、名前の衝突に気を付ける。

いずれも好ましくない特徴ですが、まー、これでもいいとします。ユーザー定義の（プラグインの）コーラブルは、引数なしコンストラクタで生成されて、設定された種別と名前で使用されます。

問題や要求があれば、コーラブルに関する情報を（アノテーションを含む）リフレクションにより取得して、精密な引数・戻り値情報に基づいた型チェックをフレームワーク側で行うことも考慮します（ってことは、問題／要求がなければやらないってこと）。

フレームワークの仕事

構文解析によって作られたルールのデータ構造をたどりながら、次のチェックをします。

  1. 条件式のトップレベルに出現するコーラブルが“存在する述語”であるかどうか。
  2. アクションのトップレベルに出現するコーラブルが“存在する”かどうか。
  3. 引数内に出現するコーラブルが“存在する関数”であるかどうか。

以前と考えが変わったのは、「アクションのトップレベルはコマンド」の制限をはずして、どんなコーラブルでもよい、としたところです。

次に、式とアクションの評価ですが：

  1. 変数は出現したら生成し（データ構造をたどったときに作っておいてもいいが）、初期値はnullとする。
  2. リテラルはそれ自身に評価される。
  3. コーラブルの呼び出しは、事前に全ての引数を評価して引数リスト（配列）を作り、生成したコーラブル実体のcallを呼び出す。
  4. 代入文は、右辺を評価した結果を変数としてセットする。代入文以外の“文の値”は捨てる。

変数とコーラブルは、名前をキーとしてマップで管理するでしょうが、変数とコーラブルで別なマップを使うことにします。つまり、同じ名前の変数とコーラブルを許します（この事を後で使うかもしれない）。

それから

以上のような評価に便利なようにパーズ結果データ構造を考えることにします。それと、ルールの成功・失敗に応じた処理についても考える必要があります。

HoareRules CallableLibrary

コーラブルはすべてユーザー（利用者）定義となるわけだが、このコーラブル群とHoareRules実行フレームワークは切り離そう。適当なインターフェースを仕切りにして、コーラブルの詳細は隠蔽する。



public interface CallableLibrary {

 // 実行フレームワークから呼ぶ必要があるメソッド群

}

絶対に必要なのは：



 // 名前をキーとしてコーラブルを取得、なければnullが返る。

 // 僕はgetXxx()よりxxx()が好き
 public Callable callable(String name);

 public Function function(String name); // 述語も関数に含まれることに注意

 public Predicate predicate(String name);

 public Command command(String name);

記事「HoareRulesの実行フレームワーク」の「フレームワークの仕事」のところを見れば、これだけでも仕事ができるはず（commandは不要とも言える）。

別な考え方としては、「コーラブル実体を取得する必要はない」点に注目するのもある。ほんとに欲しいのは：

  1. 名前からコーラブルの存在確認ができること（検証のとき）
  2. 名前と引数配列によりコーラブルを呼び出せること（評価・実行のとき）



 // 存在確認

 public boolean hasCallable(String name);

 public boolean hasFunction(String name);

 public boolean hasPredicate(String name);

 public boolean hasCommand(String name);
 // 呼び出し

 public Object call(String name, Object[] args) throws Exception;

こっちの方法だと、実行フレームワークはコーラブル実体に触れないので、CallableLibrary内部にコーラブルコードをインラインコーディング（埋め込み）で書き込んだりできて、安直さが増す。



public Object call(String name, Object[] args) throws Exception {

 if (name.equals("foo")) {

  // fooのコード

 } else if (name.equals("bar")) {

  // barのコード

 } else {

  throw new CallableNotFoundException(name);

 }

}

絶対必須ではないのだけど、CallableLibraryはコレクション（モノの集まり）だから、メンバー列挙があるほうがいいかも。いまどきのメンバー列挙はイテレータでしょう。が、例えば、lib.allPredicates() で述語が列挙されてもうれしくない。なぜなら、コーラブル実体はメタデータを（名前さえも）持たないので正体不明。そもそも「実行フレームワークはコーラブル実体に触れない」方式とは相容れないし。

名前（文字列）を列挙する、Iterable<String> callableNames(), functionNames(), predicateNames(), commandNames() あたりが妥当かな。まー、実行時にメンバー列挙が必要な状況になるまでは入れなくていいけど（ミニマリスト発想、別名手抜き主義）。