Типобезопасность
Типобезопасность (англ. type safety) — свойство языка программирования, характеризующее безопасность и надёжность в применении его системы типов.
Система типов называется безопасной (англ. safe) или надёжной (англ. sound), если в программах, прошедших проверку согласования типов (англ. well-typed programs или well-formed programs), исключена возможность возникновения ошибок согласования типов во время выполнения[1][2][3][4][5][6].
Ошибка согласования типов или ошибка типизации (англ. type error) — несогласованность типов компонентов выражений в программе, например попытка использовать целое число в роли функции[7]. Пропущенные ошибки согласования типов на этапе выполнения могут приводить к багам и даже крахам программ. Безопасность языка не является синонимом полного отсутствия багов, но, по меньшей мере, они становятся исследуемы в рамках семантики языка (формальной или неформальной)[8].
Надёжные системы типов также называют сильными (англ. strong)[1][2], но трактовка этого термина часто смягчается, кроме того, его часто применяют к языкам, осуществляющим динамическую проверку согласования типов (сильная и слабая типизация).
Иногда безопасность рассматривается как свойство конкретной программы, а не языка, на котором она написана — по той причине, что некоторые типобезопасные языки разрешают обойти или нарушить систему типов, если программист практикует скудную типобезопасность. Распространено мнение, что такие возможности на практике оказываются необходимостью, но это вымысел[9]. Понятие о «безопасности программы» важно в том смысле, что реализация безопасного языка сама может быть небезопасной. Раскрутка компилятора решает эту проблему, обеспечивая языку безопасность не только в теории, но и на практике.
Подробности
Робину Милнеру принадлежит выражение «Программы, прошедшие проверку типов, не могут „сбиться с пути истинного“»[10].
Иначе говоря, безопасная система типов предотвращает заведомо ошибочные операции, связанные с неверными типами. Например, выражение 3 / "Hello, World"
очевидно является ошибочным, поскольку арифметика не определяет операцию деления числа на строку. Формально, безопасность означает гарантию того, что значение любого выражения, прошедшего проверку типов, и имеющего тип τ
, является истинным элементом множества значений τ
, то есть будет лежать в границах диапазона значений, допустимого статическим типом этого выражения. На самом деле, в этом требовании есть нюансы — см. подтипы[англ.] и полиморфизм для сложных случаев.
Кроме того, при интенсивном использовании механизмов определения новых типов предотвращаются логические ошибки, проистекающие из семантики различных типов[5]. Например, и миллиметры, и дюймы являются единицами длины и могут представляться целыми числами, но будет ошибкой вычитать дюймы из миллиметров, и развитая система типов не допустит этого (разумеется, при условии, что программист использует для значений, выраженных в различных единицах, различные типы данных, а не описывает и те, и другие как переменные целого типа). Другими словами, безопасность языка означает, что язык защищает программиста от его собственных возможных ошибок[9].
Многие языки системного программирования (например, Ада, Си, C++) предусматривают ненадёжные (англ. unsound) или небезопасные (англ. unsafe) операции, предназначенные для возможности нарушить (англ. violate) систему типов — см. приведение типа и каламбур типизации. В одних случаях это допускается лишь в ограниченных частях программы, в других — неотличимо от хорошо типизированных операций[11].
В мейнстриме[
Надёжные статические системы типов консервативны (избыточны) в том смысле, что отвергают даже программы, которые исполнились бы корректно. Причина этого заключается в том, что для любого
Сильно динамически типизируемые языки (например, Лисп , Smalltalk) не допускают повреждения данных за счёт того, что программа, пытающаяся преобразовать значение к несовместимому типу, порождает исключение. К достоинствам сильной динамической типизации перед типобезопасностью можно отнести отсутствие консервативности, и, как следствие, расширение спектра решаемых задач программирования. Ценой этого становится неизбежное снижение быстродействия программ, а также необходимость существенно бо́льшего количества пробных запусков для выявления возможных ошибок. Поэтому многие языки комбинируют возможности статического и динамического контроля согласования типов тем или иным образом.[14][12][1]
Примеры безопасных языков
Ада
Unchecked_
.
Язык SPARK является подмножеством Ады. Из него устранены небезопасные возможности, но добавлены возможности проектирования по контракту. SPARK исключает возможность возникновения висячих указателей посредством исключения самой возможности динамического выделения памяти. Статически проверяемые контракты были добавлены в Ada2012.
Хоар в тьюринговской лекции утверждал, что для обеспечения надёжности мало статических проверок — надёжность в первую очередь является следствием простоты[15]. Тогда же он предсказал, что сложность Ады станет причиной катастроф.
BitC
Cyclone
Исследовательский язык
Rust
Многие идеи Cyclone нашли воплощение в языке Rust. Помимо сильной статической типизации в язык добавлен статический анализ времени жизни указателей, основанный на концепции «владения». Реализованы статические ограничения, блокирующие потенциально некорректный доступ к памяти: отсутствуют нулевые указатели, невозможно появление неинициализированных и деинициализированных переменных, запрещено совместное использование изменяемых переменных несколькими задачами. Проверка на выход за пределы массива обязательна.
Haskell
Haskell (потомок ML ) изначально разрабатывался как полнотиповый чистый язык, что должно было сделать поведение программ на нём ещё более предсказуемым, чем на ранних диалектах ML . Однако, позже в стандарте языка были предусмотрены небезопасные операции[16][17], необходимые в повседневной практике, хотя и отмеченные соответствующими идентификаторами (начинающимися с unsafe
)[18].
Typeable
, с учётом того, что исключения генерируются безопасным кодом (за пределами монады IO
); и классифицирует выдаваемое компилятором сообщение о внутренней ошибке как несоответствующее слогану Милнера . В последовавшем обсуждении было показано, как можно было бы реализовать в Хаскеле статически типобезопасные исключения в стиле Standard MLЛисп
«Чистый» (минимальный) Лисп представляет собой
Язык
ML
Язык
Следствием этого стало то, что потомки ML зачастую априори считаются типобезопасными, даже несмотря на то, что некоторые из них откладывают значимые проверки на этап выполнения программы (OCaml), либо отклоняются от семантики, для которой построено доказательство надёжности, и содержат небезопасные возможности явным образом (Haskell ). Для языков семейства ML характерна развитая поддержка алгебраических типов данных, использование которых существенно способствует предотвращению логических ошибок, что также поддерживает впечатление типобезопасности.
Некоторые потомки ML так же являются инструментами интерактивного доказательства (Idris, Mercury, Agda). Многие из них, хотя и могли бы использоваться для непосредственной разработки программ с доказанной надёжностью, чаще используются для верификации программ на других языках — из-за таких причин как высокая трудоёмкость использования, низкое быстродействие, отсутствие FFI[англ.] и прочее. Среди потомков ML с доказанной надёжностью выделяются как ориентированные на промышленное применение языки Standard ML и прототип его дальнейшего развития successor ML[22] (ранее известный как «ML2000»).
Standard ML
Язык
Однако, некоторые реализации (, использующий небезопасные операции для исполнения интерактивно вводимого программистом кода.
Язык Alice является расширением Standard ML, предоставляя возможности сильной динамической типизации.
См. также
- Обеспечение безопасности посредством языка (англ. language-based security)
- Аварийный отказ
- Теория типов
- Формальная верификация
- Автоматическое доказательство
- Приведение типа
- Каламбур типизации
Примечания
- ↑ 1 2 3 Ахо-Сети-Ульман, 1985, 2001, 2003, Статическая и динамическая проверка типов, с. 340.
- ↑ 1 2 3 Wright, Felleisen, 1992.
- ↑ Cardelli - Typeful programming, 1991, с. 3.
- ↑ 1 2 Mitchel - Concepts in Programming Languages, 2004, 6.2.1 Type Safety, с. 132—133.
- ↑ 1 2 Java is not type-safe.
- ↑ Harper, 2012, Chapter 4. Statics, с. 35.
- ↑ Mitchel - Concepts in Programming Languages, 2004, 6.1.2 Type Errors, с. 130.
- ↑ Appel - A Critique of Standard ML, 1992, Safety, с. 2.
- ↑ 1 2 3 Paulson, 1996, с. 2.
- ↑ Milner - A Theory of Type Polymorphism in Programming, 1978.
- ↑ Cardelli - Typeful programming, 1991, 9.3. Type violations, с. 51.
- ↑ 1 2 Mitchel - Concepts in Programming Languages, 2004, 6.2.2 Compile-Time and Run-Time Checking, с. 133—135.
- ↑ Pierce, 2002, 1.1 Типы в информатике, с. 3.
- ↑ Cardelli - Typeful programming, 1991, 9.1 Dynamic types, с. 49.
- ↑ C.A.R. Hoare — The Emperor’s Old Clothes, Communications of the ACM, 1981
- ↑ unsafeCoerce Архивная копия от 29 ноября 2014 на Wayback Machine (язык Haskell)
- ↑ System.IO.Unsafe Архивная копия от 29 ноября 2014 на Wayback Machine (язык Haskell)
- ↑ 1 2 Haskell Is Exceptionally Unsafe.
- ↑ Cardelli, Wegner - On Understanding Types, 1985, 1.1. Organizing Untyped Universes, с. 3.
- ↑ Common Lisp HyperSpec . Дата обращения: 26 мая 2013. Архивировано 16 июня 2013 года.
- ↑ SBCL Manual — Declarations as Assertions . Дата обращения: 20 января 2015. Архивировано 20 января 2015 года.
- ↑ successorML . Дата обращения: 23 декабря 2014. Архивировано из оригинала 7 января 2009 года.
- ↑ Appel - A Critique of Standard ML, 1992.
- ↑ Robin Milner, Mads Tofte. Commentary on Standard ML. — Universiry of Edinburg, University of Nigeria, 1991. Архивировано 1 декабря 2014 года.
Литература
- Robin Milner. A Theory of Type Polymorphism in Programming (англ.). — Jcss, 1978. — Vol. 17. — P. 348—375.
- Stavros Macrakis. Safety and power (англ.) // ACM SIGSOFT Software Engineering Notes. — 1982. — Vol. 7, iss. 2, no. April. — P. 25—26. — .
- Luca Cardelli, Peter Wegner. On Understanding Types, Data Abstraction, and Polymorphism (англ.). — ISSN 0360-0300.
- Альфред Ахо, Рави Сети, Джеффри Ульман. Компиляторы: принципы, технологии и инструменты. — Addison-Wesley Publishing Company, Издательский дом «Вильямс», 1985, 2001, 2003. — 768 с. — ISBN 5-8459-0189-8 (рус.), 0-201-10088-6 (ориг.).
- Лука Карделли[англ.]. Typeful programming (англ.) // IFIP State-of-the-Art Reports. — Springer-Verlag, 1991. — Iss. Formal Description of Programming Concepts. — P. 431—507.
- Andrew W. Appel. A Critique of Standard ML (англ.). — Princeton University, revised version of CS-TR-364-92, 1992.
- Andrew K. Wright, .
- 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. Types and Programming Languages (англ.). — 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. Practical Foundations for Programming Languages (англ.). — 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
- Vijay Saraswat[англ.]. Java is not type-safe.
Ссылки
- Type Safe . Portland Pattern Repository Wiki. Дата обращения: 5 февраля 2014.
- Robert Harper. Haskell Is Exceptionally Unsafe.