GNATprove

AdaCoreが提供する、SPARKコードの契約や表明を自動証明器で検証するコマンドラインツールである。

概念URI

https://comcomponent.com/knowledge/gnatprove/

別名・表記

gnatprove コマンド

上位概念

SPARK

最終確認日

2026-08-01

機械可読データ

JSON-LD

この概念が関わる関係

• SPARKはGNATproveを利用します。SPARKコードの検証には、AdaCoreが提供するGNATproveというツールを使う / 確度: 確立した関係 / 確認日: 2026-08-01 出典
• GNATproveはAda(プログラミング言語)を前提とします。GNATproveはGNATツールチェーンに同梱されて提供され、Adaのコンパイル環境を前提とする / 確度: 確立した関係 / 確認日: 2026-08-01 出典
• GNATproveはWhy3を利用します。GNATproveは契約や表明をいったんWhy3の中間言語に変換してから証明器に渡す / 確度: 確立した関係 / 確認日: 2026-08-01 出典
• Silverレベル(AoRTE)はGNATproveで確認できます。Silverレベルが達成されている(範囲外・オーバーフロー・ゼロ除算が起きない)ことはGNATproveの証明で確認できる / 確度: 確立した関係 / 確認日: 2026-08-01 出典
• データフロー契約(Global/Depends)はGNATproveで確認できます。Global/Depends契約が意図通りであることはGNATproveのフロー解析(Bronzeレベル)で確認できる / 確度: 確立した関係 / 確認日: 2026-08-01 出典
• 契約による設計(Pre/Post)はGNATproveで確認できます。Pre/Post契約が満たされることはGNATproveの証明で確認できる / 確度: 確立した関係 / 確認日: 2026-08-01 出典

この概念を扱う記事

• SPARKによる形式検証入門 ── Adaの契約から数学的証明へ(言及)

一次資料

• https://docs.adacore.com/spark2014-docs/html/ug/

このページはサイトの知識グラフ(_data/knowledge/)から自動生成されています。誤りの指摘はお問い合わせからお願いします。