@prefix schema: <https://schema.org/> .
@prefix skos: <http://www.w3.org/2004/02/skos/core#> .
@prefix rdf: <http://www.w3.org/1999/02/22-rdf-syntax-ns#> .
@prefix ks: <https://comcomponent.com/vocab/> .

<https://comcomponent.com/blog/ada-vs-rust-safety/#article>
    schema:about <https://comcomponent.com/knowledge/ada/>, <https://comcomponent.com/knowledge/rust/>, <https://comcomponent.com/knowledge/spark/> ;
    schema:mentions <https://comcomponent.com/knowledge/ada-access-type/>, <https://comcomponent.com/knowledge/ada-accessibility-rules/>, <https://comcomponent.com/knowledge/ada-modular-type/>, <https://comcomponent.com/knowledge/ada-range-constraint/>, <https://comcomponent.com/knowledge/ada-strong-typing/>, <https://comcomponent.com/knowledge/ada-unchecked-deallocation/>, <https://comcomponent.com/knowledge/cargo-overflow-checks/>, <https://comcomponent.com/knowledge/creusot/>, <https://comcomponent.com/knowledge/dangling-pointer/>, <https://comcomponent.com/knowledge/data-race/>, <https://comcomponent.com/knowledge/formal-verification/>, <https://comcomponent.com/knowledge/gnatprove/>, <https://comcomponent.com/knowledge/integer-overflow/>, <https://comcomponent.com/knowledge/jorvik-profile/>, <https://comcomponent.com/knowledge/kani/>, <https://comcomponent.com/knowledge/memory-leak/>, <https://comcomponent.com/knowledge/newtype-pattern/>, <https://comcomponent.com/knowledge/protected-object/>, <https://comcomponent.com/knowledge/prusti/>, <https://comcomponent.com/knowledge/ravenscar-profile/>, <https://comcomponent.com/knowledge/rust-borrow-checker/>, <https://comcomponent.com/knowledge/rust-ownership/>, <https://comcomponent.com/knowledge/rust-send/>, <https://comcomponent.com/knowledge/rust-sync/>, <https://comcomponent.com/knowledge/smt-solver/>, <https://comcomponent.com/knowledge/spark-ownership-policy/>, <https://comcomponent.com/knowledge/unsafe-rust/>, <https://comcomponent.com/knowledge/verus/>, <https://comcomponent.com/knowledge/why3/> .

<https://comcomponent.com/knowledge/ada/> a skos:Concept ;
    skos:prefLabel "Ada(プログラミング言語)"@ja ;
    skos:definition "1970年代後半にアメリカ国防総省の主導で標準化された、強い型付けと高信頼性を重視する汎用プログラミング言語。最新標準はAda 2022。"@ja ;
    skos:altLabel "Ada言語"@ja ;
    skos:altLabel "Ada 2022" ;
    ks:implements <https://comcomponent.com/knowledge/ada-strong-typing/> ;
    ks:implements <https://comcomponent.com/knowledge/ada-range-constraint/> ;
    ks:implements <https://comcomponent.com/knowledge/ada-modular-type/> ;
    ks:implements <https://comcomponent.com/knowledge/ada-access-type/> ;
    ks:implements <https://comcomponent.com/knowledge/ada-accessibility-rules/> .

<https://comcomponent.com/knowledge/rust/> a skos:Concept ;
    skos:prefLabel "Rust(プログラミング言語)"@ja ;
    skos:definition "所有権と借用の規則をコンパイラが検査することで、ガベージコレクションを使わずにメモリを管理するシステムプログラミング言語。"@ja ;
    skos:altLabel "Rust言語"@ja ;
    ks:uses <https://comcomponent.com/knowledge/newtype-pattern/> ;
    ks:implements <https://comcomponent.com/knowledge/rust-ownership/> ;
    ks:implements <https://comcomponent.com/knowledge/rust-borrow-checker/> ;
    ks:implements <https://comcomponent.com/knowledge/rust-send/> ;
    ks:implements <https://comcomponent.com/knowledge/rust-sync/> ;
    ks:implements <https://comcomponent.com/knowledge/unsafe-rust/> .

<https://comcomponent.com/knowledge/spark/> a skos:Concept ;
    skos:prefLabel "SPARK"@ja ;
    skos:definition "プログラムの性質を数学的に証明できるように設計された、Adaのサブセット(部分言語)とそのツール群。"@ja ;
    skos:altLabel "SPARK Ada" ;
    skos:altLabel "GNATprove" ;
    ks:implements <https://comcomponent.com/knowledge/spark-ownership-policy/> ;
    ks:implements <https://comcomponent.com/knowledge/formal-verification/> ;
    ks:uses <https://comcomponent.com/knowledge/gnatprove/> .

<https://comcomponent.com/knowledge/ada-strong-typing/> a skos:Concept ;
    skos:prefLabel "Adaの強い型付け"@ja ;
    skos:definition "構造が同じでも別名で宣言した型を別の型として扱い、暗黙の混用をコンパイルエラーにするAdaの型システムの性質。"@ja ;
    skos:altLabel "strong typing" .

