Типизация данных
Вывод типов Статическая типизация Динамическая типизация Последовательная типизация Сильная типизация Зависимые типы Утиная типизация

Типобезопасность ( англ. type safety ) — свойство языка программирования , характеризующее безопасность и надёжность в применении его системы типов .

Система типов называется безопасной ( англ. safe ) или надёжной ( англ. sound ), если в программах, прошедших проверку согласования типов ( англ. well-typed programs или well-formed programs ), исключена возможность возникновения ошибок согласования типов во время выполнения .

Ошибка согласования типов или ошибка типизации ( англ. type error ) — несогласованность типов компонентов выражений в программе, например попытка использовать целое число в роли функции . Пропущенные ошибки согласования типов на этапе выполнения могут приводить к багам и даже крахам программ . Безопасность языка не является синонимом полного отсутствия багов, но, по меньшей мере, они становятся исследуемы в рамках семантики языка (формальной или неформальной) .

Надёжные системы типов также называют сильными ( англ. strong ) , но трактовка этого термина часто смягчается, кроме того, его часто применяют к языкам, осуществляющим динамическую проверку согласования типов ( сильная и слабая типизация ).

Иногда безопасность рассматривается как свойство конкретной программы, а не языка, на котором она написана — по той причине, что некоторые типобезопасные языки разрешают обойти или нарушить систему типов , если программист практикует скудную типобезопасность. Распространено мнение, что такие возможности на практике оказываются необходимостью, но это вымысел . Понятие о «безопасности программы» важно в том смысле, что реализация безопасного языка сама может быть небезопасной. Раскрутка компилятора решает эту проблему, обеспечивая языку безопасность не только в теории, но и на практике.

Подробности

Робину Милнеру принадлежит выражение «Программы, прошедшие проверку типов, не могут „сбиться с пути истинного“» . Иначе говоря, безопасная система типов предотвращает заведомо ошибочные операции, связанные с неверными типами. Например, выражение 3 / "Hello, World" очевидно является ошибочным, поскольку арифметика не определяет операцию деления числа на строку. Формально, безопасность означает гарантию того, что значение любого выражения , прошедшего проверку типов, и имеющего тип τ , является истинным элементом множества значений τ , то есть будет лежать в границах диапазона значений, допустимого статическим типом этого выражения. На самом деле, в этом требовании есть нюансы — см. и полиморфизм для сложных случаев.

Кроме того, при интенсивном использовании механизмов определения новых типов предотвращаются логические ошибки , проистекающие из семантики различных типов . Например, и миллиметры , и дюймы являются единицами длины и могут представляться целыми числами, но будет ошибкой вычитать дюймы из миллиметров, и развитая система типов не допустит этого (разумеется, при условии, что программист использует для значений, выраженных в различных единицах, различные типы данных, а не описывает и те, и другие как переменные целого типа). Другими словами, безопасность языка означает, что язык защищает программиста от его собственных возможных ошибок .

Многие языки системного программирования (например, Ада , Си , C++ ) предусматривают ненадёжные ( англ. unsound ) или небезопасные ( англ. unsafe ) операции, предназначенные для возможности нарушить ( англ. violate ) систему типов — см. приведение типа и каламбур типизации . В одних случаях это допускается лишь в ограниченных частях программы, в других — неотличимо от хорошо типизированных операций .

В мейнстриме ^{[ уточнить ]} нередко встречается сужение понятия типобезопасности до « безопасности типов в отношении доступа к памяти » ( англ. memory type safety ), означающее, что компоненты объектов одного агрегатного типа не могут обращаться к ячейкам памяти, выделенным под объекты другого типа. Безопасность доступа к памяти означает запрещение возможности скопировать произвольную цепочку бит из одной области памяти в другую. Например, если язык предусматривает тип t , имеющий ограниченный спектр допустимых значений, и предоставляет возможность скопировать нетипизированные данные в переменную этого типа, то это не является типобезопасным, поскольку потенциально допускает, что переменная типа t будет иметь значение, не являющееся допустимым для типа t . И, в частности, если такой небезопасный язык позволяет записать произвольное целое значение в переменную, имеющую тип « указатель », то небезопасность доступа к памяти очевидна (см. Висячий указатель ). Примерами небезопасных языков служат Си и C++ . В сообществах этих языков часто называют «безопасными» любые операции, непосредственно не приводящие к краху программы . Безопасность доступа к памяти также означает предотвращение возможности переполнения буфера , например, попытки записи крупноразмерных объектов в ячейки, выделенные для объектов другого типа меньшего размера.

