СПАРК (язык программирования) - SPARK (programming language)

Эта статья о язык программирования. Для кластерные вычисления фреймворк, который может работать на Scala, Ява, и Python, видеть Apache Spark.
ИСКРА
Sparkada.jpg
ПарадигмаМультипарадигма
РазработчикАльтран и AdaCore
Стабильный выпуск
17.1 / 14 марта 2017 г.; 3 года назад (2017-03-14)
Печатная дисциплинастатический, сильный, безопасный, именительный падеж
Операционные системыКроссплатформенность: Linux, Майкрософт Виндоус, Mac OS X
ЛицензияGPLv3
Интернет сайтНабор инструментов SPARK Pro Издание "Libre" SPARK GPL
Основной реализации
SPARK Pro, SPARK GPL Edition
Под влиянием
Ада, Эйфель

ИСКРА это формально определенный компьютер язык программирования на основе Ада язык программирования, предназначенный для разработки высокой целостности программного обеспечения используется в системах, где важна предсказуемая и высоконадежная работа. Это облегчает разработку приложений, требующих безопасности, защищенности или целостности бизнеса.

Изначально существовало три версии языка SPARK (SPARK83, SPARK95, SPARK2005) на основе Ada 83, Ada 95 и Ada 2005 соответственно.

Четвертая версия языка SPARK, SPARK 2014, основанная на Ada 2012, была выпущена 30 апреля 2014 года. SPARK 2014 - это полностью переработанный язык и поддержка проверка инструменты.

Язык SPARK состоит из четко определенного подмножества языка Ada, в котором используются контракты для описания спецификации компонентов в форме, пригодной как для статической, так и для динамической проверки.

В SPARK83 / 95/2005 контракты закодированы в комментариях Ada (и поэтому игнорируются любым стандартным компилятором Ada), но обрабатываются SPARK «Examiner» и связанными с ним инструментами.

SPARK 2014, напротив, использует встроенный в Ada 2012 синтаксис «аспекта» для выражения контрактов, привнося их в ядро ​​языка. Основной инструмент для SPARK 2014 (GNATprove) основан на инфраструктуре GNAT / GCC и повторно использует почти весь интерфейс GNAT Ada 2012.

Технический обзор

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

Комбинация этих подходов предназначена для того, чтобы позволить SPARK достичь своих целей проектирования, а именно:

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

Примеры контрактов

Рассмотрим спецификацию подпрограммы Ada ниже:

процедура Приращение (X: внутрь Counter_Type);

Что на самом деле делает эта подпрограмма? В чистом Ada он мог делать практически все - он мог увеличивать Икс на одну или одну тысячу; или он может установить глобальный счетчик на Икс и вернуть исходное значение счетчика в Икс; или он может абсолютно ничего не делать с Икс вообще.

В SPARK 2014 в код добавляются контракты, чтобы предоставить дополнительную информацию о том, что на самом деле делает подпрограмма. Например, мы можем изменить приведенную выше спецификацию, чтобы сказать:

процедура Приращение (X: внутрь Counter_Type)  с Глобальный => ноль, Зависит => (X => X);

Это указывает на то, что Приращение процедура не использует (не обновляет и не читает) какие-либо глобальные переменные и что единственный элемент данных, используемый при вычислении нового значения Икс является Икс сам.

В качестве альтернативы дизайнер может указать:

процедура Приращение (X: внутрь Counter_Type)  с Global => (In_Out => Count), Depends => (Count => (Count, X), X => null);

Это указывает на то, что Приращение будет использовать глобальную переменную Считать в той же упаковке, что и Приращение, что экспортированная стоимость Считать зависит от импортированных значений Считать и Икс, и что экспортированная стоимость Икс вообще не зависит от каких-либо переменных (будет получено только из постоянных данных).

Если затем GNATprove запускается для спецификации и соответствующего тела подпрограммы, он проанализирует тело подпрограммы, чтобы построить модель информационного потока. Затем эта модель сравнивается с той, которая была указана в аннотациях и любых расхождениях, сообщаемых пользователю.

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

процедура Приращение (X: внутрь Counter_Type)  с Global => null, Depends => (X => X), Pre => X  X = X'Old + 1;

