型状態分析

型状態分析は、プロトコル分析とも呼ばれ、プログラミング言語で使用されるプログラム分析の形式です。これは、オブジェクト指向言語に最も一般的に適用されます。型状態は、特定の型のインスタンスに対して実行できる有効な操作シーケンスを定義します。型状態は、その名前が示すように、状態情報をその型の変数に関連付けます。この状態情報は、コンパイル時に、その型のインスタンスに対して呼び出すのに有効な操作を決定するために使用されます。通常は実行時にのみ実行されるオブジェクトに対する操作は、オブジェクトの新しい状態と互換性があるように変更された型状態情報に対して実行されます。

型状態は、「メソッドA はメソッドBを呼び出す前に呼び出す必要があり、メソッドC はその間に呼び出すことはできない」などの動作の型の詳細化を表すことができます。型状態は、ファイルを開いた状態のままにしておくなどの無効なシーケンスではなく、「開いてから閉じる」などの意味的に有効なシーケンスを強制することで、オープン/クローズ セマンティクスを使用するリソースを表すのに適しています。このようなリソースには、ファイル システム要素、トランザクション、接続、プロトコルが含まれます。たとえば、開発者は、ファイルまたはソケットを読み取りまたは書き込みの前に開く必要があり、閉じた場合は読み取りまたは書き込みができないように指定することができます。「型状態」という名前は、この種の分析では各タイプのオブジェクトを有限状態マシンとしてモデル化することが多いという事実に由来しています。この状態マシンでは、各状態には許可されたメソッド/メッセージの明確に定義されたセットがあり、メソッドの呼び出しによって状態遷移が発生する可能性があります。ペトリ ネットは、詳細化型で使用するための可能な動作モデルとしても提案されています。^[1]

型状態分析は、1983年にロブ・ストロムによってIBMワトソン研究所 で開発されたネットワーク実装言語（NIL）で導入されました^[2]。これは、ストロムとイエミニによって1986年の論文^[3]で形式化 され、型状態を使用して変数の初期化の程度を追跡し、不適切に初期化されたデータに操作が適用されないことを保証する方法が説明され、さらにヘルメスプログラミング言語で一般化されました。

近年、様々な研究により、型状態の概念をオブジェクト指向言語に適用する方法が開発されている。^{[4] [5]}

Strom と Yemini (1986) は、特定の型の型状態のセットが部分的に順序付けられ、一部の情報を破棄することで、より低い型状態をより高い型状態から取得できることを要求しました。たとえば、Cintの変数は通常、型状態「初期化されていない」<「初期化済み」を持ち、ポインターは型状態「割り当てられていない」<「割り当てられているが初期化されていない」<「初期化されているが、ファイルが開かれていない」< 「ファイルが開かれている」を持つ場合があります。さらに、Strom と Yemini は、2 つの型状態それぞれに最大の下限があること、つまり部分順序がmeet-semilatticeであること、および各順序には常に「⊥」と呼ばれる最小の要素があることを要求しています。 FILE*

彼らの分析は、各変数vにはプログラム テキスト内の各ポイントに対して 1 つの型状態のみが割り当てられるという単純化に基づいています。ポイントpに 2 つの異なる実行パスが到達し、v が各パスを介して異なる型状態を継承する場合、 pでのvの型状態は、継承された型状態の最大下限とみなされます。たとえば、次の C スニペットでは、変数は、と (空の)部分からそれぞれ型状態「initialized」と「uninitialized 」を継承するため、条件文全体の後には型状態「uninitialized」になります。 nthenelse

int n ; // ここで、n の型状態は "uninitialized" ですif (...) { n = 5 ; // ここで、n の型状態は "initialized" です} else { /*何もしない*/ // ここで、n の型状態は "uninitialized" です} // ここで、n の型状態は "uninitialized" です = greatest_lower_bound("initialized","uninitialized")                 
  
                  
  
        
                     

すべての基本操作^{[注 1]には、}型状態遷移、つまり各パラメータに対する操作前と操作後の必須型状態と保証型状態がそれぞれ備わっている必要があります。たとえば、操作には「ファイルが開かれたfwrite(...,fd)」という型状態が必要です。より正確には、操作には複数の結果があり、それぞれに独自の型状態遷移が必要です。たとえば、C コードは、開く操作が成功した場合と失敗した場合に、の型状態をそれぞれ「ファイルが開かれた」と「未割り当て」に設定します。 fdFILE *fd=fopen("foo","r")fd

