SPARK Discovery

SPARK DiscoveryはGNAT Proユーザが形式手法を利用して、未実行での非初期化変数の確認、データと情報のフローの正しさ、コードにランタイムエラーがないことなどの検証ができます。

SPARK 言語はAda言語のサブセットで、形式手法に対応しているため、
データアーキテクチャの一貫性（変数とサブプログラムパラメータの適切な使用）から機能の正確性に至るまで、 プログラムのプロパティの検証に、数学を応用しています。

また、SPARK言語はAdaの契約（contract）ベースのプログラミング機能を使用しているため、動的（Adaセマンティクスsemantics）または静的（SPARK証明）にチェックされる契約（contract）と、テストならびに形式手法で検証されるコード両方を記述できます。

形式手法は、ソフトウェアアシュアランスのさまざまなレベルで適用できます。 SPARK Discoveryは、Stoneレベル（SPARKサブセットに準拠）、Bronzeレベル（Stoneレベルとデータフローの検証/非初期化変数の参照の確認）、およびSilverレベル（Bronzeレベル +ランタイムエラーが無いことの検証）の使用に適しています。

SPARK Pro製品は上位のGoldレベル（Silverレベル+整合性の証明）ならびにPlatinumレベル（Gold レベル+機能の正確さの証明）の検証に対応できます。 SPARK DiscoveryとSPARK Proの差異の詳細については、SPARKユーザーガイドを参照してください。