Теперь это указывает не только на то, что Икс происходит от самого себя, но также и до Приращение называется Икс должно быть строго меньше последнего возможного значения своего типа, а затем Икс будет равно начальному значению Икс плюс один.

Условия проверки

GNATprove также может генерировать набор условия проверки или венчурные капиталисты. VC используются для попытки установить определенные свойства для данной подпрограммы. Как минимум, GNATprove будет генерировать VC, пытаясь установить, что все ошибки времени выполнения не могут возникать в подпрограмме, например

  • индекс массива вне допустимого диапазона
  • нарушение диапазона типов
  • деление на ноль
  • числовое переполнение.

Если в подпрограмму добавлено постусловие или другие утверждения, GNATprove также сгенерирует VC, которые потребуют от пользователя показать, что эти свойства сохраняются для всех возможных путей в подпрограмме.

Под капотом GNATprove использует промежуточный язык Why3 и генератор VC, а также средства доказательства теорем CVC4, Z3 и Alt-Ergo для разгрузки VC. Использование других программ доказательства (включая интерактивные средства проверки правописания) также возможно через другие компоненты набора инструментов Why3.

История

Первая версия СПАРК (на базе Ada 83) была произведена на Саутгемптонский университет (с Великобританией Министерство обороны спонсорство) Бернаром Карре и Тревором Дженнингсом. Впоследствии язык был постепенно расширен и уточнен, сначала Program Validation Limited, а затем Praxis Critical Systems Limited. В 2004 году Praxis Critical Systems Limited изменила свое название на Praxis High Integrity Systems Limited. В январе 2010 года компания стала Altran Praxis.

В начале 2009 года Praxis заключила партнерство с AdaCore и выпустила SPARK Pro на условиях GPL. За этим в июне 2009 г. последовала SPARK GPL Edition 2009, направленная на FOSS и академические сообщества.

В июне 2010 года Altran-Praxis объявила, что язык программирования SPARK будет использоваться в программном обеспечении американского проекта Lunar. CubeSat, который планируется завершить в 2015 году.

В январе 2013 года компания Altran-Praxis сменила название на Altran.

О первом выпуске Pro версии SPARK 2014 было объявлено 30 апреля 2014 года, за ним вскоре последовала версия SPARK 2014 GPL, нацеленная на FLOSS и академические сообщества.

Промышленное применение

Системы, связанные с безопасностью

SPARK использовался в нескольких важных для безопасности системах, охватывающих коммерческую авиацию (Роллс-Ройс Трент реактивные двигатели серии, система ARINC ACAMS, Lockheed Martin C130J), военная авиация (EuroFighter Тайфун, Harrier GR9, AerMacchi M346), управление воздушным движением (система UK NATS iFACTS), железнодорожный транспорт (многочисленные приложения для сигнализации), медицина (LifeFlow желудочковое вспомогательное устройство ) и космических приложений ( Проект CubeSat Технического колледжа Вермонта ).

Системы, связанные с безопасностью

SPARK также использовался при разработке безопасных систем. Пользователи включают Rockwell Collins (междоменные решения Turnstile и SecureOne), разработку оригинального MULTOS CA, демонстратора NSA Tokeneer, многоуровневую рабочую станцию ​​secunet, ядро ​​разделения Muen и шифратор блочных устройств Genode.

В августе 2010 года Род Чепмен, главный инженер Altran Praxis, реализовал Моток, один из кандидатов в SHA-3, в SPARK. Он хотел сравнить производительность реализаций SPARK и C. После тщательной оптимизации ему удалось сделать версию SPARK всего на 5-10% медленнее, чем C. Позднее усовершенствование среднего уровня Ada в GCC (реализованное Эриком Ботказоу из AdaCore) закрыло пробел, при этом код SPARK соответствовал C в исполнении ровно.[1]

Смотрите также

Примечания

  1. ^ Хенди, Алекс (24 августа, 2010). "Криптовалюта Skein, производная от Ada, показывает SPARK". SD Times. ООО «БЗ Медиа». Получено 2010-08-31.

Рекомендации

внешняя ссылка