Надёжные статические системы типов консервативны (избыточны) в том смысле, что отвергают даже программы, которые исполнились бы корректно. Причина этого заключается в том, что для любого тьюринг-полного языка, множество программ, которые могут порождать ошибки согласования типов во время выполнения, алгоритмически неразрешимо (см. проблема остановки ) . Как следствие, такие системы типов обеспечивают степень защиты, существенно более высокую, чем это необходимо для обеспечения безопасности доступа к памяти. С другой стороны, безопасность некоторых действий не может быть доказана статически и должна контролироваться динамически — например, индексация массива с произвольным доступом. Такой контроль может осуществляться либо рантайм -системой самого языка, либо непосредственно функциями, реализующими подобные потенциально небезопасные операции.

Сильно динамически типизируемые языки (например, Лисп , Smalltalk ) не допускают повреждения данных за счёт того, что программа, пытающаяся преобразовать значение к несовместимому типу, порождает исключение. К достоинствам сильной динамической типизации перед типобезопасностью можно отнести отсутствие консервативности, и, как следствие, расширение спектра решаемых задач программирования. Ценой этого становится неизбежное снижение быстродействия программ, а также необходимость существенно бо́льшего количества пробных запусков для выявления возможных ошибок. Поэтому многие языки комбинируют возможности статического и динамического контроля согласования типов тем или иным образом.

Примеры безопасных языков

Ада

Ада (наиболее типобезопасный язык в семействе Паскаля ) ориентирована на разработку надёжных встраиваемых систем , драйверов и других задач системного программирования . Для реализации критичных секций Ada предоставляет ряд небезопасных конструкций, имена которых обычно начинаются с Unchecked_ .

Язык SPARK является подмножеством Ады. Из него устранены небезопасные возможности, но добавлены возможности проектирования по контракту . SPARK исключает возможность возникновения висячих указателей посредством исключения самой возможности динамического выделения памяти. Статически проверяемые контракты были добавлены в Ada2012.

Хоар в тьюринговской лекции утверждал, что для обеспечения надёжности мало статических проверок — надёжность в первую очередь является следствием простоты . Тогда же он предсказал, что сложность Ады станет причиной катастроф.

BitC

BitC представляет собой гибридный язык, комбинирующий низкоуровневые возможности Си с безопасностью Standard ML и лаконичностью Scheme . BitC ориентирован на разработку надёжных встраиваемых систем , драйверов и решение других задач системного программирования .

Cyclone

Исследовательский язык Cyclone является безопасным диалектом языка Си , заимствующим многие идеи из ML (включая типобезопасный параметрический полиморфизм ). Cyclone предназначен для тех же задач, что и Си, и после осуществления всех проверок компилятор порождает код на ANSI C . Cyclone не требует виртуальной машины или сборки мусора для обеспечения динамической безопасности — вместо этого он основан на управлении памятью посредством регионов . Cyclone устанавливает более высокую планку требований безопасности исходного кода, и из-за небезопасной природы Си портирование даже простых программ с Си на Cyclone может потребовать определённой работы, хотя немалая её часть может быть проделана в рамках Си до смены компилятора. Поэтому Cyclone часто определяют не как диалект Си, а как « язык, синтаксически и семантически похожий на Си ».

Rust

