型安全性

コンピュータサイエンスにおいて、型安全性とは、プログラミング言語が型エラーをどの程度抑制または防止するかを指します。型安全言語は、強い型付け言語や厳密な型付け言語とも呼ばれます。特定のプログラミング言語によって型エラーとして分類される動作は、通常、適切なデータ型ではない値に対して演算を実行しようとした際に発生します。例えば、整数に文字列を加算しようとするなどです。

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

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

定義

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

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

言い換えれば、型システムが健全であれば、その型システムが受け入れる式は適切な型の値に評価されなければなりません（無関係な別の型の値を生成したり、型エラーでクラッシュしたりするのではなく）。Vijay Saraswatは、関連する以下の定義を提供しています。

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

しかし、プログラムが「適切に型付けされている」、あるいは「うまく動作しない」とは、厳密には、各プログラミング言語に固有の静的および動的意味論の特性によって決まります。したがって、型の健全性の正確かつ形式的な定義は、言語を規定するために使用される形式意味論のスタイルに依存します。1994年、アンドリュー・ライトとマティアス・フェライゼンは、操作的意味論によって定義される言語における型安全性の標準的な定義と証明手法を定式化しました。[ 4 ]これは、ほとんどのプログラマが理解する型安全性の概念に最も近いものです。このアプローチによれば、言語の意味論が型健全であるとみなされるためには、次の2つの特性を備えている必要があります。

進捗
適切に型付けされたプログラムは決して「スタック」しません。すべての式は既に値であるか、何らかの明確に定義された方法で値に還元できるかのいずれかです。言い換えれば、プログラムがそれ以上の遷移が不可能な未定義状態に陥ることはありません。
保存（または主題の縮小）
各評価ステップの後、各式の型は同じままです（つまり、その型は保存されます）。

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

他の形態の安全性との関係

型の健全性は、それ自体では比較的弱い特性です。なぜなら、本質的には型システムのルールが内部的に一貫しており、変更不可能であることを述べているに過ぎないからです。しかし、実際には、プログラミング言語は、型付けの適切さが他のより強い特性も伴うように設計されています。その一部を以下に示します。

型安全言語と型安全でない言語

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

強い型付けと弱い型付け

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

メモリ管理と型安全性

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

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

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

オブジェクト指向言語における型安全性

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

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

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

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

特定の言語における型安全性の問題

エイダ

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

Adaは、組み込みシステム、デバイスドライバ、その他のシステムプログラミングに適した設計であると同時に、型安全プログラミングを促進するようにも設計されています。これらの相反する目的を解決するため、Adaは型安全でない要素を、通常Unchecked_という文字列で始まる特定の特殊な要素に限定しています。Unchecked_Deallocationは、この要素にPureプラグマを適用することで、Adaテキストの特定のユニットから効果的に排除できます。プログラマーはUnchecked_要素を非常に慎重に、そして必要な場合にのみ使用することが期待されます。Unchecked_要素を使用しないプログラムは型安全です。

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

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

C

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

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++の機能:

C#

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

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

ジャワ

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

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

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

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

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

標準ML

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

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

モジュラ2

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規格では、型キャスト機能に関してこの問題が修正され、型キャスト構文がCASTという関数に変更されました。この関数は擬似モジュールSYSTEMからインポートする必要があります。しかし、バリアントレコードなどの他の安全でない機能は、擬似モジュール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 Revision 2010での型キャスト* )FROM UNSAFE IMPORT FFI ; (* 外部関数インターフェース機能の識別子を有効にする *) <*FFI="C"*> (* C への外部関数インターフェースのプラグマ *)

パスカル

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

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

type TwoTypes =レコード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++の例

以下の例は、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

参照

