タグ「GNATprove」の記事

画像処理の境界外アクセスをSPARKで証明する ── 2値化・平滑化・ラベリングとCとの速度比較

2026年11月10日 01:00

画像処理のコードが画像の外を読み書きしないことを、SPARKのGNATproveで証明します。2値化、3×3の平滑化、ラベリングを例に、証明の書き方と証明していない範囲、検査を外したときのCとの速度の差を実測でまとめます。

Alire で Ada のプロジェクトを始める ── プロジェクト作成、依存の追加、ビルドプロファイル、GNATproveまで

2026年11月01日 12:40

AdaのパッケージマネージャーAlireで、プロジェクトの作成、GNATの自動取得、依存クレートの追加、ビルドプロファイルの切り替え、GNATproveによる証明までを、alr 2.1で実行した出力とともに説明します。

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

2026年06月13日 00:00

Adaのサブセット言語SPARKによる形式検証の実践的な入門記事です。契約(Pre/Post)から証明へステップアップする方法、GNATproveの使い方、ループ不変条件、データフロー契約、証明レベル、そして実プロジェクトへの適用方法までを整理します。