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