類型安全
维基百科,自由的百科全书
在電腦科學中,一部分程式語言具備類型安全的性質。這個術語在不同的社群中有不同的定義,特別是正規的類型理論上的定義遠遠強過大多數的程式員的理解,但對於使用類型系統的認知,皆旨在避免必然的錯誤形式,和不良的程式行為(稱為類型錯誤)。
類型安全可以靜態方式實施,及早在編譯時期就捕捉到潛藏的錯誤;或者以動態方式,在執行時期關聯類型的資訊,並在必要時檢測即將發生的錯誤。類型安全是程式語言的性質,而不是程式所自有的。例如,有可能以類型不安全的語言,編寫出類型安全的程式。在此是以程式語言為主,而不討論以個人能力維護的類型安全。
某個行為之所以會被程式語言歸類為類型錯誤,通常是因為試圖對不適當類型的值進行運算。其分類的基本原則是:部分語言設計者和程式員的看法認為,如果所有運算不引起程式瓦解、安全上的瑕疵、或其它明顯故障,即為合理的,而不視之為一個錯誤;其他人則認為所有違背程式員意圖的,就是錯誤的,而且應該標上「不安全」。在靜態類型系統中,類型安全通常包含一個保證,所有表達式最終的值都是合理的靜態類型成員(比子類型和多態性所要求的還要更加精確細微)。
類型安全近似於所謂的記憶體安全(就是限制從記憶體的某處,將任意的位元組合複製到另一處的能力)。例如,某個語言的實作具有若干類型 t,假如存在若干適當長度的位元,且其不為 t 的正統成員。若該語言允許把那些資料複製到 t 類型的變數,那個語言就不是類型安全的,因為這些運算可將非 t 類型的值賦給該變數。反過來說,若該語言類型不安全的程度,最高只到允許將任意整數用作為指標,顯然它就不是記憶體安全的。
大部分的靜態類型語言,都提供了一定程度的類型安全,而且其嚴格性更勝於記憶體的安全性。因其類型系統強迫程式員以適當的抽象資料類型定義來使用,即使對記憶體安全或任何可能的災難而言,並不需如此嚴格的要求。
目录 |
[编辑] 定義
Robin Milner 對於類型安全所喊出的口號:
- 「具備良好類型的程式從不出錯。」
適當的形式化口號,取決於特定語言主要語義的風格。在符號語義學裡,類型安全意謂者一個表達式的值具有良好類型τ,且是一個與τ相一致的真誠成員。
1994年,Andrew Wright 和 Matthias Felleisen 以運算語義學定義的公式描述:何謂現今的標準定義,以及對於類型安全的檢驗技術。根據上述方法,類型安全是以程式語言語義中的兩個性質所決定的:
- 藏存性
- 程式中的良好類型這一性質,即使轉換了語言的法則(即,評價法則或約簡法則),也不會有所改變。
- 進行性
- 具備良好類型的程式從不卡住,即從不進入一個使其無法進一步轉換的未知狀態。
這些性質不是無中生有的,而是和程式語言所描述出來的語義相連繫,而且各式各樣的語言存在著可以此基準來充實的廣大的空間。因為「類型良好」程式的概念已是靜態語義學的一部分,而「卡住」(或者「搞錯」)則是動態語義學方面的屬性。
[编辑] 語言的類型安全性
學術研究用途的玩具語言,常會提出類型安全方面的需求。另一方面,許多語言以人工方式所產生的類型安全,證實經常需要上千次的檢查。不過,某些語言,如標準ML,其嚴格定義了語義,且 Java 也已提供類型安全[來源請求]。其它語言如 Haskell 也被認為是類型安全。暫且不理會語言定義的性質,在執行時期發生的某些錯誤,應歸於實作時的缺陷,或是用了其它語言撰寫的程式庫;這種錯誤可能使給定的實作,在某些情況下的類型不再安全。
[编辑] 類型安全語言的記憶體管理
要實現完善的類型安全語言,它至少需要垃圾回收或增加記憶體配置和解配置的限制(本節主要針對前者)。更明確地說,不允許懸置指標橫跨不同結構類型的存在。這有一技術上的原因:假定類型語言(如Pascal要求分配的記憶體必須顯式釋放)。如果存在一個仍舊指向之前的記憶體位址的懸置指標,新的資料結構可能會分配到同一空間。例如,如果初始化一個指向整數區域資料結構的指標,但新物件的指標區域卻分配在整數的地方,然後指標區域可藉由改變整數區域的值簡單改變成任可東西(經由間接引用懸置指標)。因為當指標改變時,尚未指定將會發生什麼,所以這個語言就不是類型安全的。大部分類型安全的語言滿足使用垃圾回收實現記憶體的管理。
在允許指標算術的語言中,實作垃圾回收器是最好的,所以在類型不安全的語言或類型安全可能失效的語言中,如此實作回收器的程式庫是最好的。C 和 C++ 經常使用。
[编辑] 類型安全與強類型
在各種強類型的定義中,其往往成為類型安全的同義詞;然而,類型安全與動態類型並不互相排斥。也可將動態類型視為非常寬鬆的靜態類型語言,而且所有語法正確的程式皆具備良好類型;只要它的動態語義學能夠保證絕不會有程式「搞錯」,它就可以滿足上述定義,且可稱為類型安全。
[编辑] 參閱
[编辑] 參考資料
- 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

