Объединенными усилиями компании Praxis и AdaCore выпущена GPL версия SPARK, основанного на Ada языка программирования для разработки приложений, безопасность и надежность которых имеет жизненно важное значение. SPARK предлагает инструментарий статической проверки и формирует доказательства корректности, которые могут быть использованы для создания гарантий в соответствии с требованиями промышленных систем сертификации.
Релиз сочетает в себе язык SPARK, инструменты верификации GNAT Programming Studio (GPS) от Praxis и интерактивную среду разработки GNATbench от AdaCore. Существуют версии SPARK, основанные на языках Ada 83, Ada 95 и Ada 2005, так что все ведущие Ada-компиляторы и инструменты работают прямо из коробки.
|