SPARK (programming language) とは

SPARKは、予測可能で信頼性の高い操作が不可欠なシステムで使用される高度なインテグリティソフトウェアの開発を目的とした、Adaプログラミング言語に基づいた正式に定義されたコンピュータプログラミング言語です。安全性、セキュリティ、またはビジネスの完全性を必要とするアプリケーションの開発を容易にします。
もともと、Ada 83、Ada 95、Ada 2005に基づくSPARK言語(SPARK83、SPARK95、SPARK2005)の3つのバージョンがありました。
Ada 2012に基づくSPARK言語の第4版SPARK 2014は、2014年4月30日にリリースされました。SPARK 2014は、言語とサポート検証ツールの完全な再設計です。
SPARK言語は、静的および動的検証の両方に適した形式でコンポーネントの仕様を記述するために契約を使用するAda言語の明確に定義されたサブセットで構成されています。
SPARK83 / 95/2005では、契約はAdaコメントでエンコードされています(標準のAdaコンパイラでは無視されます)が、SPARK "Examiner"とそれに関連するツールで処理されます。
対照的に、SPARK 2014は、Ada 2012に組み込まれた「アスペクト」構文を使用して契約を表現し、それらを言語の核としています。 SPARK 2014(GNATprove)の主なツールは、GNAT / GCCインフラストラクチャに基づいており、GNAT Ada 2012のフロントエンドのほとんどを再利用しています。