知識マップ: Ada と Rust の安全性の考え方の違い ── 型・オーバーフロー・所有権・データ競合・形式検証を実際に動かして比べる

記事「Ada と Rust の安全性の考え方の違い ── 型・オーバーフロー・所有権・データ競合・形式検証を実際に動かして比べる」の主張を、概念と関係(エッジ)に分解した知識グラフの全体です。各関係には根拠・確認日・確度が付いています。

Adaは範囲制約やモジュラー型で値の範囲を型に書き、アクセシビリティ規則でダングリング参照を防ぎ、保護オブジェクトでデータ競合を防ぐ。ただしUnchecked_Deallocationの後の使用や保護しない共有変数はコンパイラが止めない。SPARKはRustにならった所有権ポリシーを持ち、GNATproveがオーバーフロー・メモリリーク・データ競合を検査する。Rustは所有権と借用チェッカー、SendとSyncでダングリング参照とデータ競合をコンパイル時に止め、整数オーバーフローの扱いはoverflow-checksで決まる。Rustの形式検証にはKani・Verus・Creusot・Prustiがある。

flowchart LR
    accTitle: AdaとRustの安全性の知識マップ
    accDescr: Adaの範囲制約・アクセシビリティ規則・保護オブジェクト、SPARKの所有権ポリシーとGNATprove、Rustの所有権・借用チェッカー・Send/Sync・unsafeが、整数オーバーフロー・ダングリング参照・データ競合・メモリリークとどう関係するかを示します。
    ada["Ada(プログラミング言語)"]
    rust["Rust(プログラミング言語)"]
    spark["SPARK"]
    ada_strong_typing["Adaの強い型付け"]
    ada_range_constraint["範囲制約(range constraint)"]
    ada_modular_type["モジュラー型"]
    newtype_pattern["newtypeパターン"]
    integer_overflow["整数オーバーフロー"]
    cargo_overflow_checks["overflow-checks(Cargo)"]
    gnatprove["GNATprove"]
    rust_ownership["所有権(Rust)"]
    rust_borrow_checker["借用チェッカー"]
    dangling_pointer["ダングリング参照"]
    data_race["データ競合(data race)"]
    ada_access_type["アクセス型"]
    ada_accessibility_rules["アクセシビリティ規則"]
    ada_unchecked_deallocation["Ada.Unchecked_Deallocation"]
    spark_ownership_policy["所有権ポリシー(SPARK)"]
    memory_leak["メモリリーク"]
    formal_verification["形式検証"]
    rust_send["Send(Rust)"]
    rust_sync["Sync(Rust)"]
    protected_object["保護オブジェクト(protected object)"]
    ravenscar_profile["Ravenscarプロファイル"]
    jorvik_profile["Jorvikプロファイル"]
    unsafe_rust["unsafe Rust"]
    kani["Kani"]
    verus["Verus"]
    creusot["Creusot"]
    prusti["Prusti"]
    smt_solver["SMTソルバ(自動証明器)"]
    why3["Why3"]
    ada -->|"実装を担う"| ada_strong_typing
    ada -->|"実装を担う"| ada_range_constraint
    ada -->|"実装を担う"| ada_modular_type
    rust -->|"利用する"| newtype_pattern
    integer_overflow -->|"で構成できる"| cargo_overflow_checks
    integer_overflow -->|"で確認できる"| gnatprove
    rust -->|"実装を担う"| rust_ownership
    rust -->|"実装を担う"| rust_borrow_checker
    rust_borrow_checker -->|"防止する"| dangling_pointer
    rust_borrow_checker -->|"防止する"| data_race
    ada -->|"実装を担う"| ada_access_type
    ada -->|"実装を担う"| ada_accessibility_rules
    ada_accessibility_rules -.->|"防止する"| dangling_pointer
    ada_unchecked_deallocation -->|"前提とする"| ada_access_type
    ada_unchecked_deallocation -->|"原因になり得る"| dangling_pointer
    spark -->|"実装を担う"| spark_ownership_policy
    spark_ownership_policy -.->|"防止する"| dangling_pointer
    memory_leak -->|"で確認できる"| gnatprove
    spark -->|"実装を担う"| formal_verification
    spark -->|"利用する"| gnatprove
    rust -->|"実装を担う"| rust_send
    rust -->|"実装を担う"| rust_sync
    rust_send -->|"防止する"| data_race
    rust_sync -->|"防止する"| data_race
    protected_object -->|"防止する"| data_race
    data_race -.->|"で確認できる"| gnatprove
    spark -.->|"前提とする"| ravenscar_profile
    spark -.->|"利用する"| jorvik_profile
    rust -->|"実装を担う"| unsafe_rust
    unsafe_rust -.->|"原因になり得る"| dangling_pointer
    rust -.->|"で確認できる"| kani
    rust -.->|"で確認できる"| verus
    rust -.->|"で確認できる"| creusot
    rust -.->|"で確認できる"| prusti
    integer_overflow -->|"で確認できる"| kani
    verus -->|"利用する"| smt_solver
    creusot -->|"利用する"| why3

