| p:abstract
| - In computer science, type safety is a property of some programming languages that is defined differently by different communities, but most definitions involve the use of a type system to prevent certain erroneous or undesirable program behavior (called type errors). The formal type-theoretic definition is considerably stronger than what is understood by most programmers.
The enforcement can be static, catching potential errors at compile time, or dynamic, associating type information with values at run time and consulting them as needed to detect imminent errors, or a combination of both. Type safety is a property of the programming language, not of the programs themselves. For example, it is possible to write a safe program in a type-unsafe language.
The behaviors classified as type errors by a given programming language are usually those that result from attempts to perform an operation on some values, that is not appropriate to their data types. This classification is partly based on opinion: some language designers and programmers argue that any operation not leading to program crashes, security flaws or other obvious failures is legitimate and need not be considered an error, while others consider any contravention of the programmer's intent (as communicated via typing annotations) to be erroneous and deserving of the label "unsafe".
In the context of static type systems, type safety usually involves (among other things) a guarantee that the eventual value of any expression will be a legitimate member of that expression's static type. The precise requirement is more subtle than this — see, for example, subtype and polymorphism for complications.
Type safety is closely linked to memory safety, a restriction on the ability to copy arbitrary bit patterns from one memory location to another. For instance, in an implementation of a language that has some type t, such that some sequence of bits (of the appropriate length) does not represent a legitimate member of t, if that language allows data to be copied into a variable of type t, then it is not type safe because such an operation might assign a non-t value to that variable. Conversely, if the language is type unsafe to the extent of allowing an arbitrary integer to be used as a pointer, then it is clearly not memory safe.
Most statically-typed languages provide a degree of type safety that is strictly stronger than memory safety, because their type systems enforce the proper use of abstract data types defined by programmers even when this is not strictly necessary for memory safety or for the prevention of any kind of catastrophic failure. (en)
- Typsicherheit bezeichnet den Zustand (einer Programmausführung), bei dem die Datentypen gemäß ihren Definitionen in der benutzten Programmiersprache verwendet werden und keine Typverletzungen auftreten. Werden dementsprechend Typfehler spätestens zur Laufzeit erkannt, spricht man von „typsicheren Sprachen“. Typsicherheit herzustellen ist Aufgabe des Compilers bzw. Interpreters.
Als Typprüfung (englisch type checking) bezeichnet man dabei den Vorgang, die Verwendung von Datentypen innerhalb des Typsystems zu prüfen, um etwaige Typverletzungen festzustellen. Hierbei müssen beispielsweise bei Zuweisungen die beteiligten Typen nicht notwendig identisch sein, da ganze Zahlen unter Umständen Fließkommavariablen zugewiesen werden können. Einige Programmiersprachen machen eine strikte Typprüfung dadurch unmöglich, dass der Ergebnistyp eines Operators oder einer Funktion nicht eindeutig festgelegt ist, wie zum Beispiel beim Divisions-Operator in der Programmiersprache C oder beim Überladen von Operatoren in der objektorientierten Programmierung.
Bei den typisierten Sprachen gibt es solche mit Typprüfungen während der Kompilierung (statisch typisiert) und solche in denen Typprüfungen primär zur Laufzeit stattfinden (dynamisch typisiert). Oft wird fälschlicherweise die statische Typprüfung wegen des angenommenen qualitativen Vorteils gegenüber der dynamischen Typprüfung als „sicher“ bezeichnet.
Es kann keine allgemeine Aussage über die Tauglichkeit beider Formen der Typprüfung getroffen werden – bei statischer Typprüfung ist der Programmierer versucht, diese zu umgehen, beziehungsweise sie wird erst gar nicht vollständig durchgesetzt (zum jetzigen Stand der Technik muss es in jeder statischen Sprache eine Möglichkeit geben, „typlose“ Daten zu erzeugen oder zwischen Typen zu wechseln – etwa wenn Daten vom Massenspeicher gelesen werden), in Sprachen mit dynamischer Typprüfung werden manche Typfehler erst gefunden, wenn es zu spät ist. Bei dynamischer Typprüfung wird jedoch der Programmcode meist sehr viel einfacher. (de)
- Dans les langages à typage statique, l'un des objectifs est d'intercepter les erreurs de type à la compilation.
Un type peut être vu comme un ensemble de valeurs et un ensemble d'opérateurs. (fr)
- 在電腦科學中，一部分程式語言具備類型安全的性質。這個術語在不同的社群中有不同的定義，特別是正規的類型理論上的定義遠遠強過大多數的程式員的理解，但對於使用類型系統的認知，皆旨在避免必然的錯誤形式，和不良的程式行為（稱為類型錯誤）。
類型安全可以靜態方式實施，及早在編譯時期就捕捉到潛藏的錯誤；或者以動態方式，在執行時期關聯類型的資訊，並在必要時檢測即將發生的錯誤。類型安全是程式語言的性質，而不是程式所自有的。例如，有可能以類型不安全的語言，編寫出類型安全的程式。在此是以程式語言為主，而不討論以個人能力維護的類型安全。
某個行為之所以會被程式語言歸類為類型錯誤，通常是因為試圖對不適當類型的值進行運算。其分類的基本原則是：部分語言設計者和程式員的看法認為，如果所有運算不引起程式瓦解、安全上的瑕疵、或其它明顯故障，即為合理的，而不視之為一個錯誤；其他人則認為所有違背程式員意圖的，就是錯誤的，而且應該標上「不安全」。在靜態類型系統中，類型安全通常包含一個保證，所有表達式最終的值都是合理的靜態類型成員（比子類型和多態性所要求的還要更加精確細微）。
類型安全近似於所謂的記憶體安全（就是限制從記憶體的某處，將任意的位元組合複製到另一處的能力）。例如，某個語言的實作具有若干類型 t，假如存在若干適當長度的位元，且其不為 t 的正統成員。若該語言允許把那些資料複製到 t 類型的變數，那個語言就不是類型安全的，因為這些運算可將非 t 類型的值賦給該變數。反過來說，若該語言類型不安全的程度，最高只到允許將任意整數用作為指標，顯然它就不是記憶體安全的。
大部分的靜態類型語言，都提供了一定程度的類型安全，而且其嚴格性更勝於記憶體的安全性。因其類型系統強迫程式員以適當的抽象資料類型定義來使用，即使對記憶體安全或任何可能的災難而言，並不需如此嚴格的要求。 (zh)
|
![[RDF Data]](http://dbpedia.org/statics/sw-cube.png)
