タグ「SPARK」の記事
「SPARK」タグが付いた記事の一覧です(5件)。新しい順に掲載しています。
-
Alire で Ada のプロジェクトを始める ── プロジェクト作成、依存の追加、ビルドプロファイル、GNATproveまで
AdaのパッケージマネージャーAlireで、プロジェクトの作成、GNATの自動取得、依存クレートの追加、ビルドプロファイルの切り替え、GNATproveによる証明までを、alr 2.1で実行した出力とともに説明します。
-
Ada と Rust の安全性の考え方の違い ── 型・オーバーフロー・所有権・データ競合・形式検証を実際に動かして比べる
Ada と Rust はどちらも安全性を重視する言語ですが、誤りを止める場所が違います。値の範囲、整数オーバーフロー、メモリ、データ競合、検査を外す仕組み、形式検証の6点を、GNAT・GNATprove・rustc で実際に動かして比べます。
-
AIが書いたコードをSPARKで証明する ── 人が契約を書き、GNATproveで確かめる
AIが書いたAdaの関数に事前条件と事後条件を付け、GNATproveで証明する手順を実行例で示します。失敗メッセージの読み方、弱い契約のまま通る証明、レビューで人が見る箇所をまとめます。
-
SPARKによる形式検証入門 ── Adaの契約から数学的証明へ
Adaのサブセット言語SPARKによる形式検証の実践的な入門記事です。契約(Pre/Post)から証明へステップアップする方法、GNATproveの使い方、ループ不変条件、データフロー契約、証明レベル、そして実プロジェクトへの適用方法までを整理します。
-
Ada言語の魅力 ── 型で設計を語り、数十年動き続けるソフトウェアを支える言語
Ada言語の魅力を紹介します。強い型付け、範囲制約、パッケージによる仕様と実装の分離、契約による設計、言語組み込みのタスク、SPARKによる形式検証、GNATとAlireでの開発環境まで、高信頼ソフトウェアを支える設計思想を整理します。