В информатике безопасность типов и надежность типов — это степень, в которой язык программирования препятствует или предотвращает ошибки типов . Безопасность типов иногда также рассматривается как свойство средств языка программирования ; то есть некоторые средства являются безопасными по типу, и их использование не приведет к ошибкам типов, в то время как другие средства в том же языке могут быть небезопасными по типу, и программа, использующая их, может столкнуться с ошибками типов. Поведение, классифицируемое как ошибки типов данным языком программирования, обычно является результатом попыток выполнить операции над значениями , которые не имеют соответствующего типа данных , например, добавление строки к целому числу , когда нет определения того, как обрабатывать этот случай. Эта классификация частично основана на мнении.
Принудительное применение типов может быть статическим, выявляющим потенциальные ошибки во время компиляции , или динамическим, связывающим информацию о типах со значениями во время выполнения и обращающимся к ним по мере необходимости для обнаружения неизбежных ошибок, или комбинацией того и другого. [1] Динамическое принудительный подход к типам часто позволяет запускать программы, которые были бы недопустимы при статическом применении.
В контексте статических (компилируемых) систем типов безопасность типов обычно подразумевает (помимо прочего) гарантию того, что конечное значение любого выражения будет законным членом статического типа этого выражения. Точное требование более тонкое — см., например, подтипирование и полиморфизм для усложнений.
Интуитивно обоснованность типа отражена в кратком утверждении Робина Милнера о том, что
Другими словами, если система типов является надежной , то выражения, принимаемые этой системой типов, должны оцениваться как значение соответствующего типа (а не выдавать значение какого-то другого, не связанного типа или аварийно завершаться с ошибкой типа). Виджай Сарасват дает следующее связанное определение:
Однако, что именно означает для программы быть «хорошо типизированной» или «идти неправильно» — это свойства ее статической и динамической семантики , которые специфичны для каждого языка программирования. Следовательно, точное формальное определение корректности типа зависит от стиля формальной семантики, используемой для спецификации языка. В 1994 году Эндрю Райт и Маттиас Феллейзен сформулировали то, что стало стандартным определением и методом доказательства для безопасности типов в языках, определенных операционной семантикой , [4] , что наиболее близко к понятию безопасности типов, как его понимает большинство программистов. Согласно этому подходу, семантика языка должна иметь следующие два свойства, чтобы считаться корректной с точки зрения типа:
Также был опубликован ряд других формальных трактовок типовой обоснованности с точки зрения денотационной семантики и структурной операционной семантики . [2] [5] [6]
В изоляции надежность типа является относительно слабым свойством, поскольку по сути просто утверждает, что правила системы типов внутренне согласованы и не могут быть нарушены. Однако на практике языки программирования спроектированы так, что хорошая типизация также влечет за собой другие, более сильные свойства, некоторые из которых включают:
3 / "Hello, World" деления не определен для делителя строки . Типовая безопасность обычно является требованием для любого игрушечного языка (т. е. эзотерического языка ), предлагаемого в академических исследованиях языков программирования. С другой стороны, многие языки слишком велики для сгенерированных человеком доказательств типовой безопасности, поскольку они часто требуют проверки тысяч случаев. Тем не менее, было доказано, что некоторые языки, такие как Standard ML, который имеет строго определенную семантику, соответствуют одному определению типической безопасности. [8] Некоторые другие языки, такие как Haskell, считаются [ обсудить ] соответствующими некоторому определению типической безопасности , при условии, что не используются определенные возможности «выхода» (например, unsafePerformIO Haskell , используемый для «выхода» из обычной ограниченной среды, в которой возможен ввод-вывод, обходит систему типов и поэтому может использоваться для нарушения типической безопасности. [9] ) Каламбур типов является еще одним примером такой возможности «выхода». Независимо от свойств определения языка, некоторые ошибки могут возникать во время выполнения из-за ошибок в реализации или в связанных библиотеках, написанных на других языках; Такие ошибки могли сделать данный тип реализации небезопасным в определенных обстоятельствах. Ранняя версия виртуальной машины Java от Sun была уязвима к такого рода проблемам. [3]
Языки программирования часто в разговорной речи классифицируются как строго типизированные или слабо типизированные (также слабо типизированные) для обозначения определенных аспектов безопасности типов. В 1974 году Лисков и Зиллес определили строго типизированный язык как тот, в котором «всякий раз, когда объект передается из вызывающей функции в вызываемую функцию, его тип должен быть совместим с типом, объявленным в вызываемой функции». [10] В 1977 году Джексон писал: «В строго типизированном языке каждая область данных будет иметь отдельный тип, и каждый процесс будет указывать свои требования к коммуникации в терминах этих типов». [11] Напротив, слабо типизированный язык может давать непредсказуемые результаты или может выполнять неявное преобразование типов. [12]
Безопасность типов тесно связана с безопасностью памяти . Например, в реализации языка, который имеет некоторый тип , который допускает некоторые битовые комбинации, но не другие, ошибка памяти висячего указателя позволяет записать битовую комбинацию, которая не представляет собой законного члена, в мертвую переменную типа , вызывая ошибку типа при чтении переменной. И наоборот, если язык является безопасным для памяти, он не может разрешить использовать произвольное целое число в качестве указателя , поэтому должен быть отдельный указатель или ссылочный тип.
Как минимальное условие, типобезопасный язык не должен допускать висящих указателей между выделениями разных типов. Но большинство языков обеспечивают надлежащее использование абстрактных типов данных , определенных программистами, даже если это не является строго необходимым для безопасности памяти или для предотвращения любого вида катастрофического сбоя. Выделениям присваивается тип, описывающий их содержимое, и этот тип фиксируется на протяжении выделения. Это позволяет основанному на типах анализу псевдонимов делать вывод о том, что выделения разных типов различны.
Большинство языков с безопасной типизацией используют сборку мусора . Пирс говорит, что «чрезвычайно сложно достичь безопасности типов при наличии явной операции освобождения» из-за проблемы с висячими указателями. [13] Однако Rust обычно считается безопасным типом и использует проверку заимствований для достижения безопасности памяти вместо сборки мусора.
В объектно-ориентированных языках безопасность типов обычно является неотъемлемой частью факта наличия системы типов . Это выражается в терминах определений классов.
Класс по сути определяет структуру объектов, полученных из него, а API — как контракт для обработки этих объектов. Каждый раз, когда создается новый объект, он будет соответствовать этому контракту.
Каждая функция, которая обменивается объектами, полученными из определенного класса, или реализует определенный интерфейс , будет придерживаться этого контракта: следовательно, в этой функции разрешенные для этого объекта операции будут только теми, которые определены методами класса, реализуемого объектом. Это гарантирует сохранение целостности объекта. [14]
Исключением являются объектно-ориентированные языки, которые допускают динамическую модификацию структуры объекта или использование рефлексии для изменения содержимого объекта с целью преодоления ограничений, налагаемых определениями методов класса.
Ada была разработана для того, чтобы подходить для встроенных систем , драйверов устройств и других форм системного программирования , но также и для поощрения типобезопасного программирования. Чтобы разрешить эти противоречивые цели, Ada ограничивает типобезопасность определенным набором специальных конструкций, имена которых обычно начинаются со строки Unchecked_ . Unchecked_Deallocation можно эффективно запретить в единице текста Ada, применив pragma Pure к этой единице. Ожидается, что программисты будут использовать конструкции Unchecked_ очень осторожно и только при необходимости; программы, которые их не используют, являются типобезопасными.
Язык программирования SPARK является подмножеством Ada, устраняющим все его потенциальные двусмысленности и небезопасности, в то же время добавляя статически проверяемые контракты к доступным языковым возможностям. SPARK избегает проблем с висячими указателями , полностью запрещая выделение во время выполнения.
Ada2012 добавляет статически проверяемые контракты в сам язык (в форме пред- и постусловий, а также инвариантов типов).
Язык программирования C является типобезопасным в ограниченных контекстах; например, ошибка времени компиляции генерируется при попытке преобразовать указатель на один тип структуры в указатель на другой тип структуры, если только не используется явное приведение типов. Однако ряд очень распространенных операций не являются типобезопасными; например, обычный способ печати целого числа — это что-то вроде printf("%d", 12), где во время выполнения %dуказывает ожидать целочисленный аргумент. (Что-то вроде , которое указывает функции ожидать указатель на строку символов и при этом предоставляет целочисленный аргумент, может быть принято компиляторами, но даст неопределенные результаты.) Это частично смягчается некоторыми компиляторами (например, gcc), проверяющими соответствия типов между аргументами printf и строками формата.printfprintf("%s", 12)
Кроме того, C, как и Ada, предоставляет неуказанные или неопределенные явные преобразования; и в отличие от Ada, идиомы, которые используют эти преобразования, очень распространены и помогли придать C репутацию небезопасного по типу. Например, стандартный способ выделения памяти в куче — это вызвать функцию выделения памяти, такую как malloc, с аргументом, указывающим, сколько байт требуется. Функция возвращает нетипизированный указатель (тип void *), который вызывающий код должен явно или неявно привести к соответствующему типу указателя. Предварительно стандартизированные реализации C требовали явного приведения для этого, поэтому код стал общепринятой практикой. [15](struct foo *) malloc(sizeof(struct foo))
Некоторые особенности C++, способствующие созданию более безопасного с точки зрения типов кода:
C# является типобезопасным. Он поддерживает нетипизированные указатели, но для этого необходимо использовать ключевое слово "unsafe", которое можно запретить на уровне компилятора. Он имеет встроенную поддержку проверки приведения во время выполнения. Приведения можно проверить с помощью ключевого слова "as", которое вернет нулевую ссылку, если приведение недействительно, или с помощью приведения в стиле C, которое выдаст исключение, если приведение недействительно. См. Операторы преобразования C Sharp .
Неоправданная зависимость от типа объекта (из которого выводятся все остальные типы) рискует свести на нет цель системы типов C#. Обычно лучше отказаться от ссылок на объекты в пользу generics , аналогично шаблонам в C++ и generics в Java .
Язык Java разработан для обеспечения безопасности типов. Все, что происходит в Java, происходит внутри объекта , а каждый объект является экземпляром класса .
Для реализации обеспечения безопасности типов каждый объект перед использованием должен быть выделен . Java допускает использование примитивных типов , но только внутри правильно выделенных объектов.
Иногда часть безопасности типов реализуется косвенно: например, класс BigDecimal представляет число с плавающей точкой произвольной точности, но обрабатывает только числа, которые могут быть выражены конечным представлением. Операция BigDecimal.divide() вычисляет новый объект как деление двух чисел, выраженных как BigDecimal.
В этом случае, если деление не имеет конечного представления, как при вычислении, например, 1/3=0.33333..., метод divide() может вызвать исключение, если для операции не определен режим округления. Следовательно, библиотека, а не язык, гарантирует, что объект соблюдает контракт, подразумеваемый в определении класса.
Стандартный ML имеет строго определенную семантику и известен как типобезопасный. Однако некоторые реализации, включая Standard ML of New Jersey (SML/NJ), его синтаксический вариант Mythryl и MLton , предоставляют библиотеки, которые предлагают небезопасные операции. Эти возможности часто используются в сочетании с интерфейсами внешних функций этих реализаций для взаимодействия с кодом, не являющимся ML (например, библиотеками C), который может требовать данных, размещенных определенным образом. Другим примером является сам интерактивный верхний уровень SML/NJ , который должен использовать небезопасные операции для выполнения кода ML, введенного пользователем.
Modula-2 — это строго типизированный язык с философией проектирования, требующей, чтобы любые небезопасные объекты были явно помечены как небезопасные. Это достигается путем «перемещения» таких объектов во встроенную псевдобиблиотеку SYSTEM, откуда они должны быть импортированы до того, как их можно будет использовать. Таким образом, импорт делает это видимым, когда такие объекты используются. К сожалению, это не было впоследствии реализовано в исходном отчете языка и его реализации. [16] Все еще оставались небезопасные объекты, такие как синтаксис приведения типов и записи вариантов (унаследованные от Pascal), которые можно было использовать без предварительного импорта. [17] Трудность перемещения этих объектов в псевдомодуль SYSTEM заключалась в отсутствии какого-либо идентификатора для объекта, который затем можно было бы импортировать, поскольку можно импортировать только идентификаторы, но не синтаксис.
IMPORT SYSTEM ; (* позволяет использовать некоторые небезопасные возможности: *) VAR word : SYSTEM . WORD ; addr : SYSTEM . ADDRESS ; addr := SYSTEM . ADR ( word );(* но синтаксис приведения типа можно использовать без такого импорта *) VAR i : INTEGER ; n : CARDINAL ; n := CARDINAL ( i ); (* или *) i := INTEGER ( n );Стандарт ISO Modula-2 исправил это для возможности приведения типов, изменив синтаксис приведения типов на функцию CAST, которую необходимо импортировать из псевдомодуля SYSTEM. Однако другие небезопасные возможности, такие как записи вариантов, оставались доступными без какого-либо импорта из псевдомодуля SYSTEM. [18]
IMPORT SYSTEM ; VAR i : INTEGER ; n : CARDINAL ; i := SYSTEM . CAST ( INTEGER , n ); (* Тип приведен в ISO Modula-2 *)Недавняя ревизия языка строго применила изначальную философию дизайна. Во-первых, псевдомодуль SYSTEM был переименован в UNSAFE, чтобы сделать небезопасную природу импортируемых оттуда объектов более явной. Затем все оставшиеся небезопасные объекты были либо полностью удалены (например, записи вариантов), либо перемещены в псевдомодуль UNSAFE. Для объектов, где нет идентификатора, который можно было бы импортировать, были введены разрешающие идентификаторы. Чтобы включить такой объект, его соответствующий разрешающий идентификатор должен быть импортирован из псевдомодуля UNSAFE. В языке не осталось небезопасных объектов, которые не требуют импорта из UNSAFE. [17]
IMPORT UNSAFE ; VAR i : INTEGER ; n : CARDINAL ; i := UNSAFE . CAST ( INTEGER , n ); (* Тип приведен в Modula-2 Revision 2010 *)FROM UNSAFE IMPORT FFI ; (* идентификатор включения для интерфейса внешней функции *) <*FFI="C"*> (* прагма для интерфейса внешней функции в C *)В Pascal есть ряд требований безопасности типов, некоторые из которых сохраняются в некоторых компиляторах. Когда компилятор Pascal диктует «строгую типизацию», две переменные не могут быть назначены друг другу, если они не являются совместимыми (например, преобразование целого числа в действительное) или не назначены идентичному подтипу. Например, если у вас есть следующий фрагмент кода:
тип TwoTypes = запись I : Целое число ; Q : Действительное число ; конец ; DualTypes = запись I : Целое число ; Q : Действительное число ; конец ; var T1 , T2 : ДваТипа ; D1 , D2 : ДвойныеТипы ; При строгой типизации переменная, определенная как TwoTypes, несовместима с DualTypes ( потому что они не идентичны, хотя компоненты этого пользовательского типа идентичны), а присваивание является недопустимым. Присваивание было бы допустимым, поскольку подтипы, для которых они определены, идентичны . Однако присваивание, такое как было бы допустимым.T1 := D2;T1 := T2;T1.Q := D1.Q;
В целом, Common Lisp является типобезопасным языком. Компилятор Common Lisp отвечает за вставку динамических проверок для операций, типобезопасность которых не может быть доказана статически. Однако программист может указать, что программа должна быть скомпилирована с более низким уровнем динамической проверки типов. [19] Программа, скомпилированная в таком режиме, не может считаться типобезопасной.
Следующие примеры иллюстрируют, как операторы приведения C++ могут нарушить безопасность типов при неправильном использовании. Первый пример показывает, как базовые типы данных могут быть неправильно приведены:
#include <iostream> с использованием пространства имен std ; int main () { int ival = 5 ; // целочисленное значение float fval = reinterpret_cast < float &> ( ival ); // переинтерпретировать битовую комбинацию cout << fval << endl ; // вывести целое число как float return 0 ; } В этом примере reinterpret_castявно запрещает компилятору выполнять безопасное преобразование из целого числа в число с плавающей точкой. [20] При запуске программы она выведет мусорное значение с плавающей точкой. Проблему можно было бы избежать, написав вместо этогоfloat fval = ival;
Следующий пример показывает, как ссылки на объекты могут быть неправильно преобразованы вниз:
#include <iostream> с использованием пространства имен std ; class Parent { public : virtual ~ Parent () {} // виртуальный деструктор для RTTI }; класс Ребенок1 : публичный Родитель { публичный : int a ; }; класс Ребенок2 : публичный Родитель { публичный : float b ; }; int main () { Child1 c1 ; c1 . a = 5 ; Parent & p = c1 ; // приведение вверх всегда безопасно Child2 & c2 = static_cast < Child2 &> ( p ); // недопустимое приведение вниз cout << c2 . b << endl ; // выведет мусорные данные return 0 ; } Два дочерних класса имеют элементы разных типов. При приведении указателя родительского класса к указателю дочернего класса результирующий указатель может не указывать на допустимый объект правильного типа. В примере это приводит к выводу мусорного значения. Проблему можно было бы избежать, заменив на , static_castкоторый dynamic_castвызывает исключение при недопустимых приведениях. [21]
В языке C правильный метод — объявить, что malloc возвращает указатель на void, а затем явно привести указатель к желаемому типу с помощью приведения.