<https://comcomponent.com/knowledge/ada-range-constraint/> a skos:Concept ;
    skos:prefLabel "範囲制約(range constraint)"@ja ;
    skos:definition "型に値の範囲を持たせ、違反を実行時にConstraint_Error例外として検出するAdaの仕組み。配列アクセスの境界チェックにも使われる。"@ja ;
    skos:altLabel "subtype" ;
    skos:altLabel "Constraint_Error" .

<https://comcomponent.com/knowledge/ada-modular-type/> a skos:Concept ;
    skos:prefLabel "モジュラー型"@ja ;
    skos:definition "演算結果が範囲を超えると指定した法で剰余をとって折り返す、Adaの符号なし整数型。"@ja ;
    skos:altLabel "modular type" ;
    skos:altLabel "mod型"@ja .

<https://comcomponent.com/knowledge/newtype-pattern/> a skos:Concept ;
    skos:prefLabel "newtypeパターン"@ja ;
    skos:definition "既存の型を1要素の構造体で包んで別の型を作り、単位などの取り違えをコンパイル時に防ぐRustの書き方。"@ja ;
    skos:altLabel "newtype" .

<https://comcomponent.com/knowledge/integer-overflow/> a skos:Concept ;
    skos:prefLabel "整数オーバーフロー"@ja ;
    skos:definition "整数の演算結果が、その型で表せる範囲を超えること。言語と設定によって、例外・パニック・折り返しのいずれかになる。Adaでは、値が型の基本範囲に収まるかを確かめるOverflow_Checkに失敗すると、実行時にConstraint_Errorが送出される。"@ja ;
    skos:altLabel "Integer Overflow" ;
    skos:altLabel "integer overflow" ;
    skos:altLabel "算術オーバーフロー"@ja ;
    skos:altLabel "Overflow_Check" ;
    ks:configuredBy <https://comcomponent.com/knowledge/cargo-overflow-checks/> ;
    ks:verifiedBy <https://comcomponent.com/knowledge/gnatprove/> ;
    ks:verifiedBy <https://comcomponent.com/knowledge/kani/> .

<https://comcomponent.com/knowledge/cargo-overflow-checks/> a skos:Concept ;
    skos:prefLabel "overflow-checks(Cargo)"@ja ;
    skos:definition "実行時の整数オーバーフローでパニックさせるかを決めるCargoのプロファイル設定。既定はdevでtrue、releaseでfalse。"@ja ;
    skos:altLabel "-C overflow-checks" .

<https://comcomponent.com/knowledge/gnatprove/> a skos:Concept ;
    skos:prefLabel "GNATprove"@ja ;
    skos:definition "AdaCoreが提供する、SPARKコードの契約や表明を自動証明器で検証するコマンドラインツールである。"@ja ;
    skos:altLabel "gnatprove コマンド"@ja ;
    skos:broader <https://comcomponent.com/knowledge/spark/> .

<https://comcomponent.com/knowledge/rust-ownership/> a skos:Concept ;
    skos:prefLabel "所有権(Rust)"@ja ;
    skos:definition "各値に所有者を1つだけ持たせ、所有者がスコープを出たときに値を破棄するRustの規則。違反はコンパイルエラーになる。"@ja ;
    skos:altLabel "ownership" ;
    skos:altLabel "ムーブ"@ja .

<https://comcomponent.com/knowledge/rust-borrow-checker/> a skos:Concept ;
    skos:prefLabel "借用チェッカー"@ja ;
    skos:definition "スコープを比べて借用(参照)が有効かを判断し、規則に反する借用をコンパイルエラーにするRustコンパイラの検査。"@ja ;
    skos:altLabel "borrow checker" ;
    ks:prevents <https://comcomponent.com/knowledge/dangling-pointer/> ;
    ks:prevents <https://comcomponent.com/knowledge/data-race/> .

<https://comcomponent.com/knowledge/dangling-pointer/> a skos:Concept ;
    skos:prefLabel "ダングリング参照"@ja ;
    skos:definition "すでに存在しないオブジェクトを指すポインタや参照。参照外しすると、意図しないデータを読み書きする。Adaの参照マニュアルは、これを参照した実行をerroneous(結果が規格で定まらない)としている。"@ja ;
    skos:altLabel "dangling reference" ;
    skos:altLabel "dangling pointer" ;
    skos:altLabel "ダングリングポインタ"@ja .

<https://comcomponent.com/knowledge/data-race/> a skos:Concept ;
    skos:prefLabel "データ競合(data race)"@ja ;
    skos:definition "複数のタスクが同じメモリ位置に同時アクセスし、少なくとも一方が書き込みであるために結果が未定義になる状態である。"@ja ;
    skos:altLabel "Data Race" .

