Язык SPARK - историческая перспектива и разработка FOSS
4 февр. 2018 г. автор Yannick Moy: FOSDEM 2018 Язык SPARK - историческая перспектива и разработка FOSS. Первая версия SPARK (на основе Ada 83) была создана в Саутгемптонском университете при поддержке британского Министерства обороны Бернаром Карре (Bernard Carré) и Тревором Дженнингсом (Trevor Jennings), авторами системы надёжного программирования на Паскале SPADE-Pascal. Далее над усовершенствованием языка работали компании: Program Validation Limited, Praxis Critical Systems Limited (в дальнейшем Altran-Praxis, Altran) и AdaCore. В начале 2009 года Praxis заключила соглашение с AdaCore и выпустила SPARK Pro на условиях GPL. Затем в июне 2009 была выпущена SPARK GPL Edition, нацеленная на разработку свободного и академического ПО. О выпуске версии языка второго поколения SPARK 2014 было объявлено 30 апреля 2014 года. SPARK (SPADE Ada Kernel) - формально определённый язык программирования, являющийся подмножеством Ada, предназначен для разработки верифицированного программного обеспечения высокого уровня полноты безопасности. SPARK позволяет создавать приложения, которые обладают предсказуемым поведением и обеспечивают высокую надёжность. Версии языка SPARK связаны с версиями Ada и разделены на два поколения: SPARK 83, SPARK 95 и SPARK 2005 (Ada 83, Ada 95 и Ada 2005 соответственно) относят к первому поколению, а SPARK 2014 (Ada 2012) - ко второму. Это обусловлено тем, что первоначально для указания спецификаций и контрактов использовались комментарии, но, начиная с Ada 2012, для этого стал применяться появившийся в языке механизм аспектов. Это привело к полной переработке всего инструментария языка и появлению нового верификатора GNATprove. SPARK используется в авиации (реактивные двигатели Rolls-Royce Trent, самолёты Eurofighter Typhoon и Бе-200, система UK NATS iFACTS и для разработки космических систем (РН Вега, множество спутников). Также его применяют для разработки систем шифрования и кибербезопасности. Целью разработки SPARK было сохранение сильных сторон Ada (таких как система пакетов и ограниченные типы) и удаление из неё всех потенциально небезопасных или двусмысленных конструкций, так как Ada, несмотря на заявленные цели разработки, получилась довольно сложным языком и не имела полного формального определения, а некоторые из её частей вызвали серьёзную критику. Программы SPARK должны быть однозначными, их поведение не должно зависеть от выбора компилятора, параметров компиляции и состояния окружения. Для этого в язык введены некоторые ограничения, в том числе: использование задач возможно только в профиле Ravenscar; для выражений запрещены побочные эффекты; запрещено использование контролируемых типов, для которых возможно переопределение процедур инициализации и оператора присваивания; запрещено совмещение имён; ограничено использование некоторых операторов, таких как goto; запрещено динамическое выделение памяти (но при этом разрешены типы с динамическими границами и типы с дискриминантами). При этом любая программа SPARK всё ещё может быть собрана компилятором Ada, что позволяет смешивать эти языки в одном проекте. Разработчикам SPARK удалось получить удобный для автоматической верификации язык, имеющий простую семантику, строгое формальное определение, логическую корректность и хорошую выразительность. При верификации программ используются следующие приёмы: - проверка выполнения пред- и постусловий функций; - проверка отсутствия кода, способного вызвать исключение; - потоковый анализ зависимостей, который проверяет инициализацию переменных и взаимосвязь между параметрами и результатом работы функций. Для того, чтобы доказать корректность программы, для всех использованных программистом конструкций, таких как пред- и постусловия, создаются наборы проверочных утверждений. Верификатор GNATprove также может в некоторых случаях самостоятельно генерировать проверочные утверждения. Так, будут выполнены проверки на выход за границы массивов или типов, переполнение и деление на ноль. Далее, набор проверочных утверждений и данные о начальном состоянии программы, а также полученные от разработчика непроверяемые утверждения, передаются в программу автоматического доказательства. GNATprove при работе использует платформу Why3 и системы доказательства проверочных утверждений CVC4, Z3 и Alt-Ergo. Также для доказательства могут быть использованы сторонние системы, такие как Coq.
4 февр. 2018 г. автор Yannick Moy: FOSDEM 2018 Язык SPARK - историческая перспектива и разработка FOSS. Первая версия SPARK (на основе Ada 83) была создана в Саутгемптонском университете при поддержке британского Министерства обороны Бернаром Карре (Bernard Carré) и Тревором Дженнингсом (Trevor Jennings), авторами системы надёжного программирования на Паскале SPADE-Pascal. Далее над усовершенствованием языка работали компании: Program Validation Limited, Praxis Critical Systems Limited (в дальнейшем Altran-Praxis, Altran) и AdaCore. В начале 2009 года Praxis заключила соглашение с AdaCore и выпустила SPARK Pro на условиях GPL. Затем в июне 2009 была выпущена SPARK GPL Edition, нацеленная на разработку свободного и академического ПО. О выпуске версии языка второго поколения SPARK 2014 было объявлено 30 апреля 2014 года. SPARK (SPADE Ada Kernel) - формально определённый язык программирования, являющийся подмножеством Ada, предназначен для разработки верифицированного программного обеспечения высокого уровня полноты безопасности. SPARK позволяет создавать приложения, которые обладают предсказуемым поведением и обеспечивают высокую надёжность. Версии языка SPARK связаны с версиями Ada и разделены на два поколения: SPARK 83, SPARK 95 и SPARK 2005 (Ada 83, Ada 95 и Ada 2005 соответственно) относят к первому поколению, а SPARK 2014 (Ada 2012) - ко второму. Это обусловлено тем, что первоначально для указания спецификаций и контрактов использовались комментарии, но, начиная с Ada 2012, для этого стал применяться появившийся в языке механизм аспектов. Это привело к полной переработке всего инструментария языка и появлению нового верификатора GNATprove. SPARK используется в авиации (реактивные двигатели Rolls-Royce Trent, самолёты Eurofighter Typhoon и Бе-200, система UK NATS iFACTS и для разработки космических систем (РН Вега, множество спутников). Также его применяют для разработки систем шифрования и кибербезопасности. Целью разработки SPARK было сохранение сильных сторон Ada (таких как система пакетов и ограниченные типы) и удаление из неё всех потенциально небезопасных или двусмысленных конструкций, так как Ada, несмотря на заявленные цели разработки, получилась довольно сложным языком и не имела полного формального определения, а некоторые из её частей вызвали серьёзную критику. Программы SPARK должны быть однозначными, их поведение не должно зависеть от выбора компилятора, параметров компиляции и состояния окружения. Для этого в язык введены некоторые ограничения, в том числе: использование задач возможно только в профиле Ravenscar; для выражений запрещены побочные эффекты; запрещено использование контролируемых типов, для которых возможно переопределение процедур инициализации и оператора присваивания; запрещено совмещение имён; ограничено использование некоторых операторов, таких как goto; запрещено динамическое выделение памяти (но при этом разрешены типы с динамическими границами и типы с дискриминантами). При этом любая программа SPARK всё ещё может быть собрана компилятором Ada, что позволяет смешивать эти языки в одном проекте. Разработчикам SPARK удалось получить удобный для автоматической верификации язык, имеющий простую семантику, строгое формальное определение, логическую корректность и хорошую выразительность. При верификации программ используются следующие приёмы: - проверка выполнения пред- и постусловий функций; - проверка отсутствия кода, способного вызвать исключение; - потоковый анализ зависимостей, который проверяет инициализацию переменных и взаимосвязь между параметрами и результатом работы функций. Для того, чтобы доказать корректность программы, для всех использованных программистом конструкций, таких как пред- и постусловия, создаются наборы проверочных утверждений. Верификатор GNATprove также может в некоторых случаях самостоятельно генерировать проверочные утверждения. Так, будут выполнены проверки на выход за границы массивов или типов, переполнение и деление на ноль. Далее, набор проверочных утверждений и данные о начальном состоянии программы, а также полученные от разработчика непроверяемые утверждения, передаются в программу автоматического доказательства. GNATprove при работе использует платформу Why3 и системы доказательства проверочных утверждений CVC4, Z3 и Alt-Ergo. Также для доказательства могут быть использованы сторонние системы, такие как Coq.