2 つの型状態t ₁ <· t ₂ごとに、一意の型状態強制操作を提供する必要があります。この操作は、型状態t ₂のオブジェクトに適用されると、おそらくリソースの一部を解放することによって、その型状態をt ₁に縮小します。たとえば、の型状態を「ファイルが開かれている」から「初期化されているが、ファイルが開かれていない」にfclose(fd)強制します。 fd

プログラム実行がtypestate-correctであると言われるのは、

• 各基本操作の前に、すべてのパラメータは操作の型状態遷移に必要な型状態を正確に持ち、
• プログラム終了時には、すべての変数は型状態⊥になります。^{[注 2]}

プログラム テキストは、適切な型状態強制を追加することで、制御フローによって許可されるパスが型状態が正しいように、ポイントを型状態で静的にラベル付けできるプログラムに変換できる場合、型状態一貫性があると呼ばれます。Strom と Yemini は、指定されたプログラム テキストの型状態一貫性をチェックし、どの強制操作を挿入するかを計算する 線形時間アルゴリズムを提供します。

正確で効果的な型状態分析を実現するには、エイリアシングの問題に対処する必要があります。エイリアシングは、オブジェクトに複数の参照またはポインターが指し示す場合に発生します。分析が正確であるためには、特定のオブジェクトの状態変更がそのオブジェクトを指すすべての参照に反映される必要がありますが、一般に、そのような参照をすべて追跡することは困難な問題です。分析をモジュール化する必要がある場合、つまり、プログラムの残りの部分を考慮せずに大規模なプログラムの各部分に個別に適用する必要がある場合は、特に困難になります。

別の問題として、一部のプログラムでは、収束する実行パスで最大の下限値を取り、対応するダウン強制演算を追加する方法は不十分であるように思われます。たとえば、return 1次のプログラムでは、^{[注 3]}の前に、 、のすべてのコンポーネントx、y、が初期化されますが、Strom と Yemini のアプローチではこれを認識しておらず、ループ本体内の構造体コンポーネントの各初期化は、ループの再エントリ時に、最初のループエントリの型状態、つまり ⊥ を満たすようにダウン強制される必要があります。関連する問題は、この例では型状態遷移のオーバーロードが必要になることです。たとえば、 は型状態「コンポーネントが初期化されていません」を「 x コンポーネントが初期化されています」に変更しますが、「y コンポーネントが初期化されています」を「 x および y コンポーネントが初期化されています」にも変更します。 zcoordparse_int_attr("x",&coord->x)

int parse_coord ( struct { int x ; int y ; int z ; } * coord ) { int seen = 0 ; /* どの属性が解析されたかを記憶する */           
            

    while ( 1 ) if ( parse_int_attr ( "x" , & coord -> x )) seen |= 1 ; else if ( parse_int_attr ( "y" , & coord -> y )) seen |= 2 ; else if ( parse_int_attr ( "z" , & coord -> z )) seen |= 4 ; else break ; 
                  
              
              
         

    if ( seen != 7 ) /* いくつかの属性が欠落しているため失敗 */ return 0 ; ... /* すべての属性が存在するため、いくつかの計算を実行して成功 */ return 1 ; }       
         
                   
     

プログラム（または契約などの他の成果物）から型状態を推論しようとするアプローチはいくつかあります。その多くはコンパイル時に型状態を推論することができます^{[6] [7] [8] [9]}そして他のものはモデルを動的にマイニングします。^{[10] [11] [12] [13] [14] [15]}

型状態は実験的な概念であり、主流のプログラミング言語にはまだ導入されていない。しかし、多くの学術プロジェクトでは、日常的なプログラミング技術としてより有用なものにする方法を積極的に研究している。その例としては、カーネギーメロン大学のジョナサン・アルドリッチのグループが開発しているPlaid言語とObsidian言語が挙げられる。^{[16] [17]}その他の例としては、Clara ^{[18]言語研究フレームワーク、} Rust言語 の初期バージョン、ATS>>のキーワードなどがある。^[19]

• 状態パターン
• 契約による設計
• 線形型システム
• エフェクトシステム
• 実行時検証