類型安全

在電腦科學中，一部分程式語言具備類型安全的性質。這個術語在不同的社群中有不同的定義，特別是正規的類型理論上的定義遠遠強過大多數的程式員的理解，但對於使用類型系統的認知，皆旨在避免必然的錯誤形式，和不良的程式行為（稱為類型錯誤）。

類型安全可以靜態方式實施，及早在編譯時期就捕捉到潛藏的錯誤；或者以動態方式，在執行時期關聯類型的資訊，並在必要時檢測即將發生的錯誤。類型安全是程式語言的性質，而不是程式所自有的。例如，有可能以類型不安全的語言，編寫出類型安全的程式。在此是以程式語言為主，而不討論以個人能力維護的類型安全。

某個行為之所以會被程式語言歸類為類型錯誤，通常是因為試圖對不適當類型的值進行運算。其分類的基本原則是︰部分語言設計者和程式員的看法認為，如果所有運算不引起程式瓦解、安全上的瑕疵、或其它明顯故障，即為合理的，而不視之為一個錯誤；其他人則認為所有違背程式員意圖的，就是錯誤的，而且應該標上「不安全」。在靜態類型系統中，類型安全通常包含一個保證，所有表達式最終的值都是合理的靜態類型成員（比子類型和多態性所要求的還要更加精確細微）。

類型安全近似於所謂的記憶體安全（就是限制從記憶體的某處，將任意的位元組合複製到另一處的能力）。例如，某個語言的實作具有若干類型 t，假如存在若干適當長度的位元，且其不為 t 的正統成員。若該語言允許把那些資料複製到 t 類型的變數，那個語言就不是類型安全的，因為這些運算可將非 t 類型的值賦給該變數。反過來說，若該語言類型不安全的程度，最高只到允許將任意整數用作為指標，顯然它就不是記憶體安全的。

大部分的靜態類型語言，都提供了一定程度的類型安全，而且其嚴格性更勝於記憶體的安全性。因其類型系統強迫程式員以適當的抽象資料類型定義來使用，即使對記憶體安全或任何可能的災難而言，並不需如此嚴格的要求。

[编辑] 定義

Robin Milner 對於類型安全所喊出的口號︰

「具備良好類型的程式從不出錯。」

適當的形式化口號，取決於特定語言主要語義的風格。在符號語義學裡，類型安全意謂者一個表達式的值具有良好類型τ，且是一個與τ相一致的真誠成員。

1994年，Andrew Wright 和 Matthias Felleisen 以運算語義學定義的公式描述︰何謂現今的標準定義，以及對於類型安全的檢驗技術。根據上述方法，類型安全是以程式語言語義中的兩個性質所決定的︰

藏存性

程式中的良好類型這一性質，即使轉換了語言的法則（即，評價法則或約簡法則），也不會有所改變。

進行性

具備良好類型的程式從不卡住，即從不進入一個使其無法進一步轉換的未知狀態。

這些性質不是無中生有的，而是和程式語言所描述出來的語義相連繫，而且各式各樣的語言存在著可以此基準來充實的廣大的空間。因為「類型良好」程式的概念已是靜態語義學的一部分，而「卡住」（或者「搞錯」）則是動態語義學方面的屬性。

[编辑] 語言的類型安全性

學術研究用途的玩具語言，常會提出類型安全方面的需求。另一方面，許多語言以人工方式所產生的類型安全，證實經常需要上千次的檢查。不過，某些語言，如標準ML，其嚴格定義了語義，且 Java 也已提供類型安全^{[來源請求]} 。其它語言如 Haskell 也被認為是類型安全。暫且不理會語言定義的性質，在執行時期發生的某些錯誤，應歸於實作時的缺陷，或是用了其它語言撰寫的程式庫；這種錯誤可能使給定的實作，在某些情況下的類型不再安全。

[编辑] 類型安全語言的記憶體管理

要實現完善的類型安全語言，它至少需要垃圾回收或增加記憶體配置和解配置的限制（本節主要針對前者）。更明確地說，不允許懸置指標橫跨不同結構類型的存在。這有一技術上的原因︰假定類型語言（如Pascal要求分配的記憶體必須顯式釋放）。如果存在一個仍舊指向之前的記憶體位址的懸置指標，新的資料結構可能會分配到同一空間。例如，如果初始化一個指向整數區域資料結構的指標，但新物件的指標區域卻分配在整數的地方，然後指標區域可藉由改變整數區域的值簡單改變成任可東西（經由間接引用懸置指標）。因為當指標改變時，尚未指定將會發生什麼，所以這個語言就不是類型安全的。大部分類型安全的語言滿足使用垃圾回收實現記憶體的管理。

