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

サブプログラムに事前条件(Pre)・事後条件(Post)・型不変条件を言語機能として付与できる、Ada 2012で導入された仕組み。

概念URI

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

別名・表記

Design by Contract / Ada 2012契約

最終確認日

2026-08-01

機械可読データ

JSON-LD

この概念が関わる関係

• Ada(プログラミング言語)は契約による設計(Pre/Post条件)の実装を担います。Ada 2012では、事前条件(Pre)・事後条件(Post)・型不変条件による契約による設計が言語仕様に組み込まれた。 / 確度: 確立した関係 / 確認日: 2026-08-01 出典
• SPARKは契約による設計(Pre/Post条件)を前提とします。実行時チェックとして書いたPre/Postの契約は、SPARKではそのまま数学的証明の対象になる。ただしオーバーフロー・範囲外アクセス・ゼロ除算などの実行時エラー不在(AoRTE)の証明は、明示的なPre/Post契約を書かなくても型の範囲制約などから成立し得る。 / 確度: 条件付きの関係 / 確認日: 2026-08-01 出典

この概念を扱う記事

• Ada言語の魅力 ── 型で設計を語り、数十年動き続けるソフトウェアを支える言語(言及)

一次資料

• https://ada-lang.io/docs/arm/AA-6/AA-6.1/

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