型安全性

コンピュータサイエンスにおいて、型安全性と型の健全性は、プログラミング言語が型エラーを抑制または防止する程度です。型安全性は、コンピュータ言語の機能の特性であると見なされることもあります。つまり、一部の機能は型安全で、使用しても型エラーは発生しませんが、同じ言語の他の機能は型安全ではなく、それらを使用するプログラムで型エラーが発生する可能性があります。特定のプログラミング言語によって型エラーとして分類される動作は通常、適切なデータ型ではない値に対して操作を実行しようとした結果として生じるものです。たとえば、このケースの処理方法が定義されていない場合に文字列を整数に追加します。この分類は部分的に意見に基づいています。

型の強制は、静的（コンパイル時に潜在的なエラーをキャッチする）か、動的（実行時に型情報と値を関連付け、必要に応じてそれらを参照して差し迫ったエラーを検出する）、またはその両方の組み合わせのいずれかになります。^[1]動的な型の強制では、静的な強制では無効になるプログラムを実行できることがよくあります。

静的 (コンパイル時) 型システムのコンテキストでは、型の安全性には通常、(他の要素の中でも) 任意の式の最終的な値がその式の静的型の正当なメンバーになるという保証が含まれます。正確な要件はこれよりも微妙です。複雑さについては、たとえばサブタイプとポリモーフィズムを参照してください。

直感的に言えば、型の健全性はロビン・ミルナーの簡潔な発言 によって捉えられる。

適切に型付けされたプログラムは「間違い」を起こすことはありません。^[2]

言い換えれば、型システムが健全である場合、その型システムによって受け入れられる式は、適切な型の値に評価される必要があります (他の無関係な型の値を生成したり、型エラーでクラッシュしたりするのではなく)。Vijay Saraswat は、次の関連する定義を提供しています。

言語が型安全であるとは、その言語内のデータに対して実行できる操作が、データの型によって許可されている操作のみである場合を指します。^[3]

しかし、プログラムが「適切に型付けされている」または「うまくいかない」とは、それぞれのプログラミング言語に固有の静的および動的セマンティクスの特性によって正確には異なります。したがって、型の健全性の正確で形式的な定義は、言語を指定するために使用される形式セマンティクスのスタイルによって異なります。1994 年に、Andrew Wright とMatthias Felleisen は、操作的セマンティクス^[4]によって定義された言語における型の安全性の標準的な定義と証明手法を策定しました。これは、ほとんどのプログラマが理解している型の安全性の概念に最も近いものです。このアプローチでは、言語のセマンティクスが型の健全であるとみなされるためには、次の 2 つの特性が必要です。

進捗

適切に型付けされたプログラムは「行き詰まる」ことはありません。すべての式は、すでに値であるか、明確に定義された方法で値に縮小できます。言い換えると、プログラムは、それ以上の遷移が不可能な未定義の状態になることはありません。

保存（または主題の縮小）

各評価ステップの後、各式の型は同じままです（つまり、その型は保存されます）。

他にも、表示的意味論や構造的操作的意味論の観点から、型の健全性に関する形式的な研究が数多く発表されている。^{[2] [5] [6]}

型の健全性は、本質的には型システムのルールが内部的に一貫しており、破壊できないことを述べているだけなので、単独で見ると比較的弱い特性です。しかし、実際には、プログラミング言語は、型が適切であることが他のより強力な特性も伴うように設計されています。その一部を以下に示します。

• 不正な演算の防止。たとえば、3 / "Hello, World"除算演算子が文字列の 除数に対して定義されていないため、型システムは式を無効として拒否できます。
• メモリの安全性
  • 型システムは、ある型のオブジェクトへのポインターが別の型へのポインターとして扱われることによって発生する可能性のあるワイルドポインターを防ぐことができます。
  • 依存型をサポートするようなより洗練された型システムは、範囲外のアクセスを検出して拒否し、潜在的なバッファオーバーフローを防ぐことができます。^[7]
• 異なる型のセマンティクスに起因する論理エラー。たとえば、インチとミリメートルはどちらも整数として保存できますが、互いに置き換えたり、加算したりすることはできません。型システムでは、これらに対して 2 つの異なる整数型を強制できます。

