| dbpprop: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 operations on values that are not of the appropriate data type. 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 explicit intent (as communicated via typing annotations) to be erroneous and not "type safe. " 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 <math>t</math>, such that some sequence of bits (of the appropriate length) does not represent a legitimate member of <math>t</math>, if that language allows data to be copied into a variable of type <math>t</math>, then it is not type safe because such an operation might assign a non-<math>t</math> 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.
- 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 Gleitkommavariablen 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 und solche in denen Typprüfungen primär zur Laufzeit stattfinden. 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.
- 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.
- 在電腦科學中，一部分程式語言具備型別安全的性質。這個術語在不同的社群中有不同的定義，特別是正規的型別理論上的定義遠遠強過大多數的程式員的理解，但對於使用型別系統的認知，皆旨在避免必然的錯誤形式，和不良的程式行為（稱為型別錯誤）。 中國大陸用語習慣稱型別為类型；稱資料為数据。 型別安全可以靜態方式實施，及早在編譯時期就捕捉到潛藏的錯誤；或者以動態方式，在執行時期關聯型別的資訊，並在必要時檢測即將發生的錯誤。型別安全是程式語言的性質，而不是程式所自有的。例如，有可能以型別不安全的語言，編寫出型別安全的程式。在此是以程式語言為主，而不討論以個人能力維護的型別安全。 某個行為之所以會被程式語言歸類為型別錯誤，通常是因為試圖對不適當型別的值進行運算。其分類的基本原則是：部分語言設計者和程式員的看法認為，如果所有運算不引起程式瓦解、安全上的瑕疵、或其它明顯故障，即為合理的，而不視之為一個錯誤；其他人則認為所有違背程式員意圖的，就是錯誤的，而且應該標上「不安全」。在靜態型別系統中，型別安全通常包含一個保證，所有運算式最終的值都是合理的靜態型別成員（比子型別和多態性所要求的還要更加精確細微）。 型別安全近似於所謂的記憶體安全（就是限制從記憶體的某處，將任意的位元組合複製到另一處的能力）。例如，某個語言的實作具有若干型別 <math>t</math>，假如存在若干適當長度的位元，且其不為 <math>t</math> 的正統成員。若該語言允許把那些資料複製到 <math>t</math> 型別的變數，那個語言就不是型別安全的，因為這些運算可將非 <math>t</math> 型別的值指派給該變數。反過來說，若該語言型別不安全的程度，最高只到允許將任意整數用作為指標，顯然它就不是記憶體安全的。 大部分的靜態型別語言，都提供了一定程度的型別安全，而且其嚴格性更勝於記憶體的安全性。因其型別系統強迫程式員以適當的抽象資料型別定義來使用，即使對記憶體安全或任何可能的災難而言，並不需如此嚴格的要求。
|
![[RDF Data]](/statics/sw-cube.png)