<https://comcomponent.com/knowledge/ada-access-type/> a skos:Concept ;
    skos:prefLabel "アクセス型"@ja ;
    skos:definition "オブジェクトやサブプログラムを指す値を持つAdaの型で、ほかの言語のポインタや参照に当たる。accessだけで宣言するプール固有のアクセス型はその型のnewで作った値だけを指し、access allなどで宣言する汎用のアクセス型はaliasedを付けた変数も指せる。"@ja ;
    skos:altLabel "access type" ;
    skos:altLabel "Adaのアクセス型"@ja ;
    skos:altLabel "プール固有のアクセス型"@ja ;
    skos:altLabel "汎用のアクセス型"@ja .

<https://comcomponent.com/knowledge/ada-accessibility-rules/> a skos:Concept ;
    skos:prefLabel "アクセシビリティ規則"@ja ;
    skos:definition "アクセス型と指す先のオブジェクトの寿命(アクセシビリティレベル)を比べ、指す先より長く残るアクセス値を作らせないAdaの規則。静的に違反が分かればコンパイルエラーになり、実行時の検査(accessibility check)に失敗するとProgram_Errorが発生する。"@ja ;
    skos:altLabel "accessibility rules" ;
    skos:altLabel "accessibility check" ;
    skos:altLabel "アクセシビリティ検査"@ja ;
    skos:altLabel "accessibility level" ;
    skos:altLabel "アクセシビリティレベル"@ja .

<https://comcomponent.com/knowledge/ada-unchecked-deallocation/> a skos:Concept ;
    skos:prefLabel "Ada.Unchecked_Deallocation"@ja ;
    skos:definition "newで確保したオブジェクトを明示的に解放するために、オブジェクトの型とアクセス型を渡してインスタンス化するAdaの標準のジェネリック手続き。解放に渡した変数はnullになるが、同じオブジェクトを指すほかのアクセス値は検査しない。"@ja ;
    skos:altLabel "Unchecked_Deallocation" ;
    ks:requires <https://comcomponent.com/knowledge/ada-access-type/> ;
    ks:mayCause <https://comcomponent.com/knowledge/dangling-pointer/> .

<https://comcomponent.com/knowledge/spark-ownership-policy/> a skos:Concept ;
    skos:prefLabel "所有権ポリシー(SPARK)"@ja ;
    skos:definition "アクセス型の代入で所有権を移し、移動元からのアクセスを禁じるSPARKのメモリ所有権の規則。Rustにならったもので、GNATproveが検査する。"@ja ;
    skos:altLabel "Memory Ownership Policy" .

<https://comcomponent.com/knowledge/memory-leak/> a skos:Concept ;
    skos:prefLabel "メモリリーク"@ja ;
    skos:definition "確保したメモリを解放し忘れ、Private BytesやCommitが増え続ける現象。"@ja ;
    skos:altLabel "Memory Leak" ;
    ks:verifiedBy <https://comcomponent.com/knowledge/gnatprove/> .

<https://comcomponent.com/knowledge/formal-verification/> a skos:Concept ;
    skos:prefLabel "形式検証"@ja ;
    skos:definition "プログラムがすべての入力に対してある性質を満たすことを数学的に証明する、テストとは異なる品質保証の手法である。"@ja ;
    skos:altLabel "Formal Verification" .

<https://comcomponent.com/knowledge/rust-send/> a skos:Concept ;
    skos:prefLabel "Send(Rust)"@ja ;
    skos:definition "その型の値の所有権をスレッド間で移せることを示すRustのマーカートレイト。"@ja ;
    skos:altLabel "Send trait" ;
    ks:prevents <https://comcomponent.com/knowledge/data-race/> .

<https://comcomponent.com/knowledge/rust-sync/> a skos:Concept ;
    skos:prefLabel "Sync(Rust)"@ja ;
    skos:definition "その型を複数のスレッドから参照しても安全であることを示すRustのマーカートレイト。"@ja ;
    skos:altLabel "Sync trait" ;
    ks:prevents <https://comcomponent.com/knowledge/data-race/> .

<https://comcomponent.com/knowledge/protected-object/> a skos:Concept ;
    skos:prefLabel "保護オブジェクト(protected object)"@ja ;
    skos:definition "procedure・function・entryの3種の操作を通じてのみ内部データへアクセスさせ、排他制御を言語が保証するAda 95で導入された機構。"@ja ;
    skos:altLabel "protected type" ;
    skos:altLabel "Protected Object" ;
    ks:prevents <https://comcomponent.com/knowledge/data-race/> .

<https://comcomponent.com/knowledge/ravenscar-profile/> a skos:Concept ;
    skos:prefLabel "Ravenscarプロファイル"@ja ;
    skos:definition "動的タスク生成やselect文などを禁止し、Adaのタスク機能を静的解析可能で決定論的なサブセットに制限するプロファイル。"@ja ;
    skos:altLabel "Ravenscar" .