型安全性は、通常、学術的なプログラミング言語の研究で提案されるあらゆるおもちゃの言語（つまり、難解な言語）の要件です。一方、多くの言語は、何千ものケースをチェックする必要があるため、人間が生成した型安全性の証明には大きすぎます。それでも、厳密に定義されたセマンティクスを持つStandard MLなどの言語は、型安全性の 1 つの定義を満たしていることが証明されています。 ^[8] Haskellなどの他の言語は、特定の「エスケープ」機能を使用しない限り、型安全性の定義を満たしていると考えられています^[議論]（たとえば、I/O が可能な通常の制限された環境から「エスケープ」するために使用される Haskell の unsafePerformIO は、型システムを回避し、型安全性を破るために使用できます。^[9]）。型パンニングは、そのような「エスケープ」機能の別の例です。言語定義の特性に関係なく、実装のバグ、または他の言語で記述されたリンクされたライブラリが原因で、実行時に特定のエラーが発生する可能性があります。このようなエラーは、特定の状況下では特定の実装型を安全でないものにしてしまう可能性がある。SunのJava仮想マシンの初期バージョンは、この種の問題に対して脆弱であった。^[3]

プログラミング言語は、型安全性の特定の側面を示すために、口語的に強く型付けされた言語と弱く型付けされた言語（緩く型付けされた言語）に分類されることが多い。1974 年、リスコフとジルズは強く型付けされた言語を「呼び出し関数から呼び出される関数にオブジェクトが渡されるときは常に、その型は呼び出される関数で宣言された型と互換性がなければならない」言語と定義した。^[10] 1977 年、ジャクソンは「強く型付けされた言語では、各データ領域に異なる型があり、各プロセスはこれらの型に基づいて通信要件を宣言する」と書いた。 [ ^11] これとは対照的に、弱く型付けされた言語は、予測できない結果を生成したり、暗黙の型変換を実行したりすることがあります。^[12]

型の安全性はメモリの安全性と密接に関連しています。たとえば、一部のビットパターンを許可し、他のビットパターンを許可しない型を持つ言語の実装では、ダングリング ポインタメモリ エラーによって、型の無効な変数にの正当なメンバーを表さないビットパターンを書き込むことができ、変数が読み取られるときに型エラーが発生します。逆に、言語がメモリ安全である場合、任意の整数をポインタとして使用することは許可されないため、別のポインタまたは参照型が必要になります。 ${\displaystyle t}$${\displaystyle t}$${\displaystyle t}$

最低限の条件として、型安全言語は異なる型の割り当て間でのぶら下がりポインタを許可してはなりません。しかし、ほとんどの言語では、メモリの安全性やあらゆる種類の壊滅的な障害の防止に厳密に必要でない場合でも、プログラマーが定義した抽象データ型の適切な使用を強制します。割り当てには、その内容を説明する型が与えられ、この型は割り当ての期間中固定されます。これにより、型ベースのエイリアス分析によって、異なる型の割り当てが別個であると推測できます。

型安全言語のほとんどはガベージコレクションを使用します。ピアスは、ダングリングポインタ問題のため、「明示的な割り当て解除操作がある場合、型安全を実現することは非常に困難です」と述べています。^[13]しかし、Rustは一般的に型安全であると考えられており、ガベージコレクションの代わりに借用チェッカーを使用してメモリの安全性を実現します。

オブジェクト指向言語では、型の安全性は通常、型システムが配置されているという事実に内在しています。これはクラス定義の観点で表現されます。

クラスは基本的に、そこから派生したオブジェクトの構造と、これらのオブジェクトを処理するための契約としてのAPIを定義します。新しいオブジェクトが作成されるたびに、その契約に 準拠することになります。

特定のクラスから派生したオブジェクトや特定のインターフェースを実装したオブジェクトを交換する各関数は、その契約に従います。したがって、その関数では、そのオブジェクトに対して許可される操作は、オブジェクトが実装するクラスのメソッドによって定義されたものだけになります。これにより、オブジェクトの整合性が保持されることが保証されます。^[14]

例外として、オブジェクト構造の動的な変更や、クラス メソッド定義によって課せられた制約を克服するためにリフレクションを使用してオブジェクトの内容を変更できるオブジェクト指向言語があります。

