Loading article…
コンピュータサイエンスにおいて、型安全性とは、プログラミング言語が型エラーをどの程度抑制または防止するかを示すものです。型安全な言語は、厳密型付け言語または強型付け言語とも呼ばれます。特定のプログラミング言語で型エラーとして分類される動作は、通常、適切なデータ型ではない値に対して演算を実行しようとした結果生じるものです。例えば、文字列を整数に加算しようとする場合などです。
型の強制は、静的（コンパイル時に潜在的なエラーを検出する）、動的（実行時に型情報を値に関連付け、必要に応じて参照して差し迫ったエラーを検出する）、またはその両方の組み合わせのいずれかになります。[ 1 ]動的な型の強制は、静的な強制では無効となるプログラムを実行できる場合が多いですが、実行時にエラーが発生するという代償があります。
静的（コンパイル時）型システムの文脈では、型安全性は通常、（とりわけ）任意の式の最終的な値がその式の静的型の正当なメンバーであることを保証することを意味します。正確な要件はこれよりも複雑で、例えばサブタイピングやポリモーフィズムの項を参照してください。
直感的に言えば、型の健全性はロビン・ミルナーの簡潔な言葉に表されている。
言い換えれば、型システムが健全であれば、その型システムによって受け入れられる式は、適切な型の値に評価されるはずです（他の無関係な型の値が生成されたり、型エラーでクラッシュしたりすることはありません）。Vijay Saraswat は、関連する定義を次のように示しています。
しかし、プログラムが「型付けが適切」であることや「誤動作」することが具体的に何を意味するかは、その静的および動的意味論の特性であり、これは各プログラミング言語に固有のものです。したがって、型の健全性の正確な形式的定義は、言語を指定するために使用される形式意味論のスタイルに依存します。1994年、Andrew WrightとMatthias Felleisenは、操作的意味論で定義された言語における型安全性の標準的な定義と証明手法となったものを定式化しました[ 4 ]。これは、ほとんどのプログラマが理解している型安全性の概念に最も近いものです。このアプローチでは、言語の意味論が型健全であるとみなされるには、次の2つの特性を備えている必要があります。
型健全性に関する他の形式的な扱いも、指示的意味論と構造的操作的意味論の観点から発表されている。[ 2 ] [ 5 ] [ 6 ]
型健全性は、型システムの規則が内部的に一貫しており、覆すことができないということを意味するだけなので、単独では比較的弱い特性です。しかし実際には、プログラミング言語は、型が適切であることに加えて、以下のようなより強力な特性も含むように設計されています。
3 / "Hello, World"ため、式を無効として拒否することができます。型安全性は、学術的なプログラミング言語研究で提案されるおもちゃの言語（つまり、難解な言語）の要件であることが多い。しかし、多くの言語は、何千ものケースをチェックする必要があるため、人間が生成する型安全性の証明には大きすぎる。それにもかかわらず、厳密に定義された意味論を持つStandard MLなどの言語は、型安全性の定義の 1 つを満たすことが証明されている。 [ 8 ] Haskellなどの他の言語は、特定の「エスケープ」機能が使用されない限り、型安全性の定義を満たすと考えられている（たとえば、入出力（I/O）が可能な通常の制限された環境から「エスケープ」するために使用されるHaskell のunsafePerformIO は、型システムを回避し、型安全性を破るために使用できる。[ 9 ]）。型パンニングは、そのような「エスケープ」機能のもう 1 つの例である。言語定義の特性に関係なく、実装のバグ、または他の言語で書かれたリンクされたライブラリのバグにより、実行時に特定のエラーが発生する可能性がある。このようなエラーは、特定の状況下では特定の実装タイプを安全でないものにする可能性があります。SunのJava仮想マシンの初期バージョンは、この種の問題に対して脆弱でした。[ 3 ]
プログラミング言語は、型安全性の特定の側面を指すために、しばしば口語的に、強い型付けまたは弱い型付け（または緩い型付け）に分類されます。1974 年、リスコフとジレスは、強い型付け言語を「呼び出し関数から呼び出される関数にオブジェクトが渡されるときはいつでも、その型は呼び出される関数で宣言された型と互換性がなければならない」言語と定義しました。[ 10 ] 1977 年、ジャクソンは、「強い型付け言語では、各データ領域は明確な型を持ち、各プロセスはこれらの型に関して通信要件を記述する」と書いています。[ 11 ] 対照的に、弱い型付け言語は予測不可能な結果を生成したり、暗黙的な型変換を実行したりする可能性があります。[ 12 ]
型安全性はメモリ安全性と密接に関連しています。たとえば、ある型を持つ言語の実装ではこれは一部のビットパターンは許可するが、他のビットパターンは許可しない。ダングリングポインタメモリエラーにより、正当なメンバーを表していないビットパターンを書き込むことができる。デッド変数型へ変数を読み取る際に型エラーが発生する。逆に、メモリセーフな言語では、任意の整数をポインタとして使用することはできないため、別途ポインタ型または参照型を用意する必要がある。
型安全な言語の最低限の条件として、異なる型のメモリ割り当て間でダングリングポインタが存在しないことが求められます。しかし、ほとんどの言語では、メモリの安全性や致命的な障害の防止に必ずしも必要ではない場合でも、プログラマが定義した抽象データ型の適切な使用が強制されます。メモリ割り当てには、その内容を記述する型が割り当てられ、この型は割り当て期間中固定されます。これにより、型に基づくエイリアス解析によって、異なる型のメモリ割り当てが別個のものであると推論できます。
ほとんどの型安全な言語はガベージコレクションを使用します。ピアースは、ダングリングポインタ問題のため、「明示的な解放操作が存在する場合、型安全性を実現することは非常に難しい」と述べています。[ 13 ]しかし、Rustは一般的に型安全であると考えられており、ガベージコレクションの代わりに借用チェッカーを使用してメモリ安全性を実現しています。
オブジェクト指向言語では、型安全性は通常、型システムが存在するという事実に内在するものです。これはクラス定義によって表現されます。
クラスは基本的に、そこから派生するオブジェクトの構造を定義し、APIはこれらのオブジェクトを扱うための契約として機能します。新しいオブジェクトが作成されるたびに、そのオブジェクトはその契約に準拠します。
特定のクラスから派生したオブジェクト、または特定のインターフェースを実装するオブジェクトを交換する各関数は、その契約に従います。したがって、その関数では、そのオブジェクトに対して許可される操作は、そのオブジェクトが実装するクラスのメソッドによって定義されたものだけになります。これにより、オブジェクトの整合性が維持されることが保証されます。[ 14 ]
この例外としては、オブジェクト構造の動的な変更を可能にするオブジェクト指向言語や、リフレクションを使用してオブジェクトの内容を変更し、クラスメソッドの定義によって課される制約を克服する方法などが挙げられる。
Adaは、組み込みシステム、デバイスドライバ、その他のシステムプログラミングに適した設計であると同時に、型安全なプログラミングを促進することも目的としています。これらの相反する目標を解決するために、Adaは型安全性を損なう可能性のある特定の特殊構造に限定しており、これらの構造の名前は通常「Unchecked_ 」で始まります。「Unchecked_Deallocation」は、Adaテキストの単位に「pragma Pure」を適用することで、その単位から効果的に排除できます。プログラマは「Unchecked_」構造を非常に慎重に、必要な場合にのみ使用することが期待されており、これらを使用しないプログラムは型安全です。
SPARKプログラミング言語は、Adaのサブセットであり、Adaの潜在的な曖昧さやセキュリティ上の脆弱性をすべて排除しつつ、静的に検証された契約を言語機能に追加しています。SPARKは、実行時におけるメモリ割り当てを完全に禁止することで、ダングリングポインタの問題を回避しています。
Ada2012では、言語自体に静的にチェックされる契約（事前条件、事後条件、および型不変条件の形式）が追加されます。
C言語は、限られたコンテキストでは型安全です。たとえば、明示的なキャストを使用しない限り、ある型の構造体へのポインタを別の型の構造体へのポインタに変換しようとすると、コンパイル時エラーが発生します。しかし、非常に一般的な操作の多くは型安全ではありません。たとえば、整数を出力する通常の方法は、 のようになります。printf("%d", 12)ここで、 は実行時に整数引数を期待するように%d指示します。（ のように、関数に文字列へのポインタを期待するように指示しながら整数引数を提供するような場合、コンパイラは受け入れるかもしれませんが、未定義の結果を生成します。）これは、一部のコンパイラ（gccなど）がprintf引数とフォーマット文字列間の型対応をチェックすることで部分的に軽減されます。printfprintf("%s", 12)
さらに、C は Ada と同様に、明示的変換が未指定または未定義ですが、Ada とは異なり、これらの変換を使用するイディオムが非常に一般的であり、C が型安全でないという評判を得るのに役立っています。たとえば、ヒープにメモリを割り当てる標準的な方法は、malloc必要なバイト数を示す引数とともに、などのメモリ割り当て関数を呼び出すことです。この関数はvoid ポインタ( void*) を返しますが、呼び出し元のコードはこれを適切なポインタ型に明示的または暗黙的にキャストする必要があります。標準化前の C の実装では、これを行うために明示的なキャストが必要だったため、ある の割り当てに対してstruct Foo、コードが受け入れられた慣行となりました。[ 15 ]は を返しますが、これは C では明示的にキャストする必要はありませんが、C++ では型安全性のためにこのキャストが必須となっています。Foo* foo = (struct Foo*)malloc(sizeof(struct Foo))malloc()void*
C++は一般的に、前身のCよりも型安全性が高く、ポインタ型からvoid*別のポインタ型への暗黙的なキャストを許可しない[ 16 ]などの機能や、次のような機能があります。
dynamic_castポインタと参照の間で実行時に型チェックを行うなど、static_castより安全な型変換演算子があります。一方、コンパイル時に型変換される型の間でチェックを行う演算子は、一般的にCスタイルの型変換よりも安全です。 enum class) は、整数型や他の列挙型との間で暗黙的に変換することはできません。C#は型安全です。型指定のないポインタもサポートしていますが、これにはコンパイラレベルで禁止できる「unsafe」キーワードを使用する必要があります。実行時キャスト検証は標準でサポートされています。キャストは、「as」キーワードを使用して検証できます。「as」キーワードを使用すると、キャストが無効な場合は null 参照が返されます。また、C スタイルのキャストを使用すると、キャストが無効な場合は例外がスローされます。C シャープ変換演算子を参照してください。
オブジェクト型（他のすべての型がそこから派生する型）に過度に依存すると、C# の型システムの目的が損なわれる恐れがあります。通常は、オブジェクト参照を放棄し、C++ のテンプレートやJava のジェネリクスと同様のジェネリクスを使用する方がより良い方法です。
Java言語は型安全性を強制するように設計されています。Javaではすべての処理がオブジェクト内で行われ、各オブジェクトはクラス のインスタンスです。
型安全性を確保するためには、各オブジェクトは使用前に割り当てられる必要があります。Javaではプリミティブ型の使用が許可されていますが、それは適切に割り当てられたオブジェクト内でのみ可能です。
型安全性の一部は間接的に実装される場合もあります。例えば、BigDecimal クラスは任意精度の浮動小数点数を表しますが、有限表現で表せる数値のみを扱います。BigDecimal.divide() 操作は、BigDecimal で表された 2 つの数値の除算として新しいオブジェクトを計算します。
この場合、例えば 1/3 = 0.33333... のように除算に有限表現がない場合、演算に丸めモードが定義されていないと divide() メソッドは例外を発生させる可能性があります。したがって、クラス定義に暗黙的に含まれる契約をオブジェクトが遵守することは、言語ではなくライブラリによって保証されます。
標準MLは厳密に定義されたセマンティクスを持ち、型安全であることが知られています。しかし、Standard ML of New Jersey (SML/NJ)、その構文バリアントであるMythryl、およびMLtonなどの一部の実装では、安全でない操作を提供するライブラリが用意されています。これらの機能は、特定の形式でデータを配置する必要がある非MLコード（Cライブラリなど）とやり取りするために、これらの実装の外部関数インターフェースと組み合わせて使用されることがよくあります。もう1つの例は、SML/NJの対話型トップレベル自体です。これは、ユーザーが入力したMLコードを実行するために、安全でない操作を使用する必要があります。
Modula-2 は、安全でない機能はすべて明示的に安全でないとマークする必要があるという設計思想を持つ、強力な型付け言語です。これは、そのような機能を SYSTEM と呼ばれる組み込みの擬似ライブラリに「移動」することで実現され、使用するにはそこからインポートする必要があります。このようにインポートすると、そのような機能が使用されるときにそれが見えるようになります。残念ながら、これは元の言語レポートとその実装では実装されませんでした。[ 17 ]型キャスト構文やバリアントレコード (Pascal から継承) など、事前のインポートなしで使用できる安全でない機能がまだ残っていました。[ 18 ]これらの機能を 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 からインポートしなくても引き続き使用可能でした。[ 19 ]
IMPORT SYSTEM ; VAR i : INTEGER ; n : CARDINAL ; i := SYSTEM . CAST ( INTEGER , n ); (* ISO Modula-2 での型キャスト *)最近の言語改訂では、元の設計思想が厳密に適用されました。まず、擬似モジュール SYSTEM は UNSAFE に名前が変更され、そこからインポートされる機能の安全性の低さがより明確になりました。次に、残りのすべての安全性の低い機能は、完全に削除されるか (たとえばバリアント レコード)、擬似モジュール UNSAFE に移動されました。インポートできる識別子がない機能については、有効化識別子が導入されました。このような機能を有効にするには、対応する有効化識別子を擬似モジュール UNSAFE からインポートする必要があります。UNSAFE からのインポートを必要としない安全性の低い機能は、この言語には残っていません。[ 18 ]
IMPORT UNSAFE ; VAR i : INTEGER ; n : CARDINAL ; i := UNSAFE . CAST ( INTEGER , n ); (* Modula-2 Revision 2010 での型キャスト *)FROM UNSAFE IMPORT FFI ; (* 外部関数インターフェース機能の有効化識別子 *) <*FFI="C"*> (* C への外部関数インターフェースのプラグマ *)Pascalには多くの型安全性の要件があり、その一部は一部のコンパイラで維持されています。Pascalコンパイラが「厳密な型付け」を規定している場合、2つの変数は、互換性がある（整数から実数への変換など）か、同一のサブタイプに割り当てられている場合を除き、互いに代入することはできません。たとえば、次のコード断片があるとします。
type TwoTypes = record I : Integer ; Q : Real ; end ;DualTypes = record I : Integer ; Q : Real ; end ;var T1 , T2 : TwoTypes ; D1 , D2 : DualTypes ;厳密な型付けでは、 TwoTypesとして定義された変数はDualTypesと互換性がありません(ユーザー定義型の構成要素は同じでも、両者は同一ではないため) 。そのため、への代入は不正です。への代入は、それらが定義されているサブタイプが同一であるため、合法です。ただし、のような代入は合法です。T1 := D2;T1 := T2;T1.Q := D1.Q;
一般的に、Common Lispは型安全な言語です。Common Lisp コンパイラは、静的に型安全性を証明できない操作に対して動的なチェックを挿入する責任があります。ただし、プログラマは、より低いレベルの動的型チェックでプログラムをコンパイルするように指定することができます。[ 20 ]このようなモードでコンパイルされたプログラムは、型安全とはみなされません。
以下の例は、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コンパイラが整数から浮動小数点値への安全な変換を実行することを明示的に阻止しています。[ 21 ]プログラムを実行すると、ゴミのような浮動小数点値が出力されます。この問題は、代わりに次のように記述することで回避できたはずです。float fval = ival;
次の例は、オブジェクト参照が誤ってダウンキャストされる例を示しています。
#include <iostream> using namespace std ;class Parent { public : virtual ~ Parent () {} // RTTI 用の仮想デストラクタ};class Child1 : public Parent { public : int a ; };class 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ですdynamic_cast。[ 22 ]
がへのポインタを返すこと
を宣言し、キャストを使用してポインタを目的の型に明示的に強制することです。mallocvoid