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