Hoare流クアドラプル

トリプルじゃなくてクアドラプル（quadruple）。

(P, E; Q, F)なんだが、構文じゃなくて意味を使って説明する； コンポネントの（内部＋外部）状態空間をX、コンポネントのプラス（積極的、送り側）アルファベットをA、マイナス（消極的、受け側）アルファベットをBとする。P⊆X、Q⊆X、E⊆A^*、F⊆B^*である。その意味は：

• 状態がP内にあるとき、Eに含まれるメッセージを送出すれば、状態はQ内に入り、Fに含まれるどれかのメッセージをいずれ受け取る。

逆（外の人）の立場で読むと：

• 状態がP内にあるとき、Eに含まれるメッセージを受け取ったなら、状態はQ内に入り、Fに含まれるどれかのメッセージを送らなくてはならない。

うーん、いかにも様相、時相がからんできそうだ。

追記：あ、そうだ。(P, E; Q, F)を、when(P) sending {E} results(Q) cases {F}.とか書こうとしていた。あと、when(P) receiving {E} results(Q) motivates{F}.