<https://comcomponent.com/knowledge/jorvik-profile/> a skos:Concept ;
    skos:prefLabel "Jorvikプロファイル"@ja ;
    skos:definition "Ravenscarプロファイルから6つの制限を外し、Simple_BarriersをPure_Barriersに置き換えた、Ada 2022で標準に加わったタスク機能のプロファイル。"@ja ;
    skos:altLabel "Jorvik" ;
    skos:altLabel "pragma Profile (Jorvik)" .

<https://comcomponent.com/knowledge/unsafe-rust/> a skos:Concept ;
    skos:prefLabel "unsafe Rust"@ja ;
    skos:definition "生ポインタの参照外しなど5つの操作を許すRustの仕組み。unsafeの中でも借用チェッカーなどの検査は働く。"@ja ;
    skos:altLabel "unsafe" ;
    skos:altLabel "unsafeブロック"@ja .

<https://comcomponent.com/knowledge/kani/> a skos:Concept ;
    skos:prefLabel "Kani"@ja ;
    skos:definition "モデル検査でRustのプログラムを解析し、未定義動作・パニック・算術オーバーフロー・アサーションなどを検査するオープンソースの検証ツール。"@ja ;
    skos:altLabel "Kani Rust Verifier" .

<https://comcomponent.com/knowledge/verus/> a skos:Concept ;
    skos:prefLabel "Verus"@ja ;
    skos:definition "Rustの構文で書いた仕様を、実行時の検査を加えずに定理証明でRustのコードに対して検証するツール。"@ja ;
    ks:uses <https://comcomponent.com/knowledge/smt-solver/> .

<https://comcomponent.com/knowledge/creusot/> a skos:Concept ;
    skos:prefLabel "Creusot"@ja ;
    skos:definition "RustのコードをWhy3の中間言語Comaに変換して検証する、Rustの演繹的な検証器。"@ja ;
    ks:uses <https://comcomponent.com/knowledge/why3/> .

<https://comcomponent.com/knowledge/prusti/> a skos:Concept ;
    skos:prefLabel "Prusti"@ja ;
    skos:definition "Viper基盤の上に作られた、Rustの自動プログラム検証器。"@ja .

<https://comcomponent.com/knowledge/smt-solver/> a skos:Concept ;
    skos:prefLabel "SMTソルバ(自動証明器)"@ja ;
    skos:definition "論理式が常に成り立つかを機械的に判定する自動証明器の総称で、GNATproveはWhy3経由でこれに証明を委ねる。"@ja ;
    skos:altLabel "SMT Solver" ;
    skos:altLabel "Z3" ;
    skos:altLabel "cvc5" ;
    skos:altLabel "Alt-Ergo" .

<https://comcomponent.com/knowledge/why3/> a skos:Concept ;
    skos:prefLabel "Why3"@ja ;
    skos:definition "演繹的プログラム検証のための中間言語とプラットフォームで、証明課題を複数の自動証明器へ振り分ける。"@ja ;
    skos:altLabel "Why3プラットフォーム"@ja .

[] a rdf:Statement ;
    rdf:subject <https://comcomponent.com/knowledge/ada/> ;
    rdf:predicate ks:implements ;
    rdf:object <https://comcomponent.com/knowledge/ada-strong-typing/> ;
    schema:description "Float から type … is new で作った Meters と Feet は別の型になり、Feet の値を Meters の引数に渡すとコンパイルエラーになる。"@ja ;
    ks:evidence <https://www.adaic.org/resources/add_content/standards/22rm/html/RM-3-4.html> ;
    ks:verifiedAt "2026-11-01" ;
    ks:certainty "established" .

[] a rdf:Statement ;
    rdf:subject <https://comcomponent.com/knowledge/ada/> ;
    rdf:predicate ks:implements ;
    rdf:object <https://comcomponent.com/knowledge/ada-range-constraint/> ;
    schema:description "subtype Percent is Integer range 0 .. 100 のように範囲を型に書くと、その型への代入のたびに範囲が検査され、範囲外なら Constraint_Error になる。"@ja ;
    ks:evidence <https://www.adaic.org/resources/add_content/standards/22rm/html/RM-3-5-4.html> ;
    ks:verifiedAt "2026-11-01" ;
    ks:certainty "established" .

[] a rdf:Statement ;
    rdf:subject <https://comcomponent.com/knowledge/ada/> ;
    rdf:predicate ks:implements ;
    rdf:object <https://comcomponent.com/knowledge/ada-modular-type/> ;
    schema:description "mod で宣言した型は演算結果が範囲を超えると剰余で折り返す。符号付き整数型は範囲を超えると Constraint_Error になる。"@ja ;
    ks:evidence <https://www.adaic.org/resources/add_content/standards/22rm/html/RM-3-5-4.html> ;
    ks:verifiedAt "2026-11-01" ;
    ks:certainty "established" .

[] a rdf:Statement ;
    rdf:subject <https://comcomponent.com/knowledge/rust/> ;
    rdf:predicate ks:uses ;
    rdf:object <https://comcomponent.com/knowledge/newtype-pattern/> ;
    schema:description "Rust には型に値の範囲を書く構文がなく、1要素の構造体で包んだ newtype で単位の取り違えを防ぎ、範囲は生成関数で確かめる。"@ja ;
    ks:evidence <https://doc.rust-lang.org/book/ch20-03-advanced-types.html> ;
    ks:verifiedAt "2026-11-01" ;
    ks:certainty "established" .

