Войти
| Системы типов |
|---|
| Общие понятия |
| Основные категории |
|
| Второстепенные категории |
В информатике, безопасность типа является степенью, в которой язык программирование отпугивает или предотвращают ошибки типа. Ошибка типа - это ошибочное поведение программы, вызванное несоответствием между разными типами данных для констант, переменных и методов (функций) программы, например, обработка целого числа ( int) как числа с плавающей запятой ( float). Нужен лучший пример. Типовая безопасность иногда альтернативно рассматривается как свойство компьютерной программы, а не как язык, на котором эта программа написана; то есть некоторые языки имеют средства защиты типов, которые могут быть обойдены программистами, использующими другие средства защиты типов на том же языке. Формальное теоретико-типовое определение безопасности типов значительно сильнее, чем то, что понимает большинство программистов.
Принуждение к типу может быть статическим, обнаруживая потенциальные ошибки во время компиляции, или динамическим, связывая информацию о типе со значениями во время выполнения и консультируясь с ними по мере необходимости для обнаружения неизбежных ошибок, или сочетание того и другого. Применение динамического типа позволяет запускать некорректную программу.
Поведение, классифицируемое как ошибки типа данным языком программирования, обычно является результатом попыток выполнения операций со значениями, не относящимися к соответствующему типу данных. Эта классификация частично основана на мнениях.
В контексте систем статических (во время компиляции) типов типовая безопасность обычно включает (среди прочего) гарантию того, что конечное значение любого выражения будет законным членом статического типа этого выражения. Точное требование более тонкое, чем это - см., Например, Подтипирование и полиморфизм (информатика), где описаны сложности.
Безопасность типов тесно связана с безопасностью памяти, ограничением возможности копирования произвольных битовых комбинаций из одной области памяти в другую. Например, в реализации языка, имеющего некоторый тип, такого, что некоторая последовательность битов (соответствующей длины) не представляет законного члена, если этот язык позволяет копировать данные в переменную типа, тогда он не является типобезопасным, потому что такая операция может присвоить этой переменной не значение. И наоборот, если язык небезопасен по типу до такой степени, что позволяет использовать произвольное целое число в качестве указателя, то он не безопасен для памяти.
Большинство языков со статической типизацией обеспечивают степень безопасности типов, которая строго выше, чем безопасность памяти, потому что их системы типов предписывают правильное использование абстрактных типов данных, определенных программистами, даже если это не является строго необходимым для безопасности памяти или для предотвращения любого рода катастрофического отказа.
Типобезопасный код обращается только к тем ячейкам памяти, к которым ему разрешен доступ. (В этом обсуждении безопасность типов конкретно относится к безопасности типов памяти и не должна путаться с безопасностью типов в более широком смысле.) Например, безопасный тип кода не может считывать значения из частных полей другого объекта.
Робин Милнер использовал следующий слоган для описания безопасности типов:
Соответствующая формализация этого слогана зависит от стиля формальной семантики, используемой для конкретного языка. В контексте денотационной семантики безопасность типов означает, что значение выражения, которое хорошо типизировано, например, с типом τ, является добросовестным членом множества, соответствующего τ.
В 1994 году Эндрю Райт и Маттиас Фелляйзен сформулировали то, что сейчас является стандартным методом определения и доказательства для безопасности типов в языках, определяемых операционной семантикой. При таком подходе безопасность типов определяется двумя свойствами семантики языка программирования:
Эти свойства не существуют в вакууме; они связаны с семантикой языка программирования, который они описывают, и существует большое пространство различных языков, которые могут соответствовать этим критериям, поскольку понятие "хорошо типизированной" программы является частью статической семантики языка программирования, а понятие "застревание" (или "сбой") - это свойство его динамической семантики.
Виджай Сарасват дает следующее определение:
Типовая безопасность в конечном итоге направлена на исключение других проблем, например:
3 / "Hello, World"как недопустимое, потому что правила арифметики не определяют, как делить целое число на строку.Типовая безопасность обычно является требованием для любого игрушечного языка, предлагаемого в академических исследованиях языков программирования. С другой стороны, многие языки слишком велики для доказательств безопасности типов, созданных человеком, поскольку часто требуют проверки тысяч случаев. Тем не менее, было доказано, что некоторые языки, такие как Standard ML, в котором строго определена семантика, соответствуют одному определению безопасности типов. Считается, что некоторые другие языки, такие как Haskell, соответствуют определенному определению безопасности типов при условии, что не используются определенные функции «выхода» (например, unsafePerformIO в Haskell, используемый для «выхода» из обычной ограниченной среды, в которой возможен ввод-вывод, обходит система типов и поэтому может использоваться для нарушения безопасности типов.) Воспроизведение типов - еще один пример такой возможности "escape". Независимо от свойств определения языка, определенные ошибки могут возникать во время выполнения из-за ошибок в реализации или в связанных библиотеках, написанных на других языках; такие ошибки могут сделать данный тип реализации небезопасным при определенных обстоятельствах. Ранняя версия виртуальной машины Sun Java была уязвима для такого рода проблем.
Языки программирования часто в просторечии классифицируются как строго типизированные или слабо типизированные (также слабо типизированные) для обозначения определенных аспектов безопасности типов. В 1974 году Лисков и Зиллес определили строго типизированный язык как язык, в котором «всякий раз, когда объект передается от вызывающей функции к вызываемой функции, его тип должен быть совместим с типом, объявленным в вызываемой функции». В 1977 году Джексон писал: «В строго типизированном языке каждая область данных будет иметь отдельный тип, и каждый процесс будет определять свои требования к коммуникации в терминах этих типов». Напротив, слабо типизированный язык может давать непредсказуемые результаты или может выполнять неявное преобразование типов.
В объектно-ориентированных языках безопасность типов обычно присуща наличию системы типов. Это выражается в определениях классов.
Класс по существу, определяет структуру объектов, получаемых из него и API в качестве контракта для обработки этих объектов. Каждый раз, когда создается новый объект, он будет соответствовать этому контракту.
Каждая функция, которая обменивается объектами, производными от определенного класса или реализующими конкретный интерфейс, будет придерживаться этого контракта: следовательно, в этой функции операции, разрешенные для этого объекта, будут только теми, которые определены методами класса, реализуемого объектом. Это гарантирует сохранение целостности объекта.
Исключением являются объектно-ориентированные языки, которые позволяют динамически изменять структуру объекта или использовать отражение для изменения содержимого объекта, чтобы преодолеть ограничения, налагаемые определениями методов класса.
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 , с аргументом, указывающим, сколько байтов требуется. Функция возвращает нетипизированный указатель (тип void *), который вызывающий код должен явно или неявно привести к соответствующему типу указателя. Предварительно стандартизованные реализации C требовали для этого явного приведения, поэтому код стал общепринятой практикой. (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..., метод div () может вызвать исключение, если для операции не определен режим округления. Следовательно, библиотека, а не язык, гарантирует, что объект соблюдает контракт, подразумеваемый в определении класса.
Стандартный ML имеет строго определенную семантику и известен как типобезопасный. Однако некоторые реализации, включая Standard ML of New Jersey (SML / NJ), его синтаксический вариант Mythryl и MLton, предоставляют библиотеки, предлагающие небезопасные операции. Эти средства часто используются в сочетании с интерфейсами внешних функций этих реализаций для взаимодействия с кодом, отличным от ML (например, библиотеками C), которым могут потребоваться данные, размещенные определенным образом. Другим примером является сам интерактивный верхний уровень SML / NJ, который должен использовать небезопасные операции для выполнения кода ML, введенного пользователем.
Modula-2 - это строго типизированный язык с философией проектирования, требующей, чтобы любые небезопасные объекты были явно помечены как небезопасные. Это достигается «перемещением» таких средств во встроенную псевдобиблиотеку под названием SYSTEM, откуда они должны быть импортированы, прежде чем их можно будет использовать. Таким образом, импорт делает видимым, когда такие средства используются. К сожалению, это не было последовательно реализовано в отчете на языке оригинала и его реализации. По-прежнему оставались небезопасными средствами, такими как синтаксис приведения типов и вариантные записи (унаследованные от Паскаля), которые можно было использовать без предварительного импорта. Сложность при перемещении этих средств в псевдомодуль SYSTEM заключалась в отсутствии какого-либо идентификатора для средства, который затем можно было бы импортировать, поскольку можно импортировать только идентификаторы, но не синтаксис.
IMPORT SYSTEM; (* allows the use of certain unsafe facilities: *) VAR word: SYSTEM.WORD; addr: SYSTEM.ADDRESS; addr:= SYSTEM.ADR(word); (* but type cast syntax can be used without such import *) VAR i: INTEGER; n: CARDINAL; n:= CARDINAL(i); (* or *) i:= INTEGER(n);
Стандарт ISO Modula-2 исправил это для средства приведения типов, изменив синтаксис приведения типов в функцию CAST, которую необходимо импортировать из псевдомодуля SYSTEM. Однако другие небезопасные средства, такие как записи вариантов, оставались доступными без какого-либо импорта из псевдомодуля SYSTEM.
IMPORT SYSTEM; VAR i: INTEGER; n: CARDINAL; i:= SYSTEM.CAST(INTEGER, n); (* Type cast in ISO Modula-2 *)
В недавней редакции языка строго применялась оригинальная философия дизайна. Во-первых, псевдомодуль SYSTEM был переименован в UNSAFE, чтобы прояснить небезопасный характер импортированных оттуда средств. Затем все оставшиеся небезопасные объекты были либо полностью удалены (например, вариантные записи), либо перемещены в псевдомодуль UNSAFE. Для объектов, где нет идентификатора, который можно было бы импортировать, были введены разрешающие идентификаторы. Чтобы включить такую возможность, соответствующий ей разрешающий идентификатор должен быть импортирован из псевдомодуля UNSAFE. На языке не остается небезопасных объектов, не требующих импорта из UNSAFE.
IMPORT UNSAFE; VAR i: INTEGER; n: CARDINAL; i:= UNSAFE.CAST(INTEGER, n); (* Type cast in Modula-2 Revision 2010 *) FROM UNSAFE IMPORT FFI; (* enabling identifier for foreign function interface facility *) lt;*FFI="C"*gt; (* pragma for foreign function interface to C *)
У Паскаля был ряд требований к безопасности типов, некоторые из которых сохранены в некоторых компиляторах. Если компилятор Паскаля предписывает «строгую типизацию», две переменные не могут быть присвоены друг другу, если они не совместимы (например, преобразование целого числа в действительное) или присвоены одному и тому же подтипу. Например, если у вас есть следующий фрагмент кода:
type TwoTypes = record I: Integer; Q: Real; end; DualTypes = record I: Integer; Q: Real; end; var T1, T2: TwoTypes; D1, D2: DualTypes;
Под строгим ввода, переменная определяется как TwoTypes это не совместимо с DualTypes (потому что они не являются идентичными, даже если компоненты этого пользователя определенного типа являются идентичными) и присвоение {{{1}}} является незаконным. Присвоение {{{1}}} было бы законным, потому что подтипы, для которых они определены, идентичны. Однако такое назначение, как {{{1}}}, будет законным.
В общем, Common Lisp - это типобезопасный язык. Компилятор Common Lisp отвечает за вставку динамических проверок для операций, безопасность типов которых не может быть доказана статически. Однако программист может указать, что программа должна быть скомпилирована с более низким уровнем динамической проверки типов. Программа, скомпилированная в таком режиме, не может считаться типобезопасной.
В следующих примерах показано, как операторы приведения C ++ могут нарушить безопасность типов при неправильном использовании. Первый пример показывает, как можно неверно привести основные типы данных:
#include lt;iostreamgt; using namespace std; int main () { int ival = 5; // integer value float fval = reinterpret_castlt;floatamp;gt;(ival); // reinterpret bit pattern cout lt;lt; fval lt;lt; endl; // output integer as float return 0; } В этом примере reinterpret_castявно запрещает компилятору выполнять безопасное преобразование из целого числа в значение с плавающей запятой. Когда программа запускается, она выводит мусорное значение с плавающей запятой. Этой проблемы можно было избежать, написав вместо этогоfloat fval = ival;
В следующем примере показано, как ссылки на объекты могут быть неправильно понижены:
#include lt;iostreamgt; using namespace std; class Parent { public: virtual ~Parent() {} // virtual destructor for RTTI }; class Child1: public Parent { public: int a; }; class Child2: public Parent { public: float b; }; int main () { Child1 c1; c1.a = 5; Parent amp; p = c1; // upcast always safe Child2 amp; c2 = static_castlt;Child2amp;gt;(p); // invalid downcast cout lt;lt; c2.b lt;lt; endl; // will output garbage data return 0; } В двух дочерних классах есть члены разных типов. При понижении значения указателя родительского класса на указатель дочернего класса результирующий указатель может не указывать на действительный объект правильного типа. В этом примере это приводит к тому, что печатается мусорное значение. Проблему можно было бы избежать, заменив static_castпри dynamic_castтом, что бросает исключение на недействительных слепков.
