WikiSort.ru - Программирование

ПОИСК ПО САЙТУ | о проекте
Типизация данных

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

Шаблон: просмотр • обсуждение • править
Эта статья — об обеспечении целостности информации в процессе работы ЭВМ. О разграничении прав доступа к секретной или конфиденциальной информации см. информационная безопасность.

В информатике типобезопасность (англ. 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" очевидно является ошибочным, поскольку арифметика не определяет операцию деления числа на строку. Формально, безопасность означает гарантию того, что значение любого выражения, прошедшего проверку типов, и имеющего тип τ, является истинным элементом множества значений τ, то есть будет лежать в границах диапазона значений, допустимого статическим типом этого выражения. На самом деле, в этом требовании есть нюансы — см. подтипы[en] и полиморфизм для сложных случаев.

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

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

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

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

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

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

Ada

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

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

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

BitC

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

Cyclone

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

Haskell

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

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

Lisp

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

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

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

ML

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

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

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

Standard ML

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

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

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

См. также

Примечания

  1. 1 2 3 Ахо-Сети-Ульман, 1985, 2001, 2003, Статическая и динамическая проверка типов, с. 340.
  2. 1 2 3 Wright, Felleisen, 1992.
  3. ↑ Cardelli - Typeful programming, 1991, с. 3.
  4. 1 2 Mitchel - Concepts in Programming Languages, 2004, 6.2.1 Type Safety, с. 132—133.
  5. 1 2 Java is not type-safe.
  6. ↑ Harper, 2012, Chapter 4. Statics, с. 35.
  7. ↑ Mitchel - Concepts in Programming Languages, 2004, 6.1.2 Type Errors, с. 130.
  8. ↑ Appel - A Critique of Standard ML, 1992, Safety, с. 2.
  9. 1 2 3 Paulson, 1996, с. 2.
  10. ↑ Milner - A Theory of Type Polymorphism in Programming, 1978.
  11. ↑ Cardelli - Typeful programming, 1991, 9.3. Type violations, с. 51.
  12. 1 2 Mitchel - Concepts in Programming Languages, 2004, 6.2.2 Compile-Time and Run-Time Checking, с. 133—135.
  13. ↑ Pierce, 2002, 1.1 Типы в информатике, с. 3.
  14. ↑ Cardelli - Typeful programming, 1991, 9.1 Dynamic types, с. 49.
  15. ↑ C.A.R. Hoare — The Emperor’s Old Clothes, Communications of the ACM, 1981
  16. ↑ unsafeCoerce (язык Haskell)
  17. ↑ System.IO.Unsafe (язык Haskell)
  18. 1 2 Haskell Is Exceptionally Unsafe.
  19. ↑ Cardelli, Wegner - On Understanding Types, 1985, 1.1. Organizing Untyped Universes, с. 3.
  20. ↑ Common Lisp HyperSpec. Проверено 26 мая 2013.
  21. ↑ SBCL Manual — Declarations as Assertions
  22. ↑ successorML
  23. ↑ Appel - A Critique of Standard ML, 1992.
  24. ↑ Robin Milner, Mads Tofte. Commentary on Standard ML. — Universiry of Edinburg, University of Nigeria, 1991.

Литература

Ссылки

Данная страница на сайте WikiSort.ru содержит текст со страницы сайта "Википедия".

Если Вы хотите её отредактировать, то можете сделать это на странице редактирования в Википедии.

Если сделанные Вами правки не будут кем-нибудь удалены, то через несколько дней они появятся на сайте WikiSort.ru .



Текст в блоке "Читать" взят с сайта "Википедия" и доступен по лицензии Creative Commons Attribution-ShareAlike; в отдельных случаях могут действовать дополнительные условия.

Другой контент может иметь иную лицензию. Перед использованием материалов сайта WikiSort.ru внимательно изучите правила лицензирования конкретных элементов наполнения сайта.

2019-2024
WikiSort.ru - проект по пересортировке и дополнению контента Википедии