[] a rdf:Statement ;
    rdf:subject <https://comcomponent.com/knowledge/integer-overflow/> ;
    rdf:predicate ks:configuredBy ;
    rdf:object <https://comcomponent.com/knowledge/cargo-overflow-checks/> ;
    schema:description "Rust で整数オーバーフローをパニックにするか折り返すかは overflow-checks で決まる。既定は dev で true、release で false で、言語仕様は検査のないビルドでパニックか2の補数の折り返しかを実装に任せている。"@ja ;
    ks:evidence <https://doc.rust-lang.org/cargo/reference/profiles.html>, <https://doc.rust-lang.org/reference/behavior-not-considered-unsafe.html> ;
    ks:verifiedAt "2026-11-01" ;
    ks:certainty "established" .

[] a rdf:Statement ;
    rdf:subject <https://comcomponent.com/knowledge/integer-overflow/> ;
    rdf:predicate ks:verifiedBy ;
    rdf:object <https://comcomponent.com/knowledge/gnatprove/> ;
    schema:description "GNATprove は SPARK のコードについて、整数の演算がオーバーフローしないことを証明の対象にする。"@ja ;
    ks:evidence <https://docs.adacore.com/spark2014-docs/html/ug/> ;
    ks:verifiedAt "2026-11-01" ;
    ks:certainty "established" .

[] a rdf:Statement ;
    rdf:subject <https://comcomponent.com/knowledge/rust/> ;
    rdf:predicate ks:implements ;
    rdf:object <https://comcomponent.com/knowledge/rust-ownership/> ;
    schema:description "値には所有者が1つだけあり、所有権を移した後の変数を使うとコンパイルエラー(E0382)になる。"@ja ;
    ks:evidence <https://doc.rust-lang.org/book/ch04-01-what-is-ownership.html> ;
    ks:verifiedAt "2026-11-01" ;
    ks:certainty "established" .

[] a rdf:Statement ;
    rdf:subject <https://comcomponent.com/knowledge/rust/> ;
    rdf:predicate ks:implements ;
    rdf:object <https://comcomponent.com/knowledge/rust-borrow-checker/> ;
    schema:description "Rust コンパイラは借用チェッカーでスコープを比べ、借用が有効かを判断する。"@ja ;
    ks:evidence <https://doc.rust-lang.org/book/ch10-03-lifetime-syntax.html> ;
    ks:verifiedAt "2026-11-01" ;
    ks:certainty "established" .

[] a rdf:Statement ;
    rdf:subject <https://comcomponent.com/knowledge/rust-borrow-checker/> ;
    rdf:predicate ks:prevents ;
    rdf:object <https://comcomponent.com/knowledge/dangling-pointer/> ;
    schema:description "スコープを出た変数への参照を残す書き方は、借用チェッカーがコンパイルエラー(E0597)にする。"@ja ;
    ks:evidence <https://doc.rust-lang.org/book/ch10-03-lifetime-syntax.html> ;
    ks:verifiedAt "2026-11-01" ;
    ks:certainty "established" .

[] a rdf:Statement ;
    rdf:subject <https://comcomponent.com/knowledge/rust-borrow-checker/> ;
    rdf:predicate ks:prevents ;
    rdf:object <https://comcomponent.com/knowledge/data-race/> ;
    schema:description "可変の参照は同時に1つしか持てないので、複数のスレッドが同じ変数を書き換えるコードはコンパイルエラー(E0499)になる。"@ja ;
    ks:evidence <https://doc.rust-lang.org/book/ch04-02-references-and-borrowing.html> ;
    ks:verifiedAt "2026-11-01" ;
    ks:certainty "established" .

[] a rdf:Statement ;
    rdf:subject <https://comcomponent.com/knowledge/ada/> ;
    rdf:predicate ks:implements ;
    rdf:object <https://comcomponent.com/knowledge/ada-access-type/> ;
    schema:description "Ada のポインタはアクセス型と呼ばれ、new で確保した領域やaliasedなオブジェクトを指す。"@ja ;
    ks:evidence <https://www.adaic.org/resources/add_content/standards/22rm/html/RM-3-10.html> ;
    ks:verifiedAt "2026-11-01" ;
    ks:certainty "established" .

[] a rdf:Statement ;
    rdf:subject <https://comcomponent.com/knowledge/ada/> ;
    rdf:predicate ks:implements ;
    rdf:object <https://comcomponent.com/knowledge/ada-accessibility-rules/> ;
    schema:description "Ada の言語仕様はアクセシビリティ規則を定め、多くの場合コンパイル時に検査する。"@ja ;
    ks:evidence <https://www.adaic.org/resources/add_content/standards/22rm/html/RM-3-10-2.html> ;
    ks:verifiedAt "2026-11-01" ;
    ks:certainty "established" .

