Набор утилит SPARK теперь доступен под GNU GPL

Компания AdaCore объявила о выпуске свободной версии своего набора инструментов для верификации программного обеспечения — SPARK GPL Edition.

Свободная редакция SPARK, GPL Edition, состоит из нескольких компонентов: определение языка SPARK, полный набор утилит SPARK Toolset (в него входят Examiner, Simplifier и Checker), вспомогательные инструменты (SPARKSimp, SPARKMake, SPARKFormat и POGS). Кроме того, учебные пособия по SPARK и SPARK Pro включены в состав сопутствующего релиза пакета Tokeneer Discovery.

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