SPARK（プログラミング言語）

スパーク

パラダイム	マルチパラダイム
開発者	AltranとAdaCore
安定リリース	コミュニティ 2021 / 2021年6月1日; 3年前 (2021-06-01)
タイピングの規律	静的、強い、安全、主格
OS	クロスプラットフォーム: Linux、Microsoft Windows、Mac OS X
ライセンス	GPLv3
Webサイト	SPARKについて
主な実装
SPARK Pro、SPARK GPL エディション、SPARK コミュニティ
影響を受けた
エイダ、エッフェル

SPARK は、 Adaプログラミング言語に基づいて正式に定義された コンピュータ プログラミング言語であり、予測可能で信頼性の高い操作が不可欠なシステムで使用される高整合性ソフトウェアの開発を目的としています。安全性、セキュリティ、またはビジネス整合性を要求するアプリケーションの開発を容易にします。

もともと、SPARK 言語には、それぞれ Ada 83、Ada 95、Ada 2005 に基づく 3 つのバージョン (SPARK83、SPARK95、SPARK2005) がありました。

SPARK 言語の 4 番目のバージョンである SPARK 2014 は、Ada 2012 に基づいて、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 フロントエンドのほぼ全体を再利用します。

SPARK は、Ada の長所を活用しながら、その潜在的な曖昧さや安全でない構造をすべて排除しようとします。SPARK プログラムは、設計上、曖昧さがないように意図されており、その動作は Adaコンパイラの選択によって影響を受けないようにする必要があります。これらの目標は、Ada のより問題のある機能 (無制限の並列タスクなど) の一部を省略し、アプリケーションの設計者の意図とプログラムの特定のコンポーネントに対する要件をエンコードする契約を導入することで部分的に達成されます。

これらのアプローチを組み合わせることで、SPARK は次の設計目標を達成できます。

• 論理的妥当性
• 厳密な正式な定義
• 単純な意味論
• 安全
• 表現力
• 検証可能性
• 制限されたリソース（空間と時間）要件。
• 最小限のランタイムシステム要件

以下の Ada サブプログラム仕様を検討してください。

手順Increment (X : in out Counter_Type);

純粋な Ada では、変数がX1 または 1000 増加されるか、何らかのグローバル カウンタが に設定されX、カウンタの元の値が返されるかX、または に対してまったく何も行われない可能性がありますX。

SPARK 2014 では、サブプログラムが実際に何を行うかに関する追加情報を提供するための契約がコードに追加されます。たとえば、上記の仕様を次のように変更できます。

手順Increment (X : in out Counter_Type)
  グローバル=> null、
       依存 => (X => X);

Incrementこれは、プロシージャがグローバル変数を使用せず (更新も読み取りも行わず)、 の新しい値の計算に使用される唯一のデータ項目がそれ自体であることXを指定しますX。

あるいは、設計者は次のように指定することもできます。

手順Increment (X : in out Counter_Type)
   with Global => (In_Out => Count)、
       依存 => (Count => (Count, X)、
                   X => null);

これは、が と同じパッケージ内のIncrementグローバル変数を使用すること、 のエクスポートされた値がおよびのインポートされた値に依存すること、 のエクスポートされた値がどの変数にもまったく依存せず、定数データのみから導出されることを指定します。 CountIncrementCountCountXX

GNATprove を仕様と対応するサブプログラムの本体で実行すると、サブプログラムの本体が分析され、情報フローのモデルが構築されます。次に、このモデルが注釈で指定されたモデルと比較され、矛盾があればユーザーに報告されます。

これらの仕様は、サブプログラムが呼び出されたときに保持する必要があるさまざまなプロパティ (前提条件) またはサブプログラムの実行が完了した後に保持されるさまざまなプロパティ (事後条件)をアサートすることでさらに拡張できます。たとえば、次のように言うことができます。

手順Increment (X : in out Counter_Type)
  グローバル=> null、
       依存 => (X => X)、
       Pre => X < Counter_Type'Last、
       投稿 => X = X'Old + 1;

これにより、 がそれX自体からのみ派生することを指定するだけでなく、 beforeIncrementが呼び出される値はその型の最後の可能な値よりも厳密に小さくなければならないこと (結果がオーバーフローXしないことを保証するため)、 after が の初期値+ 1 に等しくなることも指定します。 XX

GNATprove は、検証条件(VC)のセットを生成することもできます。これらの条件は、特定のプロパティが特定のサブプログラムに当てはまるかどうかを確認するために使用されます。少なくとも、GNATprove は、次のようなすべての実行時エラーがサブプログラム内で発生しないことを確認する VC を生成します。

• 配列インデックスが範囲外です
• 型範囲違反
• ゼロ除算
• 数値オーバーフロー。

サブプログラムに事後条件またはその他のアサーションが追加された場合、GNATprove は、これらのプロパティがサブプログラムを通るすべての可能なパスに当てはまることをユーザーが示すことを要求する VC も生成します。