[] a rdf:Statement ;
    rdf:subject <https://comcomponent.com/knowledge/ada-accessibility-rules/> ;
    rdf:predicate ks:prevents ;
    rdf:object <https://comcomponent.com/knowledge/dangling-pointer/> ;
    schema:description "ローカル変数を指すアクセス値をより外側のアクセス型の変数に入れるコードはコンパイルエラーになる。ただし Unchecked_Access などの unchecked な機能を使った場合と、Unchecked_Deallocation で解放した後の使用は防がない。"@ja ;
    ks:evidence <https://www.adaic.org/resources/add_content/standards/22rm/html/RM-3-10-2.html>, <https://www.adaic.org/resources/add_content/standards/22rm/html/RM-13-11-2.html> ;
    ks:verifiedAt "2026-11-01" ;
    ks:certainty "context-dependent" .

[] a rdf:Statement ;
    rdf:subject <https://comcomponent.com/knowledge/ada-unchecked-deallocation/> ;
    rdf:predicate ks:requires ;
    rdf:object <https://comcomponent.com/knowledge/ada-access-type/> ;
    schema:description "Ada.Unchecked_Deallocation は解放する対象の型とアクセス型を指定してインスタンス化する。"@ja ;
    ks:evidence <https://www.adaic.org/resources/add_content/standards/22rm/html/RM-13-11-2.html> ;
    ks:verifiedAt "2026-11-01" ;
    ks:certainty "established" .

[] a rdf:Statement ;
    rdf:subject <https://comcomponent.com/knowledge/ada-unchecked-deallocation/> ;
    rdf:predicate ks:mayCause ;
    rdf:object <https://comcomponent.com/knowledge/dangling-pointer/> ;
    schema:description "Free(X) は X だけを null にし、同じ領域を指す別のアクセス変数は残る。それを参照外しした実行は誤った実行になる。"@ja ;
    ks:evidence <https://www.adaic.org/resources/add_content/standards/22rm/html/RM-13-11-2.html> ;
    ks:verifiedAt "2026-11-01" ;
    ks:certainty "established" .

[] a rdf:Statement ;
    rdf:subject <https://comcomponent.com/knowledge/spark/> ;
    rdf:predicate ks:implements ;
    rdf:object <https://comcomponent.com/knowledge/spark-ownership-policy/> ;
    schema:description "SPARK は Rust と同じようにメモリの所有権ポリシーを強制し、アクセス型の代入で所有権を左辺に移す。"@ja ;
    ks:evidence <https://docs.adacore.com/spark2014-docs/html/ug/en/source/access.html> ;
    ks:verifiedAt "2026-11-01" ;
    ks:certainty "established" .

[] a rdf:Statement ;
    rdf:subject <https://comcomponent.com/knowledge/spark-ownership-policy/> ;
    rdf:predicate ks:prevents ;
    rdf:object <https://comcomponent.com/knowledge/dangling-pointer/> ;
    schema:description "所有権を移した後の変数を通した書き込みは、GNATprove が移動後の使用としてエラーにする。SPARK_Mode を Off にした部分は解析されない。"@ja ;
    ks:evidence <https://docs.adacore.com/spark2014-docs/html/ug/en/source/access.html> ;
    ks:verifiedAt "2026-11-01" ;
    ks:certainty "context-dependent" .

[] a rdf:Statement ;
    rdf:subject <https://comcomponent.com/knowledge/memory-leak/> ;
    rdf:predicate ks:verifiedBy ;
    rdf:object <https://comcomponent.com/knowledge/gnatprove/> ;
    schema:description "GNATprove は代入と宣言の寿命の終わりでメモリを漏らしていないかを検査し、解放しないコードにリークの可能性を報告する。"@ja ;
    ks:evidence <https://docs.adacore.com/spark2014-docs/html/ug/en/source/access.html> ;
    ks:verifiedAt "2026-11-01" ;
    ks:certainty "established" .

[] a rdf:Statement ;
    rdf:subject <https://comcomponent.com/knowledge/spark/> ;
    rdf:predicate ks:implements ;
    rdf:object <https://comcomponent.com/knowledge/formal-verification/> ;
    schema:description "SPARK は Ada のサブセットで、契約や実行時エラーの不在を GNATprove で証明する。"@ja ;
    ks:evidence <https://docs.adacore.com/spark2014-docs/html/ug/> ;
    ks:verifiedAt "2026-11-01" ;
    ks:certainty "established" .

[] a rdf:Statement ;
    rdf:subject <https://comcomponent.com/knowledge/spark/> ;
    rdf:predicate ks:uses ;
    rdf:object <https://comcomponent.com/knowledge/gnatprove/> ;
    schema:description "SPARK のコードの所有権・メモリリーク・オーバーフロー・データ競合の検査は GNATprove が行う。"@ja ;
    ks:evidence <https://docs.adacore.com/spark2014-docs/html/ug/> ;
    ks:verifiedAt "2026-11-01" ;
    ks:certainty "established" .