Wikibook Adaプログラミングには、型システムに関するページがあります。

Ada は、組み込みシステム、デバイス ドライバー、その他の形式のシステム プログラミングに適した設計になっていますが、型安全プログラミングも推奨しています。これらの相反する目的を解決するために、Ada では、型安全でない部分を、通常Unchecked_ という文字列で始まる名前の特定の特別な構造に制限しています。このユニットにプラグマ Pureを適用することで、Ada テキストのユニットから Unchecked_Deallocation を効果的に禁止できます。プログラマーは、 Unchecked_構造を非常に慎重に、必要な場合にのみ使用することが期待されます。Unchecked_ 構造を使用しないプログラムは型安全です。

SPARKプログラミング言語はAda のサブセットであり、その潜在的な曖昧さや不安定さをすべて排除すると同時に、利用可能な言語機能に静的にチェックされたコントラクトを追加します。SPARK は、実行時の割り当てを完全に禁止することで、 ダングリング ポインターの問題を回避します。

Ada2012 は、静的にチェックされた契約を言語自体に追加します (事前条件、事後条件、および型不変条件の形式で)。

WikibooksにはCプログラミングに関する本があります。

C プログラミング言語は、限られたコンテキストでのみ型安全です。たとえば、明示的なキャストを使用しない限り、ある型の構造体へのポインタを別の型の構造体へのポインタに変換しようとすると、コンパイル時エラーが生成されます。ただし、非常に一般的な操作の多くは型安全ではありません。たとえば、整数を出力する通常の方法は のようなものでprintf("%d", 12)、 は実行時に整数引数を期待するように%d指示します。(関数に文字列へのポインタを期待するように指示しながらも整数引数を提供する のようなものは、コンパイラーに受け入れられる場合もありますが、結果は未定義になります。)この問題は、一部のコンパイラー (gcc など) が printf 引数と書式文字列の型の対応をチェックすることで、部分的に緩和されます。 printfprintf("%s", 12)

さらに、C は Ada と同様に、未指定または未定義の明示的な変換を提供します。Ada とは異なり、これらの変換を使用するイディオムは非常に一般的であり、C が型安全でないという評判を得るのに役立っています。たとえば、ヒープにメモリを割り当てる標準的な方法は、malloc必要なバイト数を示す引数を指定して、 などのメモリ割り当て関数を呼び出すことです。この関数は型なしのポインタ (型void *) を返します。呼び出しコードは、このポインタを適切なポインタ型に明示的または暗黙的にキャストする必要があります。C の標準化前の実装では、これを行うには明示的なキャストが必要であったため、 というコードが一般的な方法になりました。^[15](struct foo *) malloc(sizeof(struct foo))

より型安全なコードを促進する C++ の機能の一部:

• new演算子はオペランドに基づいて型のポインターを返しますが、malloc はvoid ポインターを返します。
• C++ コードでは、仮想関数とテンプレートを使用して、void ポインターなしでポリモーフィズムを実現できます。
• 実行時の型チェックを実行する動的キャストなどの、より安全なキャスト演算子。
• C++11 の厳密に型指定された列挙型は、整数や他の列挙型との間で暗黙的に変換することはできません。
• C++ の明示的なコンストラクターと C++11 の明示的な変換演算子は、暗黙的な型変換を防止します。

C# はタイプセーフです。型指定されていないポインターをサポートしていますが、これはコンパイラ レベルで禁止できる "unsafe" キーワードを使用してアクセスする必要があります。実行時のキャスト検証が本質的にサポートされています。キャストは、キャストが無効な場合に null 参照を返す "as" キーワードを使用するか、キャストが無効な場合に例外をスローする C スタイルのキャストを使用して検証できます。C Sharp 変換演算子を参照してください。

オブジェクト型 (他のすべての型はここから派生します)に過度に依存すると、C# 型システムの目的が損なわれるリスクがあります。通常は、オブジェクト参照を放棄して、C++ のテンプレートや Java のジェネリックと同様に、ジェネリックを使用する方がよいでしょう。

WikibooksにはJavaプログラミングに関する本があります。

Java言語は、型の安全性を強化するように設計されています。Java ではすべてオブジェクト内で行われ、各オブジェクトはクラス のインスタンスです。

