Silverレベル(AoRTE)

範囲外アクセス・オーバーフロー・ゼロ除算などの実行時エラーが起きないことを証明する、証明レベルのうち実務上の既定目標とされる段階である。

概念URI

https://comcomponent.com/knowledge/spark-silver-level/

別名・表記

Absence of Run-time Errors / AoRTE

上位概念

証明レベル(Stone〜Platinum)

最終確認日

2026-08-01

機械可読データ

JSON-LD

この概念が関わる関係

• Silverレベル(AoRTE)はSPARKに対する本記事の推奨です。実行時エラーが起きないことを証明するSilverレベルは、SPARK導入における実務上の既定の目標として推奨される / 確度: 確立した関係 / 確認日: 2026-08-01 出典
• Silverレベル(AoRTE)はGNATproveで確認できます。Silverレベルが達成されている(範囲外・オーバーフロー・ゼロ除算が起きない)ことはGNATproveの証明で確認できる / 確度: 確立した関係 / 確認日: 2026-08-01 出典

この概念を扱う記事

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

一次資料

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

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