タグ「形式検証」の記事
「形式検証」タグが付いた記事の一覧です(3件)。新しい順に掲載しています。
-
Ada と Rust の安全性の考え方の違い ── 型・オーバーフロー・所有権・データ競合・形式検証を実際に動かして比べる
Ada と Rust はどちらも安全性を重視する言語ですが、誤りを止める場所が違います。値の範囲、整数オーバーフロー、メモリ、データ競合、検査を外す仕組み、形式検証の6点を、GNAT・GNATprove・rustc で実際に動かして比べます。
-
AIが書いたコードをSPARKで証明する ── 人が契約を書き、GNATproveで確かめる
AIが書いたAdaの関数に事前条件と事後条件を付け、GNATproveで証明する手順を実行例で示します。失敗メッセージの読み方、弱い契約のまま通る証明、レビューで人が見る箇所をまとめます。
-
SPARKによる形式検証入門 ── Adaの契約から数学的証明へ
Adaのサブセット言語SPARKによる形式検証の実践的な入門記事です。契約(Pre/Post)から証明へステップアップする方法、GNATproveの使い方、ループ不変条件、データフロー契約、証明レベル、そして実プロジェクトへの適用方法までを整理します。