[] a rdf:Statement ;
    rdf:subject <https://comcomponent.com/knowledge/rust/> ;
    rdf:predicate ks:implements ;
    rdf:object <https://comcomponent.com/knowledge/rust-send/> ;
    schema:description "スレッドに値を渡せるかは Send で表し、Send を実装しない Rc を thread::spawn に渡すとコンパイルエラー(E0277)になる。"@ja ;
    ks:evidence <https://doc.rust-lang.org/book/ch16-04-extensible-concurrency-sync-and-send.html> ;
    ks:verifiedAt "2026-11-01" ;
    ks:certainty "established" .

[] a rdf:Statement ;
    rdf:subject <https://comcomponent.com/knowledge/rust/> ;
    rdf:predicate ks:implements ;
    rdf:object <https://comcomponent.com/knowledge/rust-sync/> ;
    schema:description "複数のスレッドから参照してよい型かは Sync で表す。"@ja ;
    ks:evidence <https://doc.rust-lang.org/book/ch16-04-extensible-concurrency-sync-and-send.html> ;
    ks:verifiedAt "2026-11-01" ;
    ks:certainty "established" .

[] a rdf:Statement ;
    rdf:subject <https://comcomponent.com/knowledge/rust-send/> ;
    rdf:predicate ks:prevents ;
    rdf:object <https://comcomponent.com/knowledge/data-race/> ;
    schema:description "Rc は参照カウントを同期せずに更新するので Send を実装しておらず、別スレッドへ渡すコードはコンパイルできない。"@ja ;
    ks:evidence <https://doc.rust-lang.org/book/ch16-04-extensible-concurrency-sync-and-send.html> ;
    ks:verifiedAt "2026-11-01" ;
    ks:certainty "established" .

[] a rdf:Statement ;
    rdf:subject <https://comcomponent.com/knowledge/rust-sync/> ;
    rdf:predicate ks:prevents ;
    rdf:object <https://comcomponent.com/knowledge/data-race/> ;
    schema:description "複数スレッドから参照される値は Sync を実装する型に限られる。"@ja ;
    ks:evidence <https://doc.rust-lang.org/book/ch16-04-extensible-concurrency-sync-and-send.html> ;
    ks:verifiedAt "2026-11-01" ;
    ks:certainty "established" .

[] a rdf:Statement ;
    rdf:subject <https://comcomponent.com/knowledge/protected-object/> ;
    rdf:predicate ks:prevents ;
    rdf:object <https://comcomponent.com/knowledge/data-race/> ;
    schema:description "保護オブジェクトの操作を通して更新したカウンタは毎回正しい値になった。保護しない共有変数の同時更新はコンパイルは通るが誤った実行になる。"@ja ;
    ks:evidence <https://www.adaic.org/resources/add_content/standards/22rm/html/RM-9-4.html>, <https://www.adaic.org/resources/add_content/standards/22rm/html/RM-9-10.html> ;
    ks:verifiedAt "2026-11-01" ;
    ks:certainty "established" .

[] a rdf:Statement ;
    rdf:subject <https://comcomponent.com/knowledge/data-race/> ;
    rdf:predicate ks:verifiedBy ;
    rdf:object <https://comcomponent.com/knowledge/gnatprove/> ;
    schema:description "Ravenscar または Jorvik プロファイルの SPARK コードで、複数のタスクが同期されていない変数にアクセスすると、GNATprove がデータ競合の可能性を報告する。"@ja ;
    ks:evidence <https://docs.adacore.com/spark2014-docs/html/ug/en/source/concurrency.html> ;
    ks:verifiedAt "2026-11-01" ;
    ks:certainty "context-dependent" .

[] a rdf:Statement ;
    rdf:subject <https://comcomponent.com/knowledge/spark/> ;
    rdf:predicate ks:requires ;
    rdf:object <https://comcomponent.com/knowledge/ravenscar-profile/> ;
    schema:description "SPARK で並行処理を書くには Ravenscar プロファイルが必要で、代わりに Jorvik プロファイルも使える。"@ja ;
    ks:evidence <https://docs.adacore.com/spark2014-docs/html/ug/en/source/concurrency.html> ;
    ks:verifiedAt "2026-11-01" ;
    ks:certainty "context-dependent" .

[] a rdf:Statement ;
    rdf:subject <https://comcomponent.com/knowledge/spark/> ;
    rdf:predicate ks:uses ;
    rdf:object <https://comcomponent.com/knowledge/jorvik-profile/> ;
    schema:description "GNATprove は Ada 2022 で定義された Jorvik プロファイルにも対応しており、並行処理の SPARK コードで Ravenscar の代わりに指定できる。"@ja ;
    ks:evidence <https://docs.adacore.com/spark2014-docs/html/ug/en/source/concurrency.html> ;
    ks:verifiedAt "2026-11-01" ;
    ks:certainty "context-dependent" .