在允許指標算術的語言中，實作垃圾回收器是最好的，所以在類型不安全的語言或類型安全可能失效的語言中，如此實作回收器的程式庫是最好的。C 和 C++ 經常使用。

[编辑] 類型安全與強類型

在各種強類型的定義中，其往往成為類型安全的同義詞；然而，類型安全與動態類型並不互相排斥。也可將動態類型視為非常寬鬆的靜態類型語言，而且所有語法正確的程式皆具備良好類型；只要它的動態語義學能夠保證絕不會有程式「搞錯」，它就可以滿足上述定義，且可稱為類型安全。

[编辑] 在各個語言中的類型安全問題

[编辑] Ada

Ada was designed to be suitable for embedded systems, device drivers and other forms of system programming, but also to encourage type safe programming. To resolve these conflicting goals, Ada confines type-unsafety to a certain set of special constructs whose names usually begin with the string "Unchecked_". Unchecked_Deallocation can be effectively banned from a unit of Ada text by applying pragma Pure to this unit. It is expected that programmers will use "Unchecked_" constructs very carefully and only when necessary; programs that do not use them are type safe.

The SPARK programming language is a subset of Ada eliminating all its potential ambiguities and insecurities while at the same time adding statically checked contracts to the language features available. SPARK avoids the issues with dangling pointers by disallowing allocation at run time entirely.

[编辑] C

在Wikibooks Programming有更多關於本條目的內容：

C

The poster child of type-unsafe languages. While the language definition explicitly calls out the fact that behavior of 'type-unsafe' conversions is not defined, most implementations perform conversions that programmers find useful. The widespread use of C language idioms that make use of conversions has helped give it a reputation for being a type-unsafe language (the same kind of conversions can be performed in Ada using unchecked conversions, however this usage is much less common than in C).

[编辑] 標準 ML

在Wikibooks Programming有更多關於本條目的內容：

ML

SML has a rigorously defined semantics and is known to be type safe. However, some implementations of SML, including Standard ML of New Jersey (SML/NJ) and Mlton, provide libraries that offer certain unsafe operations. These facilities are often used in conjunction with those implementations' foreign function interfaces to interact with non-ML code (such as C libraries) that may require data laid out in specific ways. Another example is the SML/NJ interactive toplevel itself, which must use unsafe operations to execute ML code entered by the user.

[编辑] Pascal

在Wikibooks Programming有更多關於本條目的內容：

Pascal

Pascal has had a number of type safety requirements, some of which are kept in some compilers. Where a Pascal compiler dictates "strict typing", two variables cannot be assigned to each other unless they are either compatible (such as conversion of integer to real) or assigned to the identical subtype. For example, if you have the following code fragment:

TYPE TwoTypes: 
    I:Integer;      
    Q:Real;    
END;             

TYPE DualTypes:
    I:Integer;
    Q:Real;
END;

VAR TT:TwoTypes;
    DT:DualTypes;
    TT1:TwoTypes;
    DT1:DualTypes;

Under strict typing, a variable defined as TwoTypes is not compatible with DualTypes (because they are not identical, even though the components of that user defined type are identical) and an assignment of TT := DT; is illegal. An assignment of TT := TT1; would be legal because the subtypes they are defined to are identical. However, an assignment such as TT.Q := DT.Q; would be legal.

[编辑] 參閱

• 資料類型
• 類型理論

[编辑] 參考資料

• Benjamin C. Pierce, Types and Programming Languages, MIT Press, 2002. (ISBN 0-262-16209-1) [1]
• Type Safe defined in the Portland Pattern Repository's Wiki [2]
• Andrew K. Wright and Matthias Felleisen, "A Syntactic Approach to Type Soundness," Information and Computation 115(1), pp. 38-94, 1994. [3]
• Stavros Macrakis, "Safety and power", ACM SIGSOFT Software Engineering Notes 7:2:25 (April 1982)requires subscription