型安全性の強制を実装するには、各オブジェクトは使用前に割り当てておく必要があります。Java では、適切に割り当てられたオブジェクト内でのみ プリミティブ型を使用できます。

場合によっては、型の安全性の一部が間接的に実装されます。たとえば、BigDecimal クラスは任意の精度の浮動小数点数を表しますが、有限表現で表現できる数値のみを処理します。BigDecimal.divide() 操作は、BigDecimal として表現された 2 つの数値の除算として新しいオブジェクトを計算します。

この場合、たとえば 1/3=0.33333... を計算するときのように、除算に有限表現がない場合、divide() メソッドは、演算に丸めモードが定義されていないと例外を発生させる可能性があります。したがって、言語ではなくライブラリは、オブジェクトがクラス定義に暗黙的に含まれている契約を尊重することを保証します。

Wikibooksには、標準MLプログラミングに関する本があります。

標準 ML は厳密に定義されたセマンティクスを持ち、型安全であることが知られています。ただし、Standard ML of New Jersey (SML/NJ)、その構文バリアントである Mythryl、およびMLtonなどの一部の実装では、安全でない操作を提供するライブラリが提供されています。これらの機能は、多くの場合、特定の方法でレイアウトされたデータを必要とする可能性のある非 ML コード (C ライブラリなど) と対話するために、それらの実装の外部関数インターフェイスと組み合わせて使用​​されます。もう 1 つの例は、ユーザーが入力した ML コードを実行するために安全でない操作を使用する必要がある SML/NJ対話型トップレベル自体です。

Modula-2 は、安全でない機能は明示的に安全でないとマークする必要があるという設計思想を持つ、強く型付けされた言語です。これは、そのような機能を SYSTEM と呼ばれる組み込み疑似ライブラリに「移動」することで実現され、使用する前にそこからインポートする必要があります。インポートにより、そのような機能が使用されているときに表示されます。残念ながら、これは元の言語レポートとその実装では実装されていませんでした。^[16]型キャスト構文やバリアントレコード (Pascal から継承) など、事前のインポートなしで使用できる安全でない機能がまだ残っていました。^[17]これらの機能を SYSTEM 疑似モジュールに移動する際の難しさは、インポートできるのは識別子だけで、構文はインポートできないため、インポートできる機能の識別子がなかったことです。

IMPORT  SYSTEM ;  (* 特定の安全でない機能の使用を許可します: *) 
VAR  word  :  SYSTEM . WORD ;  addr  :  SYSTEM . ADDRESS ; 
addr  :=  SYSTEM . ADR ( word );

(* ただし、型キャスト構文はこのようなインポートなしでも使用できます *) 
VAR  i  :  INTEGER ;  n  :  CARDINAL ; 
n  :=  CARDINAL ( i );  (* または *)  i  :=  INTEGER ( n );

ISO Modula-2標準では、型キャスト構文を疑似モジュールSYSTEMからインポートする必要があるCASTという関数に変更することで、型キャスト機能の問題を修正しました。ただし、バリアントレコードなどの他の安全でない機能は、疑似モジュールSYSTEMからインポートしなくても引き続き使用可能でした。^[18]

IMPORT  SYSTEM ; 
VAR  i  :  INTEGER ;  n  :  CARDINAL ; 
i  :=  SYSTEM.CAST ( INTEGER , n ); ( * ISO Modula-2 での型キャスト* )  

最近の言語の改訂では、元の設計思想が厳密に適用されました。まず、疑似モジュール SYSTEM が UNSAFE に名前変更され、そこからインポートされた機能の安全でない性質がより明確になりました。次に、残りのすべての安全でない機能は完全に削除されるか (バリアント レコードなど)、疑似モジュール UNSAFE に移動されました。インポートできる識別子がない機能については、有効化識別子が導入されました。このような機能を有効にするには、対応する有効化識別子を疑似モジュール UNSAFE からインポートする必要があります。UNSAFE からのインポートを必要としない安全でない機能は、言語に残っていません。^[17]

IMPORT  UNSAFE ; 
VAR  i  :  INTEGER ;  n  :  CARDINAL ; 
i  : =  UNSAFE.CAST ( INTEGER , n ); ( * Modula-2 リビジョン 2010 での型キャスト *)  

