契約による設計(Pre/Post)

サブプログラムの入口での前提条件(Pre)と、出口で保証する性質(Post)を宣言的に記述する、Ada 2012の契約機構である。

概念URI

https://comcomponent.com/knowledge/design-by-contract/

別名・表記

Design by Contract / 事前条件・事後条件

上位概念

Ada(プログラミング言語)

最終確認日

2026-08-01

機械可読データ

JSON-LD

この概念が関わる関係

• SPARKは契約による設計(Pre/Post)を前提とします。SPARKの証明のうち、書いた性質の証明はPre/Postで書かれた契約を証明の入力とすることを前提とする。ただしオーバーフロー・範囲外アクセス・ゼロ除算などの実行時エラー不在(AoRTE)の証明は、明示的なPre/Post契約を書かなくても型の範囲制約などから成立し得る / 確度: 条件付きの関係 / 確認日: 2026-08-01 出典
• 契約による設計(Pre/Post)はGNATproveで確認できます。Pre/Post契約が満たされることはGNATproveの証明で確認できる / 確度: 確立した関係 / 確認日: 2026-08-01 出典

この概念を扱う記事

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

一次資料

• https://www.adaic.org/ada-resources/standards/ada22/

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