SPARK_Mode

コードをSPARKとして扱うかを指定するアスペクトとプラグマ。Onの部分はSPARKの制限に従ってGNATproveが解析し、Offの部分は解析されず、SPARKの制限にも従う必要がない。

概念URI

https://comcomponent.com/knowledge/spark-mode/

別名・表記

SPARK_Mode => Off / SPARK_Mode => On

上位概念

SPARK

最終確認日

2026-08-01

機械可読データ

JSON-LD

この概念が関わる関係

• GNATproveはSPARK_Modeで構成できます。GNATproveが解析する範囲はSPARK_Modeで決まり、SPARK_Mode => Offにした本体は解析されない / 確度: 確立した関係 / 確認日: 2026-11-01 出典

この概念を扱う記事

• AIが書いたコードをSPARKで証明する ── 人が契約を書き、GNATproveで確かめる(言及)

一次資料

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

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