[] a rdf:Statement ;
    rdf:subject <https://comcomponent.com/knowledge/rust/> ;
    rdf:predicate ks:implements ;
    rdf:object <https://comcomponent.com/knowledge/unsafe-rust/> ;
    schema:description "unsafe で使えるようになるのは生ポインタの参照外しなど5つの操作だけで、unsafe の外で生ポインタを参照外しするとコンパイルエラー(E0133)になる。#![forbid(unsafe_code)] で unsafe ブロックを禁止できる。"@ja ;
    ks:evidence <https://doc.rust-lang.org/book/ch20-01-unsafe-rust.html> ;
    ks:verifiedAt "2026-11-01" ;
    ks:certainty "established" .

[] a rdf:Statement ;
    rdf:subject <https://comcomponent.com/knowledge/unsafe-rust/> ;
    rdf:predicate ks:mayCause ;
    rdf:object <https://comcomponent.com/knowledge/dangling-pointer/> ;
    schema:description "生ポインタは有効なメモリを指す保証がなく、unsafe での参照外しはコンパイラが検査しない。"@ja ;
    ks:evidence <https://doc.rust-lang.org/book/ch20-01-unsafe-rust.html> ;
    ks:verifiedAt "2026-11-01" ;
    ks:certainty "context-dependent" .

[] a rdf:Statement ;
    rdf:subject <https://comcomponent.com/knowledge/rust/> ;
    rdf:predicate ks:verifiedBy ;
    rdf:object <https://comcomponent.com/knowledge/kani/> ;
    schema:description "Kani はモデル検査で Rust のプログラムの未定義動作・パニック・算術オーバーフロー・アサーションを検査する。この記事では実行していない。"@ja ;
    ks:evidence <https://model-checking.github.io/kani/> ;
    ks:verifiedAt "2026-11-01" ;
    ks:certainty "context-dependent" .

[] a rdf:Statement ;
    rdf:subject <https://comcomponent.com/knowledge/rust/> ;
    rdf:predicate ks:verifiedBy ;
    rdf:object <https://comcomponent.com/knowledge/verus/> ;
    schema:description "Verus は Rust の構文で書いた仕様を定理証明で検証するが、Rust のすべての機能への対応は目指していない。この記事では実行していない。"@ja ;
    ks:evidence <https://verus-lang.github.io/verus/guide/> ;
    ks:verifiedAt "2026-11-01" ;
    ks:certainty "context-dependent" .

[] a rdf:Statement ;
    rdf:subject <https://comcomponent.com/knowledge/rust/> ;
    rdf:predicate ks:verifiedBy ;
    rdf:object <https://comcomponent.com/knowledge/creusot/> ;
    schema:description "Creusot は Rust のコードにパニック・オーバーフロー・アサーションの失敗がないことを検証する。この記事では実行していない。"@ja ;
    ks:evidence <https://github.com/creusot-rs/creusot> ;
    ks:verifiedAt "2026-11-01" ;
    ks:certainty "context-dependent" .

[] a rdf:Statement ;
    rdf:subject <https://comcomponent.com/knowledge/rust/> ;
    rdf:predicate ks:verifiedBy ;
    rdf:object <https://comcomponent.com/knowledge/prusti/> ;
    schema:description "Prusti は unsafe の機能を含まない Rust の一部を対象に、機能上の性質を検証する。この記事では実行していない。"@ja ;
    ks:evidence <https://www.pm.inf.ethz.ch/research/prusti.html> ;
    ks:verifiedAt "2026-11-01" ;
    ks:certainty "context-dependent" .

[] a rdf:Statement ;
    rdf:subject <https://comcomponent.com/knowledge/integer-overflow/> ;
    rdf:predicate ks:verifiedBy ;
    rdf:object <https://comcomponent.com/knowledge/kani/> ;
    schema:description "Kani は算術オーバーフローを検査の対象に含む。"@ja ;
    ks:evidence <https://model-checking.github.io/kani/> ;
    ks:verifiedAt "2026-11-01" ;
    ks:certainty "established" .

[] a rdf:Statement ;
    rdf:subject <https://comcomponent.com/knowledge/verus/> ;
    rdf:predicate ks:uses ;
    rdf:object <https://comcomponent.com/knowledge/smt-solver/> ;
    schema:description "Verus は自動証明器の Z3 を使って仕様を満たすことを確かめる。"@ja ;
    ks:evidence <https://verus-lang.github.io/verus/guide/> ;
    ks:verifiedAt "2026-11-01" ;
    ks:certainty "established" .

[] a rdf:Statement ;
    rdf:subject <https://comcomponent.com/knowledge/creusot/> ;
    rdf:predicate ks:uses ;
    rdf:object <https://comcomponent.com/knowledge/why3/> ;
    schema:description "Creusot は Rust のコードを Why3 の中間言語 Coma に変換し、Why3 で検証条件を扱う。"@ja ;
    ks:evidence <https://github.com/creusot-rs/creusot> ;
    ks:verifiedAt "2026-11-01" ;
    ks:certainty "established" .