FROM  UNSAFE  IMPORT  FFI ;  (* 外部関数インターフェース機能の識別子を有効にする *) 
<*FFI="C"*>  (* C への外部関数インターフェースのプラグマ *)

Wikibooksには、 Pascalプログラミングに関する本があります。

Pascal にはいくつかの型安全性要件があり、その一部は一部のコンパイラで維持されています。Pascal コンパイラが「厳密な型付け」を規定している場合、2 つの変数は、互換性があるか (整数から実数への変換など)、同一のサブタイプに割り当てられていない限り、互いに割り当てることはできません。たとえば、次のコード フラグメントがあるとします。

type 
TwoTypes = record I :整数; Q :実数;終了;    
      
      
  

  DualTypes =レコードI :整数; Q :実数;終了;  
     
     
  

var 
T1 、T2 : TwoTypes ; D1 、D2 : DualTypes ;     
     

厳密な型付けでは、 TwoTypesとして定義された変数はDualTypesと互換性がなく(ユーザー定義型のコンポーネントは同一ですが、同一ではないため)、 の割り当ては無効です。 の割り当ては、定義されているサブタイプが同一であるため有効です。ただし、 などの割り当ては有効です。 T1 := D2;T1 := T2;T1.Q := D1.Q;

一般的に、Common Lispは型安全言語です。Common Lispコンパイラは、型の安全性を静的に証明できない操作に対して動的チェックを挿入する役割を担っています。しかし、プログラマーは、プログラムをより低いレベルの動的型チェックでコンパイルするように指示する場合があります。^[19]このようなモードでコンパイルされたプログラムは、型安全とは見なされません。

次の例は、C++ キャスト演算子が誤って使用されると型の安全性が損なわれる可能性があることを示しています。最初の例は、基本データ型が誤ってキャストされる可能性があることを示しています。

#include <iostream> using namespace std ; 
  

int main () { int ival = 5 ; // 整数値float fval = reinterpret_cast < float &> ( ival ); // ビットパターンを再解釈cout << fval << endl ; // 整数を float として出力return 0 ; }   
                                       
        
                                
     

この例では、reinterpret_castコンパイラが整数から浮動小数点値への安全な変換を行うことを明示的に防いでいます。^[20]プログラムを実行すると、ゴミの浮動小数点値が出力されます。この問題は、代わりに次のように書くことで回避できます。float fval = ival;

次の例は、オブジェクト参照が誤ってダウンキャストされる可能性があることを示しています。

#include <iostream> using namespace std ; 
  

class Parent { public : virtual ~ Parent () {} // RTTI の仮想デストラクタ};  

       


クラスChild1 : public Parent { public : int a ; };     

     


クラスChild2 : public Parent { public : float b ; };     

     


int main () { Child1 c1 ; c1.a = 5 ; Parent & p = c1 ; // アップキャストは常に安全 Child2 & c2 = static_cast < Child2 & > ( p ) ; //ダウンキャストが無効cout << c2.b << endl ; //ゴミデータが出力されますreturn 0 ; }   
     
      
                             
         
                  
     

2 つの子クラスには異なる型のメンバーがあります。親クラスのポインタを子クラスのポインタにダウンキャストすると、結果のポインタが正しい型の有効なオブジェクトを指していない可能性があります。この例では、これによりゴミの値が出力されます。この問題は、無効なキャストで例外をスローする に置き換えることで回避できます。static_cast[ ^21]dynamic_cast

• 型理論

• ピアス、ベンジャミン C. (2002)。型とプログラミング言語。MIT プレス。ISBN 978-0-262-16209-8。
• 「タイプセーフ」。Portlandパターン リポジトリ Wiki。
• ライト、アンドリュー K.;マティアスフェライゼン(1994)。「型の健全性に対する統語的アプローチ」。情報と計算。115 (1): 38–94。doi : 10.1006/inco.1994.1093。
• Macrakis, Stavros (1982 年 4 月)。 「安全性と電力」。ACM SIGSOFT ソフトウェア エンジニアリング ノート。7 (2): 25–26。doi :10.1145/ 1005937.1005941。S2CID 10426644  。