タイプステート分析


Typestate_analysis
タイプステート分析は、プロトコル分析と呼ばれることもあり、プログラミング言語で使用されるプログラム分析の形式です。これは、オブジェクト指向言語に最も一般的に適用されます。タイプステートは、特定のタイプのインスタンスに対して実行できる操作の有効なシーケンスを定義します。タイプステートは、その名前が示すように、状態情報をそのタイプの変数に関連付けます。この状態情報は、コンパイル時に、その型のインスタンスで呼び出されるのに有効な操作を判別するために使用されます。通常は実行時にのみ実行されるオブジェクトに対して実行される操作は、オブジェクトの新しい状態と互換性があるように変更されたタイプ状態情報に対して実行されます。
タイプステートは、「メソッドBを呼び出す前にメソッドAを呼び出す必要があり、その間にメソッドCを呼び出すことはできません」などの動作タイプの改良を表すことができます。タイプステートは、ファイルを開いた状態のままにするなどの無効なシーケンスとは対照的に、「開いてから閉じる」などの意味的に有効なシーケンスを適用することにより、開く/閉じるセマンティクスを使用するリソースを表すのに適しています。このようなリソースには、ファイルシステム要素、トランザクション、接続、およびプロトコルが含まれます。たとえば、開発者は、ファイルまたはソケットを読み取りまたは書き込みの前に開く必要があり、閉じていると読み取りまたは書き込みができないように指定したい場合が「typestate」という名前は、この種の分析が各タイプのオブジェクトを有限状態マシンとしてモデル化することが多いという事実に由来しています。このステートマシンでは、各状態に許可されたメソッド/メッセージの明確なセットがあり、メソッドの呼び出しによって状態遷移が発生する可能性がペトリネットは、改良タイプで使用するための可能な動作モデルとしても提案されています。
タイプステート分析は、1983年にRob Stromによって、IBMのWatsonLabで開発されたNetworkImplementation Language(NIL)で導入されました。1986年の記事で、StromとYeminiによって形式化され、typestateを使用して変数の初期化の程度を追跡し、不適切に初期化されたデータに操作が適用されないことを保証し、Hermesプログラミング言語でさらに一般化されました。
近年、さまざまな研究により、タイプステートの概念をオブジェクト指向言語に適用する方法が開発されています。

コンテンツ
1 アプローチ
2 課題
3 タイプステート推論
4 typestateをサポートする言語
5 も参照してください
6 ノート
7 参考文献

アプローチ
image"
  タイプの変数の初期化から生じる非線形タイプステートラティス
struct{int x;int y;int z;}。
最小要素⊥は、構造体コンポーネントが初期化されていない状態∅と一致します。
Strom and Yemini(1986)は、特定のタイプのタイプステートのセットを部分的に順序付けて、一部の情報を破棄することにより、高いタイプステートから低いタイプステートを取得できるようにすることを要求しました。例えば、int可変Cは、典型的には、「typestatesを有する初期化されていない<」「初期化」、およびFILE*ポインタは「typestatesを有していてもよい未割り当て」<「割り当てが、初期化されていない」<「に初期化するが、ファイルが開かれていない」<「ファイルを開きます」 。さらに、StromとYeminiは、2つのタイプステートのそれぞれに最大の下限があることを要求します。つまり、半順序が半束でさえあることを要求します。そして、各注文には常に「⊥」と呼ばれる最小の要素が
それらの分析は、各変数vにプログラムテキストの各ポイントに対して1つのタイプステートのみが割り当てられるという単純化に基づいています。2つの異なる実行パスがポイントpに到達し、vが各パスを介して異なるタイプステートを継承する場合、pでのvのタイプステートは、継承されたタイプステートの最大の下限と見なされます。例えば、以下のC断片において、変数はtypestateを継承し、「初期化」および「初期化されていないから」と(空の)部分はそれぞれ、したがってそれはtypestate「が初期化されていないが、全条件文の後に」。nthenelse
int n ; //ここで、nはtypestate “”uninitialized”” if (…){
n = 5 ; //ここで、nはtypestate “”initialized”” } else {
/ *何もしない* ///ここでnはtypestate “”uninitialized”” } //ここで、nはtypestate “”uninitialized”” = great_lower_bound( “”initialized””、 “”uninitialized””)
すべての基本操作には、タイプ状態遷移を装備する必要がつまり、各パラメーターについて、操作の前後にそれぞれ必要なタイプ状態と保証されたタイプ状態を備えている必要がたとえば、操作がfwrite(…,fd)必要ですfdtypestate「持っているファイル開くを」。より正確には、操作にはいくつかの結果があり、それぞれに独自の型状態遷移が必要です。例えば、CコードFILE *fd=fopen(“”foo””