注記

  1. ^ 「型システムについて議論する前に知っておくべきこと | Ovid [blogs.perl.org]」 . blogs.perl.org . 2023年6月27日閲覧。
  2. ^ a bミルナー、ロビン（1978）、「プログラミングにおける型多態性理論」、コンピュータとシステム科学ジャーナル、17（3）：348– 375、doi：10.1016/0022-0000（78）90014-4、hdl：20.500.11820/d16745d7-f113-44f0-a7a3-687c2b709f66
  3. ^ a b Saraswat, Vijay (1997-08-15). 「Javaは型安全ではない」 . 2008年10月8日閲覧。
  4. ^ Wright, AK; Felleisen, M. (1994年11月15日). 「型の健全性に対する統語的アプローチ」 . Information and Computation . 115 (1): 38–94 . doi : 10.1006/inco.1994.1093 . ISSN 0890-5401 . 
  5. ^ルイス・ダマス、ロビン・ミルナー（1982年1月25日）「関数型プログラムのための主要な型スキーム」。第9回ACM SIGPLAN-SIGACTシンポジウム「プログラミング言語の原理 - POPL '82」の議事録。ACM（計算機協会）  207～ 212頁。doi：10.1145/582153.582176。ISBN 0897910656. S2CID  11319320 .
  6. ^ Tofte, Mads (1988).操作的意味論と多態的型推論（論文）.
  7. ^ Henriksen, Troels; Elsman, Martin (2021年6月17日). 「配列プログラミングにおけるサイズ依存型に向けて」 .第7回ACM SIGPLAN国際ワークショップ「配列プログラミングのためのライブラリ、言語、コンパイラ」議事録. Association for Computing Machinery. pp.  1– 14. doi : 10.1145/3460944.3464310 . ISBN 9781450384667. S2CID  235474098 .
  8. ^ Standard ML . Smlnj.org. 2013年11月2日閲覧。
  9. ^ "System.IO.Unsafe" . GHCライブラリマニュアル: base-3.0.1.0 . 2008年7月5日時点のオリジナルよりアーカイブ。2008年7月17日閲覧。
  10. ^ Liskov, B; Zilles, S (1974). 「抽象データ型を使ったプログラミング」. ACM SIGPLAN Notices . 9 (4): 50– 59. CiteSeerX 10.1.1.136.3043 . doi : 10.1145/942572.807045 . 
  11. ^ Jackson, K. (1977). 「並列処理とモジュール型ソフトウェア構築」.プログラミング言語の設計と実装. コンピュータサイエンス講義ノート. 第54巻. pp.  436– 443. doi : 10.1007/BFb0021435 . ISBN 3-540-08360-X。
  12. ^ 「CS1130. オブジェクト指向プログラミングへの移行 - 2012年春 - 自習版」コーネル大学コンピュータサイエンス学部 2005年. 2023年9月15日閲覧。
  13. ^ピアス、ベンジャミン・C. (2002). 『型とプログラミング言語』 マサチューセッツ州ケンブリッジ: MITプレス. p. 158. ISBN 0-262-16209-1。
  14. ^型安全性は、適切なクラス定義の問題でもある。オブジェクトの内部状態を変更するパブリックメソッドは、オブジェクトの完全性を維持する必要がある。
  15. ^カーニハン、デニス・M・リッチー（ 1988年3月）『プログラミング言語C』（第2版）ニュージャージー州エングルウッド・クリフス：プレンティス・ホール、 116ページ 。ISBN 978-0-13-110362-7C では、malloc が void へのポインタを返すことを宣言し、次にキャストを使用してポインタを明示的に目的の型に強制変換するのが適切な方法です。
  16. ^ニクラス・ヴィルト (1985)。Modula-2 でのプログラミング。スプリンガー・フェルラーグ。
  17. ^ a b「安全な施設と安全でない施設の分離」 。 2015年3月24日閲覧。
  18. ^ "ISO Modula-2 言語リファレンス" . 2015 年3 月 24 日に取得。
  19. ^ 「Common Lisp HyperSpec」 . 2013年5月26日閲覧。
  20. ^ "reinterpret_cast 変換 - cppreference.com" . En.cppreference.com . 2022年9月21日閲覧。
  21. ^ "dynamic_cast 変換 - cppreference.com" . En.cppreference.com . 2022年9月21日閲覧。

参考文献

「 https://en.wikipedia.org/w/index.php?title=Type_safety&oldid=1319864588」から取得