Многие идеи Cyclone нашли воплощение в языке Rust . Помимо сильной статической типизации в язык добавлен статический анализ времени жизни указателей, основанный на концепции «владения». Реализованы статические ограничения, блокирующие потенциально некорректный доступ к памяти: отсутствуют нулевые указатели, невозможно появление неинициализированных и деинициализированных переменных, запрещено совместное использование изменяемых переменных несколькими задачами. Проверка на выход за пределы массива обязательна.

Haskell

Haskell (потомок ML ) изначально разрабатывался как полнотиповый чистый язык, что должно было сделать поведение программ на нём ещё более предсказуемым, чем на ранних диалектах ML . Однако, позже в стандарте языка были предусмотрены небезопасные операции , необходимые в повседневной практике, хотя и отмеченные соответствующими идентификаторами (начинающимися с unsafe ) .

Haskell также предоставляет возможности слабой динамической типизации, и в стандарт языка была включена реализация механизма обработки исключений посредством этих возможностей. Её использование может приводить к аварийному завершению программ, за что назвал Хаскел « исключительно небезопасным » . Он считает неприемлемым тот факт, что исключения имеют тип, определённый пользователем в контексте класса типов Typeable , с учётом того, что исключения генерируются безопасным кодом (за пределами монады IO ); и классифицирует выдаваемое компилятором сообщение о внутренней ошибке как несоответствующее слогану Милнера . В последовавшем обсуждении было показано, как можно было бы реализовать в Хаскеле статически типобезопасные исключения в стиле Standard ML .

Лисп

«Чистый» (минимальный) Лисп представляет собой однотиповый язык (то есть любая конструкция принадлежит к типу « S-выражение ») , хотя даже первые промышленные реализации Lisp предусматривали как минимум определённое количество . Семейство потомков языка Lisp представлено по большей степени сильно динамически типизируемыми языками, но существуют статически типизируемые и сочетающие обе формы типизации.

Common Lisp является сильно динамически типизируемым языком, но предусматривает возможность явно ( ) назначать типы (а компилятор SBCL способен сам их выводить ), однако, эта возможность используется для оптимизации и усиления динамических проверок и не означает статическую типобезопасность. Программист может установить для компилятора сниженный уровень динамических проверок с целью повышения быстродействия, и скомпилированная таким образом программа уже не может считаться безопасной .

Язык Scheme также является сильно динамически типизируемым языком, но компилятор статически выводит типы, используя их для агрессивной оптимизации программ. Языки «Typed Racket» (расширение Racket Scheme ) и типобезопасны. Clojure сочетает сильный динамический и статический контроль типов.

ML

Язык ML изначально разрабатывался в качестве интерактивной системы доказательства теорем , и лишь впоследствии стал самостоятельным компилируемым языком общего назначения. Много усилий было уделено доказательству надёжности параметрически полиморфной системы типов Хиндли-Милнера , лежащей в основе ML . Доказательство надёжности построено для чисто функционального подмножества ( «Fuctional ML» ), расширения ссылочными типами ( «Reference ML» ), расширения исключениями ( «Exception ML» ), для языка, объединяющего все эти расширения ( «Core ML» ) и наконец, его расширения первоклассными продолжениями ( «Control ML» ), сперва мономорфными, затем полиморфными .

Следствием этого стало то, что потомки ML зачастую априори считаются типобезопасными, даже несмотря на то, что некоторые из них откладывают значимые проверки на программы ( OCaml ), либо отклоняются от семантики, для которой построено доказательство надёжности, и содержат небезопасные возможности явным образом ( Haskell ). Для языков семейства ML характерна развитая поддержка алгебраических типов данных , использование которых существенно способствует предотвращению логических ошибок , что также поддерживает впечатление типобезопасности.

Некоторые потомки ML так же являются инструментами интерактивного доказательства ( Idris , Mercury , Agda ). Многие из них, хотя и могли бы использоваться для непосредственной разработки программ с доказанной надёжностью, чаще используются для верификации программ на других языках — из-за таких причин как высокая трудоёмкость использования, низкое быстродействие, отсутствие и прочее. Среди потомков ML с доказанной надёжностью выделяются как ориентированные на промышленное применение языки Standard ML и прототип его дальнейшего развития successor ML (ранее известный как «ML2000»).