GNATprove は、内部的には Why3 中間言語と VC ジェネレーター、およびCVC4、Z3、およびAlt-Ergo定理証明器を使用して VC を実行します。他の証明器 (対話型証明チェッカーを含む) の使用も、Why3 ツールセットの他のコンポーネントを通じて可能です。

SPARKの最初のバージョン（Ada 83ベース）は、サウサンプトン大学（英国国防省の支援を受けて）でバーナード・カレとトレバー・ジェニングスによって開発されました。SPARKという名前は、Pascalプログラミング言語のSPADEサブセットにちなんで、SPADE Adaカーネルに由来しています。^[1]

その後、この言語は、最初は Program Validation Limited によって、次に Praxis Critical Systems Limited によって、徐々に拡張および改良されました。2004 年、Praxis Critical Systems Limited は社名を Praxis High Integrity Systems Limited に変更しました。2010 年 1 月、同社はAltran Praxisになりました。

2009 年初頭、Praxis は AdaCore と提携し、GPL の条件に基づいて「SPARK Pro」をリリースしました。その後、2009 年 6 月にFOSSおよび学術コミュニティを対象とした SPARK GPL Edition 2009 がリリースされました。

2010年6月、Altran-Praxisは、2015年に完了予定の 米国の月探査プロジェクトCubeSatのソフトウェアにSPARKプログラミング言語が使用されることを発表しました。

2013年1月、Altran-Praxisは社名をAltranに変更し、2021年4月にCapgemini Engineering（AltranとCapgeminiの合併後）となりました。

SPARK 2014 の最初の Pro リリースは 2014 年 4 月 30 日に発表され、その後すぐにFLOSSおよび学術コミュニティ を対象とした SPARK 2014 GPL エディションがリリースされました。

SPARK は、商業航空 (ロールスロイス トレントシリーズ ジェット エンジン、ARINC ACAMS システム、ロッキード マーティン C130J )、軍用航空 (ユーロファイター タイフーン、ハリアー GR9、アエルマッキ M346 )、航空交通管理 (英国 NATS iFACTS システム)、鉄道 (多数の信号アプリケーション)、医療 (LifeFlow心室補助装置)、宇宙アプリケーション (バーモント工科大学の CubeSat プロジェクト) など、安全性が極めて重要ないくつかのシステムで使用されています。^{[出典が必要]}

SPARK は、セキュア システムの開発にも使用されています。ユーザーには、Rockwell Collins (Turnstile および SecureOne クロスドメイン ソリューション)、オリジナルのMULTOS CA の開発、NSA Tokeneer デモンストレーター、secunet マルチレベル ワークステーション、Muen 分離カーネル、Genodeブロック デバイス暗号化プログラムなどがあります。

2010年8月、Altran Praxisの主任エンジニアであるRod Chapmanは、SHA-3の候補の1つであるSkeinをSPARKに実装しました。SPARKとCの実装のパフォーマンスを比較し、慎重に最適化した結果、SPARKバージョンはCよりも約5〜10％遅くなることがありました。その後、GCCのAdaミドルエンド（AdaCoreのEric Botcazouによって実装）が改良され、SPARKコードはCとパフォーマンスがまったく同じになりました。^[2]

NVIDIAもセキュリティクリティカルなファームウェアの実装にSPARKを採用しています。^[3]

2020年、ロッド・チャップマンはSPARK 2014でTweetNaCl暗号ライブラリを再実装しました。^[4]ライブラリのSPARKバージョンは、型安全性、メモリ安全性、およびいくつかの正確性プロパティの完全な自動アクティブ証明を備えており、全体を通して定数時間アルゴリズムを保持しています。SPARKコードはTweetNaClよりも大幅に高速です。

• Z表記
• Javaモデリング言語

• バーンズ、ジョン(2012)。SPARK: 実証済みの高信頼性ソフトウェアへのアプローチ。Altran Praxis。ISBN 978-0-9572905-1-8。

• McCormick, John W.; Chapin, Peter C. (2015)。SPARK による高信頼性アプリケーションの構築。ケンブリッジ大学出版局。ISBN 978-1-107-65684-0。

• Ross, Philip E. ( 2005 年 9 月)。「The Exterminators」。IEEE  Spectrum 42 ( 9): 36–41。doi : 10.1109 /MSPEC.2005.1502527。ISSN 0018-9235。S2CID 26369398  。

• SPARK 2014 コミュニティサイト
• SPARK Proウェブサイト
• SPARK Libre (GPL) 版ウェブサイト
• アルトラン
• 構築による正確性: 高信頼性ソフトウェアの宣言 アーカイブ 2012 年 10 月 30 日、Wayback Machineで公開
• 英国のセーフティクリティカルシステムクラブ
• C仕様言語（Frama C）との比較
• Tokeneer プロジェクトページ
• Muen カーネルの公開リリース
• LifeFlow LVAD プロジェクト
• VTU キューブサット プロジェクト