概念間の関係(全37件)

図と同じ関係を文章でも列挙します。表示している文と機械可読な意味データ(RDFa)は同じ要素に載っています。確度が「確立した関係」のものは直接の関係として、「条件付きの関係」のものは成立条件つきの言明(rdf:Statement)として表現しています。

Ada(プログラミング言語)はAdaの強い型付けの実装を担います。Float から type … is new で作った Meters と Feet は別の型になり、Feet の値を Meters の引数に渡すとコンパイルエラーになる。 / 確度: 確立した関係 / 確認日: 2026-11-01 出典
Ada(プログラミング言語)は範囲制約(range constraint)の実装を担います。subtype Percent is Integer range 0 .. 100 のように範囲を型に書くと、その型への代入のたびに範囲が検査され、範囲外なら Constraint_Error になる。 / 確度: 確立した関係 / 確認日: 2026-11-01 出典
Ada(プログラミング言語)はモジュラー型の実装を担います。mod で宣言した型は演算結果が範囲を超えると剰余で折り返す。符号付き整数型は範囲を超えると Constraint_Error になる。 / 確度: 確立した関係 / 確認日: 2026-11-01 出典
Rust(プログラミング言語)はnewtypeパターンを利用します。Rust には型に値の範囲を書く構文がなく、1要素の構造体で包んだ newtype で単位の取り違えを防ぎ、範囲は生成関数で確かめる。 / 確度: 確立した関係 / 確認日: 2026-11-01 出典
整数オーバーフローはoverflow-checks(Cargo)で構成できます。Rust で整数オーバーフローをパニックにするか折り返すかは overflow-checks で決まる。既定は dev で true、release で false で、言語仕様は検査のないビルドでパニックか2の補数の折り返しかを実装に任せている。 / 確度: 確立した関係 / 確認日: 2026-11-01 出典出典
整数オーバーフローはGNATproveで確認できます。GNATprove は SPARK のコードについて、整数の演算がオーバーフローしないことを証明の対象にする。 / 確度: 確立した関係 / 確認日: 2026-11-01 出典
Rust(プログラミング言語)は所有権(Rust)の実装を担います。値には所有者が1つだけあり、所有権を移した後の変数を使うとコンパイルエラー(E0382)になる。 / 確度: 確立した関係 / 確認日: 2026-11-01 出典
Rust(プログラミング言語)は借用チェッカーの実装を担います。Rust コンパイラは借用チェッカーでスコープを比べ、借用が有効かを判断する。 / 確度: 確立した関係 / 確認日: 2026-11-01 出典
借用チェッカーはダングリング参照を防ぎます。スコープを出た変数への参照を残す書き方は、借用チェッカーがコンパイルエラー(E0597)にする。 / 確度: 確立した関係 / 確認日: 2026-11-01 出典
借用チェッカーはデータ競合(data race)を防ぎます。可変の参照は同時に1つしか持てないので、複数のスレッドが同じ変数を書き換えるコードはコンパイルエラー(E0499)になる。 / 確度: 確立した関係 / 確認日: 2026-11-01 出典
Ada(プログラミング言語)はアクセス型の実装を担います。Ada のポインタはアクセス型と呼ばれ、new で確保した領域やaliasedなオブジェクトを指す。 / 確度: 確立した関係 / 確認日: 2026-11-01 出典
Ada(プログラミング言語)はアクセシビリティ規則の実装を担います。Ada の言語仕様はアクセシビリティ規則を定め、多くの場合コンパイル時に検査する。 / 確度: 確立した関係 / 確認日: 2026-11-01 出典
アクセシビリティ規則はダングリング参照を防ぎます。ローカル変数を指すアクセス値をより外側のアクセス型の変数に入れるコードはコンパイルエラーになる。ただし Unchecked_Access などの unchecked な機能を使った場合と、Unchecked_Deallocation で解放した後の使用は防がない。 / 確度: 条件付きの関係 / 確認日: 2026-11-01 出典出典
Ada.Unchecked_Deallocationはアクセス型を前提とします。Ada.Unchecked_Deallocation は解放する対象の型とアクセス型を指定してインスタンス化する。 / 確度: 確立した関係 / 確認日: 2026-11-01 出典
Ada.Unchecked_Deallocationはダングリング参照の原因になることがあります。Free(X) は X だけを null にし、同じ領域を指す別のアクセス変数は残る。それを参照外しした実行は誤った実行になる。 / 確度: 確立した関係 / 確認日: 2026-11-01 出典
SPARKは所有権ポリシー(SPARK)の実装を担います。SPARK は Rust と同じようにメモリの所有権ポリシーを強制し、アクセス型の代入で所有権を左辺に移す。 / 確度: 確立した関係 / 確認日: 2026-11-01 出典
所有権ポリシー(SPARK)はダングリング参照を防ぎます。所有権を移した後の変数を通した書き込みは、GNATprove が移動後の使用としてエラーにする。SPARK_Mode を Off にした部分は解析されない。 / 確度: 条件付きの関係 / 確認日: 2026-11-01 出典
メモリリークはGNATproveで確認できます。GNATprove は代入と宣言の寿命の終わりでメモリを漏らしていないかを検査し、解放しないコードにリークの可能性を報告する。 / 確度: 確立した関係 / 確認日: 2026-11-01 出典
SPARKは形式検証の実装を担います。SPARK は Ada のサブセットで、契約や実行時エラーの不在を GNATprove で証明する。 / 確度: 確立した関係 / 確認日: 2026-11-01 出典
SPARKはGNATproveを利用します。SPARK のコードの所有権・メモリリーク・オーバーフロー・データ競合の検査は GNATprove が行う。 / 確度: 確立した関係 / 確認日: 2026-11-01 出典
Rust(プログラミング言語)はSend(Rust)の実装を担います。スレッドに値を渡せるかは Send で表し、Send を実装しない Rc を thread::spawn に渡すとコンパイルエラー(E0277)になる。 / 確度: 確立した関係 / 確認日: 2026-11-01 出典
Rust(プログラミング言語)はSync(Rust)の実装を担います。複数のスレッドから参照してよい型かは Sync で表す。 / 確度: 確立した関係 / 確認日: 2026-11-01 出典
Send(Rust)はデータ競合(data race)を防ぎます。Rc は参照カウントを同期せずに更新するので Send を実装しておらず、別スレッドへ渡すコードはコンパイルできない。 / 確度: 確立した関係 / 確認日: 2026-11-01 出典
Sync(Rust)はデータ競合(data race)を防ぎます。複数スレッドから参照される値は Sync を実装する型に限られる。 / 確度: 確立した関係 / 確認日: 2026-11-01 出典
保護オブジェクト(protected object)はデータ競合(data race)を防ぎます。保護オブジェクトの操作を通して更新したカウンタは毎回正しい値になった。保護しない共有変数の同時更新はコンパイルは通るが誤った実行になる。 / 確度: 確立した関係 / 確認日: 2026-11-01 出典出典
データ競合(data race)はGNATproveで確認できます。Ravenscar または Jorvik プロファイルの SPARK コードで、複数のタスクが同期されていない変数にアクセスすると、GNATprove がデータ競合の可能性を報告する。 / 確度: 条件付きの関係 / 確認日: 2026-11-01 出典
SPARKはRavenscarプロファイルを前提とします。SPARK で並行処理を書くには Ravenscar プロファイルが必要で、代わりに Jorvik プロファイルも使える。 / 確度: 条件付きの関係 / 確認日: 2026-11-01 出典
SPARKはJorvikプロファイルを利用します。GNATprove は Ada 2022 で定義された Jorvik プロファイルにも対応しており、並行処理の SPARK コードで Ravenscar の代わりに指定できる。 / 確度: 条件付きの関係 / 確認日: 2026-11-01 出典
Rust(プログラミング言語)はunsafe Rustの実装を担います。unsafe で使えるようになるのは生ポインタの参照外しなど5つの操作だけで、unsafe の外で生ポインタを参照外しするとコンパイルエラー(E0133)になる。#![forbid(unsafe_code)] で unsafe ブロックを禁止できる。 / 確度: 確立した関係 / 確認日: 2026-11-01 出典
unsafe Rustはダングリング参照の原因になることがあります。生ポインタは有効なメモリを指す保証がなく、unsafe での参照外しはコンパイラが検査しない。 / 確度: 条件付きの関係 / 確認日: 2026-11-01 出典
Rust(プログラミング言語)はKaniで確認できます。Kani はモデル検査で Rust のプログラムの未定義動作・パニック・算術オーバーフロー・アサーションを検査する。この記事では実行していない。 / 確度: 条件付きの関係 / 確認日: 2026-11-01 出典
Rust(プログラミング言語)はVerusで確認できます。Verus は Rust の構文で書いた仕様を定理証明で検証するが、Rust のすべての機能への対応は目指していない。この記事では実行していない。 / 確度: 条件付きの関係 / 確認日: 2026-11-01 出典
Rust(プログラミング言語)はCreusotで確認できます。Creusot は Rust のコードにパニック・オーバーフロー・アサーションの失敗がないことを検証する。この記事では実行していない。 / 確度: 条件付きの関係 / 確認日: 2026-11-01 出典
Rust(プログラミング言語)はPrustiで確認できます。Prusti は unsafe の機能を含まない Rust の一部を対象に、機能上の性質を検証する。この記事では実行していない。 / 確度: 条件付きの関係 / 確認日: 2026-11-01 出典
整数オーバーフローはKaniで確認できます。Kani は算術オーバーフローを検査の対象に含む。 / 確度: 確立した関係 / 確認日: 2026-11-01 出典
VerusはSMTソルバ(自動証明器)を利用します。Verus は自動証明器の Z3 を使って仕様を満たすことを確かめる。 / 確度: 確立した関係 / 確認日: 2026-11-01 出典
CreusotはWhy3を利用します。Creusot は Rust のコードを Why3 の中間言語 Coma に変換し、Why3 で検証条件を扱う。 / 確度: 確立した関係 / 確認日: 2026-11-01 出典

