レベル: 初級 Eric Allen, Software Engineer, Cycorp, Inc.
2002年 7月 01日 従来のアサーションでもJavaコードに対して可能なチェックの程度を高めることができますが、従来のアサーションでは実行できないチェックもたくさんあります。そのギャップを埋める1つの方法として「時相論理」があります。これは、プログラムの状態が時間と共にどう変化するかを記述するのに使用されるための1つの表記形式です。この記事では、Eric Allen氏がアサーションについて論じ、時相論理について紹介し、プログラムで使用できるツールについて説明します。(次回の記事では、以前取り上げたバグ・パターンと時相論理の応用について調べます。)
Javaコードはチェックすればするほどよいということは、だれしも認めることです。新たなプログラミング、また改善されたプログラミングをテストするためにアサーション（表明）を活用する方法については、すでに検討しました。とはいえ、従来型アサーションはチェックの程度を高めはするものの、従来型アサーションでは実行できないチェックがたくさんあります。
しかし、チェックに関して、アサーションでは対応できないこのギャップを埋める方法があります。それは、時相論理の利用です。時相論理とは、プログラムの状態が時間と共にどう変化するかを記述するために使用される1つの表記形式です。では、アサーションとその特性について、また時相論理をチェックの中にどう取り入れるかについて調べてみましょう。その後、時相論理アサーションを処理するための1つのツールを紹介します。
アサーションとその特性
型検査と単体テスト以外に、アサーションはプログラムの中でさまざまな特性が維持されていることを決定する手段になります。
では、よく利用されるいくつかのアサーションの特性の3つのカテゴリー (よく利用されるがすべての場合を網羅するわけではない) について簡単に触れた後、それらを従来型アサーション言語で表現できるプログラム特性のタイプと比較し、マルチスレッド・コンテキストでは必要だが従来型アサーションとしては表現できないアサーション特性について調べてみましょう。サンプル・コードもいくつか示します。
よく利用されるアサーション特性
従来、アサーション特性は、以下の3つのカテゴリーのうちのいずれかに分類されてきました。
- 事前条件の表明 (ある特性ーがコード・ブロックの実行前 に満たす)。
- 事後条件の表明 (ある特性がコード・ブロックの実行後 に満たす)。
- 不変条件の表明 (ある特性がコード・ブロックの実行前 でも後 でも満たす)。
これらの典型的なアサーションは確かに便利ではありますが、プログラムの中で保持したいあらゆる特性をすべて網羅するものではありません。アサーションの形で表現されるプログラム特性の典型的な例を見てみましょう。
アサーションとして表現可能なプログラム特性
従来型アサーション言語で表現可能なプログラム特性 (プログラマーがコード中で利用したいような) の種類のリストを、ほんの少しですが以下に示します。
- どんなnonceも一度しか生成されないこと
- 許可されていないエージェントが文書にアクセスしないようにすること
- 各スレッドに実行の機会が与えられること
- システムがデッドロックに陥らないこと
nonce (number used once、ランダム・ストリング) の生成プログラムは、セキュリティー・プロトコルがトランザクションの新鮮さを保証するために使用されます。セキュリティーの1つの簡単な概念として、特定のnonceが生成されたなら、それが再度生成されないようにすることは重要です。セキュリティー上のもう1つの重要なアサーションは、許可を受けていないエージェントが機密文書にアクセスしないようにすることです。
マルチスレッド・コードの場合は、どのスレッドもいつかは実行の機会が与えられるということを保証するアサーションを設定したいと思うことがよくあります。また、複数のスレッドが、処理を継続するために互いに相手からのリソースを必要とし、それが提供されるのを互いに待機するという事態 (デッドロック) がシステム内で発生しないようにしたいものです。
重要な、しかし従来型でないアサーション特性
従来型アサーションでは表現できない (そしてマルチスレッド・コードのコンテキストではしばしば望ましい) 特性のうち、次の2つは非常に便利です。
- 安全(Safety)アサーション
- 活性(Liveness)アサーション
安全アサーションは、どんな状況においても、特定の望ましくないシステム状態が決して発生しないというものです。活性アサーションは、特定のイベントがいつかは発生するというものです (たとえば、特定のスレッドがいつまでもスリープ状態のままではなくいつかは実行される、など)。
時相論理を使用すれば、これらのアサーションを作成できます。
時相論理の使用方法
このようなアサーションは、通常のアサーション言語の表現能力を超えていますが、そのようなステートメントを表現するために利用できる表記形式およびツールがあります。それは時相論理 と呼ばれます。
時相論理の定義
時相論理は、時間と共に変化する特性に関して推論するために使用される様相 論理の一種です。
時間という要素を考慮すると、時相論理には一般に次の2種類があります。
- イベントのリニア・シーケンスとして将来をモデリングするもの
- さまざまな可能性のある分岐ツリー型として将来をモデリングするもの
この記事では、将来をイベントのリニア・シーケンスとしてモデリングする時相論理だけを考慮することにします。(「分岐ツリー」ロジックもなかなかよさそうではありますが、扱いは難しくなります。)
普通、時相論理は、従来型プログラム・アサーションなど、分割不能な (小単位の) 一連の単純な命題の上に構築されます。そして、それらの分割不能アサーションに対してさまざまな様相演算子を適用することによって、もっと複雑なアサーションを生成できます。and またはor など、従来型でブール型の論理演算子をそれらのアサーションに適用することによって、さらに複雑なアサーションを生成することができ、そのようにしてこの連鎖は続きます。新たに生成されたアサーションに基づいてさらに複雑なアサーションを生成することができ、この連鎖は際限なく続けることができます。
時相論理では、3個の様相演算子が使用されます (モデルによっては4個)。
典型的な様相演算子
時相論理で通常使用される様相演算子は、次のとおりです。
-
Always
-
Sometime
-
Until
-
Next (特殊なケース)
Always をアサーションに適用した場合、プログラムの実行の残りの部分において、そのアサーションがずっと成立することを保証します。
Sometime は、Always よりも効力の弱い演算子です。Sometime をアサーションに適用した場合、プログラム実行中、将来のどこかでアサーションが成立する時点がなければならない、というものです。
Until は、2つのアサーションに対するものであり、第1のアサーションが成立しなくなったなら第2のアサーションがすぐに成立しなければならない、というものです。
プログラム実行中などのように、一連の離散的なステップで構成される1つのモデルとして時間をみなすことのできるコンテキストでは、上のリストにNext 演算子が追加されることがあります。アサーションにNext を追加した場合、「次の」(Next) ステップにおいてそのアサーションが成立している、ということを保証するものになります。もちろん、これが意味を持つのは、時間を複数の離散的なステップに分割している場合だけです。
リスト1に、時相論理アサーションのいくつかの例を示します。
リスト1. 時相論理アサーションのサンプル
Always x != 0
Sometime x == 0
{x == y} implies {Next {x == y + 1}}
{x == y} Until {y == 0}
{x == 0} implies {Next {Always {x != 0}}} // xが0になるのは1回だけ
Sometime {! this.isInterrupted()} // このスレッドは永久に割り込まれない
|
次に示すのは、2つのスレッドについて、それらがデッドロックにならないというサンプル・アサーションです。(1つのスレッドがもう一方のスレッドによって実行されるタスクに関して保留になっているかどうかを調べるために、ブール・メソッドisWaitingOn が使用されている点に注意してください。)
リスト2. マルチスレッド化のサンプル
Always {x.isWaitingOn(y) implies {! y.isWaitingOn(x)}}
|
そして、時相論理は拡張可能です。
言語の拡張
時相論理の言語は、データベース内の値のコレクションに関する限量子を含むように拡張できます。たとえば、あるテーブルのすべての値についてアサーションが常に成立すること、あるいはテーブルのうち少なくとも1つの値について常に成立することをチェックすることができます。
この程度まで表現できるようになると、安全およびセキュリティーについて非常に強力なアサーションの構成が可能になります。たとえば、明示的なエージェント・オブジェクトがさまざまな文書へのアクセスを要求できるというコンテキストを考えてみてください。さまざまな文書を閲覧するエージェントの許可についてのアサーションを構成できます。
次に示すアサーションは、許可が与えられるまでどのエージェントも文書を閲覧できない、というものです。
リスト3. データベース・セキュリティーを示すサンプル
ForAll agents in AgentPool
{ForAll document in TopSecretDocumentPool
{{! agent.canView(document)} Until {agent.hasClearanceFor(document)}}}
|
時相論理をチェックするにはどうすればよいか
さて、ここで次のような疑問が出てくるかもしれません。「なるほど、これらのすべてのことを記述 できるというのはすばらしい。しかし、記述していることが真実であることをチェックする方法がない。何の意味があるのだろうか?!」
私の答えは次のとおりです。これらのアサーションをチェックするツールがあります。ディジタル回路の場合、そのようなアサーションは、チップ作成の前に静的に確認されます。
ソフトウェアの場合、そのようなアサーションを静的に チェックできるということは大したことではないかもしれませんが、プログラムの特定の実行 (たとえば単体テスト中) においてこれらのアサーションが成立しているかどうかをチェックするための優れたツールがあります。そのようなアサーションを活用すれば、単体テストを一層有効に活用できます。1つの時相論理だけで、無数の従来型アサーションに匹敵することもあり得ます (従来型アサーションでそのアサーションを表現できる場合にはです)。
Time Rover Inc. の提供するTemporal Roverは、Javaプログラムの中の時相論理アサーションを処理し、そのアサーションに基づいて妥当なJavaコードを生成するためのツールです。(参考文献を参照。) 同社は、データベース・テーブルに対して使用するツール、DBRoverも提供しています。
Temporal Roverには、時相演算子がすべて含まれており、さらに過去に発生したイベントについて記述するための演算子も含まれています。DBRoverでは、データベース内のさまざまな値についてのアサーションの限量化も可能です。残念ながら、これらのツールは無料ではありませんが、30日間のトライアル版が用意されています。
JUnitにおけるアサーションのように、Temporal Rover/DBRoverのアサーションを使用すると、アサーションが成立しない場合に診断メッセージが出力されるよう設定できます。実際、Temporal Roverアサーションの構文は、上記の例と同じであり、様相演算子のオペランドとなるアサーションを中括弧で囲みます。それらのアサーションは、次の構文でTRAssert (Tmporal Rover Assert) 関数に渡されます。
/* TRAssert{<assertion> => <output string>}
|
<output string> は、アサーションが成立していない場合に表示される文字ストリングです。このような構文により、TRAssert のステートメントを有効なJavaプログラムの中に埋め込んでも、Temporal Roverなしでプログラムをコンパイルできます (もちろん、Temporal Roverなしでコンパイルすると、アサーションは無効になります)。
結論
以上のような時相論理アサーションを活用すれば、単体テストを一層有効に活用できます。1つの時相論理だけで、多数の従来型アサーションに匹敵することもあり得ます。そのようなわけで、これらのアサーションの強力な機能を活用すれば、このコラムでこれまで扱ってきた古典的なバグ・パターンの多くを一掃することができます。
次回の記事では、いくつかのバグ・パターンを時相論理アサーションのコンテキストでもう一度検討し、それらのアサーションを使用してそのようなパターンが発生しないようにする方法を示します。
参考文献
著者について  | | | Eric Allen氏は、コーネル大学でコンピューター・サイエンスと数学の学士号を取得しています。現在は、ライス大学の博士課程の大学院生としてJavaプログラミング言語チームに加わっています。学位を終了するためにライス大学に戻るまでは、Cycorp, IncでJavaソフトウェア開発主任として勤務していました。彼は、JavaWorldで「Java Beginner」ディスカッション・フォーラムの司会者も務めています。主な研究対象は、Java言語のセマンティック・モデルと静的分析ツールの開発であり、いずれもソース・レベルとバイトコード・レベルで研究しています。Ericは、NextGenというプログラミング言語 (汎用ランタイム型によるJava言語の拡張版) のためのライスのコンパイラーの開発にも携わってきました。連絡先は、eallen@cs.rice.edu です。 |
記事の評価
| 
