Think Stitch
PRINCIPIA  最近の更新


コンポーネントの交換と正当性

コンポーネント P を使って作られたシステム SYSTEM があるとします。 システムは与えられた仕様 SPEC を満たしています。 あるとき、コンポーネント P をアップグレードする要求が発生したとしましょう。 たとえば、より効率的なアルゴリズムを使ったものに置き換えたいとか、ハードウェア支援を使うものに入れ替えたいとか、そういう理由によってです。

仕様は変わらないので、新しい機能を追加する、ということではありません。 したがって、新しいコンポーネントを Q とすると、P を Q で置き換えたシステムも、仕様 SPEC を満たさなければなりません。

もしコンポーネント P と Q が同じ動作をするものであれば、当然置き換えた後のシステムは仕様を満たすでしょう。 当然とかいっちゃいましたけど、現実にはあまり当然ではないですけどね。 そもそも同じ動作をするかどうかを完全に確認することはできませんし。テストにだって漏れはありますから。 まあ、理想的にはそうだ、ということです。

さて、ここで考えたいのは、P と Q が同じではなくて、正当性関係にある場合はどうかということです。 コンポーネント P に非決定性がなければ、これは P = Q と同じことです。 でもそうでなければ、P とは異なる振る舞いをする Q が複数あり得ます。 このとき、Q で置き換えたシステムは仕様を満たすでしょうか。

答えは YES です。 いま、システムの P の部分を外して、穴の空いたシステムを考えたとします。 これを SYSTEM[X] と書くことにします。 (図のチェックの部分は穴が空いているつもり。) システムが状態遷移図で記述されているなら図の一部分、プロセス式だったら式の一部や名前のついたプロセスを丸ごといくつか外しておくということです。 SYSTEM[X] はテンプレートのようなもので、穴の部分 X にいろいろなコンポーネントを入れると、それに応じていろいろなシステムになるというわけです。 もちろんインターフェイスは合わないといけないですけど。

このとき SYSTEM[X] は次のような性質を持っています。 X に入れることのできるコンポーネント(プロセス) P と Q が P ⊑ Q を満たすならば、SYSTEM[P] ⊑ SYSTEM[Q] が成り立ちます。

これはおよそ自明とは程遠い性質です。 だって、どんなシステムでも、どんな穴を空けてもそうなるのですから。 CSP の各演算子がこの性質を持っているので、CSP で記述されたプロセスは自動的にこの性質を持つのです。 このことは CSP の数学的な理論で保証されている事実です。

さらに、プロセスの間の関係 ⊑ は推移律を満たします。 どういうことかというと、A ⊑ B かつ B ⊑ C だったら、B を飛ばして A と C の間にも A ⊑ C が成り立つということです。

この2つの性質をまとめると次のようになります。 コンポーネントをアップグレードするときは、コンポーネントの正当性だけを確認すれば十分だということです。 入れ替えたあとのシステム全体の正当性確認を、再度行う必要はないのです。

この性質は、システムをチームで設計する場合にも重要です。 システム全体を設計する人は、システムを分割し、そのコンポーネントの1つとして S の動作を規定するでしょう。 システムのモデルが仕様を満たすことを確認するのはこの人の責務です。 確認が済んだら、S のモデルを実装者に渡します。 つまり、S が実装者にとっては実装すべきコンポーネントの仕様になります。

コンポーネント S の実装者は、実装モデル P を作り、正当性関係を確認します。 コンポーネント S の実装者はこれだけを確認すればよく、システム全体の正当性を気にしたり、確認したりする必要はありません。 S ⊑ P だけ確認すれば、システム全体の正当性は自動的に保証されるからです。

くどいですけど、システム全体の設計者が P を受け取って再度確認する必要もありません。 (もちろん実コードでのテストはしますよ。あくまで、設計初期段階、あるいは繰り返しの初期段階でのモデルによる設計検討での話です。)

一般に、開発ではこのことを当然のように、あるいは暗黙に仮定しているでしょう。 (設計や実装で非決定性を減らしていることもあまり意識していないからです。) でも自明ではないのです。 いま使っているプログラミング言語や設計手法、手法が大げさなら考え方でもいいですが、もしかしたらこの性質を持っていないかもしれませんよ :P

補足

実践的にはこういう性質があるということだけを知っていて利用できれば十分だと思います。 もし、どうしてこれがいえるのか、その理由を知りたい場合は

A W Roscoe, The Theory and Practice of Concurrency, Prentice Hall, 1998

を見てください。 Roscoe さんのページから PDF をダウンロードできます。

数学にも興味がある人のために、もう少し蛇足を付け加えさせてください。 正当性関係 ⊑ は大小関係 ≤ に似ています。記号も似ています。 正当性関係を順序のように考えながら、改めて1番目の条件を見るとこうです。

P ⊑ Q ならば C[P] ⊑ C[Q]

ここでは SYSTEM[X] の代わりに C[X] と書きました。 文献ではコンテキストと呼ばれているからです。 プロセス X が、より大きなプロセス記述 C[ ] の中に置かれているので、文脈という意味なのでしょう。

このような性質は単調性と呼ばれています。 大小関係だったら関数 C[X] は単調増加関数ということです(厳密には非減少ですが)。 CSP の記述はこのような単調性を持っているということです。 このことは解析学の力を借りて示すことができます。 極限や連続性、距離に不動点など、面白い話がたくさん出てきます。 わくわくしますね。実践で役に立つだけでなく、理論自体もとても面白いです。 数学的に根拠づけられた理論があるから、安心して実用できるということですね。 機械や電気の分野だけでなく、ソフトウェア開発でも数学はとても役に立つということです。

2013/08/14
© 2013,2014,2015 PRINCIPIA Limited