述語変換意味論

述語変換意味論（じゅつごへんかんいみろん、Predicate Transformer Semantics）は、エドガー・ダイクストラによるホーア論理の拡張であり、その後も他の研究者が改良を加えたものである。最初に登場したのはダイクストラの論文 "Guarded commands, nondeterminacy and formal derivation of programs" であった。

概要

述語変換意味論では、命令型プログラミング言語の意味論（プログラム意味論）を定義するため、その言語の各「コマンド」に「述語変換子; Predicate Transformer」を対応させる。「述語変換子」は、プログラムの部分について2つの述語を対応させる全体関数である。

逐次的命令型プログラミングの基本的な述語は、最弱事前条件 $wp(S,R)$ で表される。ここで S はコマンドのリスト、R は事後条件空間内の述語を意味する。この関数を適用することで R が真となって完了する S の最弱事前条件（weakest precondition）が得られる。以下に代入文の例を挙げる:

wp(x:=E,R)=R_{E}^{x}

これはつまり、R の中の x を E に置換した述語が得られることを意味する。整数型変数 x と y について代入文の wp を正しく計算した例を以下に示す:

wp(x:=y-5,x>10)=(y-5>10)=(y>15)

この意味は、事後条件 x > 10 が代入実行後に真となるためには、事前条件として y > 15 が代入前に成り立っていなければならないことを示している。これも最弱事前条件であり、代入後に x > 10 を真とするために最低限必要となる y に対する条件である。

ダイクストラは他にも選択（if）や繰り返し（do）、接合演算子（;）を wp を使って定義した。選択や繰り返し構文はガード付きコマンドを使って実行を制御する。彼が wp の定義に課した規則により、コマンドのガードが互いに素でない場合、これらの構文では非決定的実行が可能になる。

他の形式主義的意味論とは異なり、述語変換意味論は計算の基礎を研究するような設計ではない。むしろ、プログラマが計算をするような感覚でプログラムの正しさを確認する手法を与えるものである。この手法はダイクストラらが提唱し、Ralph-Johan Back の Refinement Calculusで高階論理へと拡張された。

なお、逐次型プログラミングの意味論として最弱事前条件は広く認知されているが、これが唯一の述語変換子ではない。例えば、レスリー・ランポートは並行プログラミングのための述語変換子として win と sin を提唱した。

参考文献

Edsger W. Dijkstra, "Guarded commands, nondeterminacy and formal derivation of programs". Communications of the ACM, 18(8):453–457, August 1975. [1]
Leslie Lamport, "win and sin: Predicate Transformers for Concurrency". ACM Transactions on Programming Languages and Systems, 12(3), July 1990. [2]
Ralph-Johan Back and Joakim von Wright, Refinement Calculus: A Systematic Introduction, 1st edition, 1998. ISBN 0-387-98417-8.
Edsger W. Dijkstra. A Discipline of Programming (A systematic introduction with examples). ISBN 0-613-92411-8.

概要

関連項目

参考文献