主要概念の定義

Ada(プログラミング言語): 1970年代後半にアメリカ国防総省の主導で標準化された、強い型付けと高信頼性を重視する汎用プログラミング言語。最新標準はAda 2022。
Rust(プログラミング言語): 所有権と借用の規則をコンパイラが検査することで、ガベージコレクションを使わずにメモリを管理するシステムプログラミング言語。
SPARK: プログラムの性質を数学的に証明できるように設計された、Adaのサブセット(部分言語)とそのツール群。
整数オーバーフロー: 整数の演算結果が、その型で表せる範囲を超えること。言語と設定によって、例外・パニック・折り返しのいずれかになる。Adaでは、値が型の基本範囲に収まるかを確かめるOverflow_Checkに失敗すると、実行時にConstraint_Errorが送出される。
借用チェッカー: スコープを比べて借用(参照)が有効かを判断し、規則に反する借用をコンパイルエラーにするRustコンパイラの検査。
アクセシビリティ規則: アクセス型と指す先のオブジェクトの寿命(アクセシビリティレベル)を比べ、指す先より長く残るアクセス値を作らせないAdaの規則。静的に違反が分かればコンパイルエラーになり、実行時の検査(accessibility check)に失敗するとProgram_Errorが発生する。
Ada.Unchecked_Deallocation: newで確保したオブジェクトを明示的に解放するために、オブジェクトの型とアクセス型を渡してインスタンス化するAdaの標準のジェネリック手続き。解放に渡した変数はnullになるが、同じオブジェクトを指すほかのアクセス値は検査しない。
所有権ポリシー(SPARK): アクセス型の代入で所有権を移し、移動元からのアクセスを禁じるSPARKのメモリ所有権の規則。Rustにならったもので、GNATproveが検査する。
メモリリーク: 確保したメモリを解放し忘れ、Private BytesやCommitが増え続ける現象。
Send(Rust): その型の値の所有権をスレッド間で移せることを示すRustのマーカートレイト。
Sync(Rust): その型を複数のスレッドから参照しても安全であることを示すRustのマーカートレイト。
保護オブジェクト(protected object): procedure・function・entryの3種の操作を通じてのみ内部データへアクセスさせ、排他制御を言語が保証するAda 95で導入された機構。
データ競合(data race): 複数のタスクが同じメモリ位置に同時アクセスし、少なくとも一方が書き込みであるために結果が未定義になる状態である。
unsafe Rust: 生ポインタの参照外しなど5つの操作を許すRustの仕組み。unsafeの中でも借用チェッカーなどの検査は働く。
Verus: Rustの構文で書いた仕様を、実行時の検査を加えずに定理証明でRustのコードに対して検証するツール。
Creusot: RustのコードをWhy3の中間言語Comaに変換して検証する、Rustの演繹的な検証器。

機械可読データ

JSON-LD / Turtle ── この記事の知識グラフ全体
概念一覧 / 語彙(述語)の定義

このデータセットについて

作成: 合同会社小村ソフト
ライセンス: CC BY 4.0 ── 出典(合同会社小村ソフト)とライセンスへのリンクを明示し、改変した場合はその旨を示すことを条件に、再配布・改変を含めて再利用できます
最終確認日: 2026-11-01 ── 収録する関係のうち、最後に出典と照合した日

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