Standard ML

Язык Standard ML (старший в семействе языков ML ) ориентирован на разработку программ промышленного быстродействия . Язык имеет строгое формальное определение и его статическая и динамическая безопасность доказана . После статической проверки согласованности интерфейсов компонентов программы (в том числе порождаемых — см. функторы ML ), дальнейший контроль безопасности поддерживается рантайм -системой. Как следствие, даже содержащая ошибку программа на Standard ML всегда продолжает вести себя как ML-программа: она может навечно уйти в расчёты или выдать пользователю сообщение об ошибке, но она не может обрушиться .

Однако, некоторые реализации ( , , MLton ) включают нестандартные библиотеки , предоставляющие определённые небезопасные операции (их идентификаторы начинаются с Unsafe ). Эти возможности необходимы для этих реализаций, обеспечивающего взаимодействие с не-ML-кодом (обычно это код на Си , реализующий критичные по скорости компоненты программ), который может требовать своеобразного битового представления данных. Кроме того, многие реализации Standard ML , хотя сами написаны на нём самом , используют рантайм -систему, написанную на Си . Другим примером является режим REPL компилятора , использующий небезопасные операции для исполнения интерактивно вводимого программистом кода.

Язык Alice является расширением Standard ML , предоставляя возможности сильной динамической типизации.

См. также

• ( англ. )
• Аварийный отказ
• Теория типов
• Формальная верификация
• Автоматическое доказательство
• Приведение типа
• Каламбур типизации

Примечания

Литература

• Robin Milner . (англ.) . — Jcss, 1978. — Vol. 17 . — P. 348—375 .
• Stavros Macrakis. (англ.) // ACM SIGSOFT Software Engineering Notes. — 1982. — Vol. 7 , iss. 2 , no. April . — P. 25—26 . — doi : .
• Luca Cardelli, Peter Wegner. (англ.) . — , 1985. — P. 471—523 . — ISSN .
• Альфред Ахо, Рави Сети, Джеффри Ульман. Компиляторы: принципы, технологии и инструменты. — Addison-Wesley Publishing Company, Издательский дом «Вильямс», 1985, 2001, 2003. — 768 с. — ISBN 5-8459-0189-8 (рус.), 0-201-10088-6 (ориг.).
• . (англ.) // IFIP State-of-the-Art Reports. — Springer-Verlag, 1991. — Iss. Formal Description of Programming Concepts . — P. 431—507 .
• Andrew W. Appel. (англ.) . — Princeton University, revised version of CS-TR-364-92, 1992.
• Andrew K. Wright, . (англ.) // Information and Computation. — 1992. — Vol. 115 , iss. 1 . — P. 38—94 . — doi : .
• Lawrence C. Paulson. ML for the Working Programmer (англ.) . — 2nd. — Cambridge University Press, 1996. — 492 p. — ISBN 0-521-57050-6 (твёрдый переплёт), 0-521-56543-X (мягкий переплёт).
• Pierce, Benjamin C. (англ.) . — MIT Press , 2002. — ISBN 0-262-16209-1 .
  • Перевод на русский язык: Пирс Б. Типы в языках программирования. — , 2012. — 680 с. — ISBN 978-5-7913-0082-9 .
• John C. Mitchell. Concepts in Programming Languages (англ.) . — Cambridge University Press, 2004. — ISBN 0-511-04091-1 (eBook in netLibrary); 0-521-78098-5 (hardback).
• Harper. (англ.) . — version 1.37 (revised 01.11.2014). — licensed under the Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 United States License., 2012. — 544 p. от 24 октября 2015 на Wayback Machine
• . .

Ссылки

• (неопр.) . Portland Pattern Repository Wiki . Дата обращения: 5 февраля 2014.
• Robert Harper . .