@prefix schema: .
@prefix skos: .
@prefix rdf: .
@prefix ks: .
schema:about , , ;
schema:mentions , , , , , , , , , , , , .
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 ;
ks:uses .
a skos:Concept ;
skos:prefLabel "ストレージプール(Ada)"@ja ;
skos:definition "アクセス型のnewが領域を確保する場所。アクセス型ごとにStorage_PoolやStorage_Sizeで指定でき、Root_Storage_Poolを継承してAllocate・Deallocate・Storage_Sizeを上書きすると独自のプールを作れる。"@ja ;
skos:altLabel "storage pool" ;
skos:altLabel "System.Storage_Pools" ;
skos:altLabel "Root_Storage_Pool" .
a skos:Concept ;
skos:prefLabel "Controlled型(Ada)"@ja ;
skos:definition "Ada.FinalizationのControlledまたはLimited_Controlledから派生し、Initialize・Adjust・Finalizeを上書きして、既定の初期化・代入・スコープを出るときの処理を定義できるAdaの型。"@ja ;
skos:altLabel "Ada.Finalization.Controlled" ;
skos:altLabel "Limited_Controlled" ;
skos:altLabel "被制御型"@ja ;
ks:implements .
a skos:Concept ;
skos:prefLabel "GNAT"@ja ;
skos:definition "GCCに含まれる無償のAdaコンパイラで、Adaの代表的な処理系。"@ja ;
skos:altLabel "GNATコンパイラ"@ja ;
ks:implements .
a skos:Concept ;
skos:prefLabel "Ada(プログラミング言語)"@ja ;
skos:definition "1970年代後半にアメリカ国防総省の主導で標準化された、強い型付けと高信頼性を重視する汎用プログラミング言語。最新標準はAda 2022。"@ja ;
skos:altLabel "Ada言語"@ja ;
skos:altLabel "Ada 2022" .
a skos:Concept ;
skos:prefLabel "セカンダリスタック(GNAT)"@ja ;
skos:definition "GNATが、関数が返す長さの決まっていない配列やレコードなどのオブジェクトを置くために使う領域。多くのターゲットでは必要に応じて伸び、ヒープ上のブロックの連なりとして実装される。"@ja ;
skos:altLabel "secondary stack" .
a skos:Concept ;
skos:prefLabel "Ada.Unchecked_Deallocation"@ja ;
skos:definition "newで確保したオブジェクトを明示的に解放するために、オブジェクトの型とアクセス型を渡してインスタンス化するAdaの標準のジェネリック手続き。解放に渡した変数はnullになるが、同じオブジェクトを指すほかのアクセス値は検査しない。"@ja ;
skos:altLabel "Unchecked_Deallocation" ;
ks:requires ;
ks:mayCause .
a skos:Concept ;
skos:prefLabel "ダングリング参照"@ja ;
skos:definition "すでに存在しないオブジェクトを指すポインタや参照。参照外しすると、意図しないデータを読み書きする。Adaの参照マニュアルは、これを参照した実行をerroneous(結果が規格で定まらない)としている。"@ja ;
skos:altLabel "dangling reference" ;
skos:altLabel "dangling pointer" ;
skos:altLabel "ダングリングポインタ"@ja .
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 .
a skos:Concept ;
skos:prefLabel "SPARK"@ja ;
skos:definition "プログラムの性質を数学的に証明できるように設計された、Adaのサブセット(部分言語)とそのツール群。"@ja ;
skos:altLabel "SPARK Ada" ;
skos:altLabel "GNATprove" ;
ks:uses .
a skos:Concept ;
skos:prefLabel "GNATprove"@ja ;
skos:definition "AdaCoreが提供する、SPARKコードの契約や表明を自動証明器で検証するコマンドラインツールである。"@ja ;
skos:altLabel "gnatprove コマンド"@ja ;
skos:broader .
a skos:Concept ;
skos:prefLabel "Valgrind"@ja ;
skos:definition "プログラムを実行しながら解析するツール群。そのうちMemcheckは、解放済み領域の読み取りなどの不正なメモリアクセスやメモリリークを検出する。"@ja ;
skos:altLabel "Memcheck" .
a skos:Concept ;
skos:prefLabel "メモリリーク"@ja ;
skos:definition "確保したメモリを解放し忘れ、Private BytesやCommitが増え続ける現象。"@ja ;
skos:altLabel "Memory Leak" .
a skos:Concept ;
skos:prefLabel "RAII(Resource Acquisition Is Initialization)"@ja ;
skos:definition "オブジェクトの生成時に資源を確保し、デストラクタでの解放を保証することで、途中失敗時にも資源が漏れないようにするC++の設計パターン。"@ja ;
skos:altLabel "RAII" .
a skos:Concept ;
skos:prefLabel "サブプール(Ada)"@ja ;
skos:definition "Ada 2012で追加された、1つのストレージプールを複数に分ける仕組み。newで確保先のサブプールを指定でき、Unchecked_Deallocate_Subpoolでサブプールごとまとめて解放できる。"@ja ;
skos:altLabel "storage subpool" ;
skos:altLabel "System.Storage_Pools.Subpools" ;
ks:requires .
a skos:Concept ;
skos:prefLabel "Ada.Containers"@ja ;
skos:definition "Ada 2005で標準に加わった、ベクタ・リスト・マップ・集合などの要素の集まりを扱うAdaの標準パッケージ群。"@ja ;
skos:altLabel "Adaの標準コンテナ"@ja ;
skos:altLabel "Ada.Containers.Vectors" ;
skos:altLabel "Ada.Containers.Indefinite_Vectors" .
[] a rdf:Statement ;
rdf:subject ;
rdf:predicate ks:implements ;
rdf:object ;
schema:description "GNATはAda言語のコンパイラとしての実装を担う処理系で、本記事の例はGNAT 13.3.0でコンパイルして実行した。"@ja ;
ks:evidence ;
ks:verifiedAt "2026-11-01" ;
ks:certainty "established" .
[] a rdf:Statement ;
rdf:subject ;
rdf:predicate ks:uses ;
rdf:object ;
schema:description "GNATは、長さの決まっていない値を返す関数の戻り値をセカンダリスタックに置き、呼び出し側のスコープを出ると戻す。pragma Restrictions (No_Secondary_Stack)を付けると、その使用はコンパイルエラーになる。"@ja ;
ks:evidence , ;
ks:verifiedAt "2026-11-01" ;
ks:certainty "context-dependent" .
[] a rdf:Statement ;
rdf:subject ;
rdf:predicate ks:uses ;
rdf:object ;
schema:description "アクセス型のnewは、そのアクセス型に結び付いたストレージプールから領域を確保する。指定しなければ処理系の既定のプール(GNATではmallocとfreeを使うSystem.Pool_Global)が使われ、Storage_PoolやStorage_Sizeで型ごとに差し替えたり上限を付けたりできる。"@ja ;
ks:evidence , ;
ks:verifiedAt "2026-11-01" ;
ks:certainty "established" .
[] a rdf:Statement ;
rdf:subject ;
rdf:predicate ks:requires ;
rdf:object ;
schema:description "Unchecked_Deallocationは、解放するオブジェクトの型とそれを指すアクセス型を渡してインスタンス化して使う。"@ja ;
ks:evidence ;
ks:verifiedAt "2026-11-01" ;
ks:certainty "established" .
[] a rdf:Statement ;
rdf:subject ;
rdf:predicate ks:mayCause ;
rdf:object ;
schema:description "Free(X)のあとXはnullになるが、同じオブジェクトを指していたほかのアクセス値は元のアドレスを持ったまま残る。それを参照した実行はerroneousで、GNAT 13.3では例外にならなかった。"@ja ;
ks:evidence ;
ks:verifiedAt "2026-11-01" ;
ks:certainty "established" .
[] a rdf:Statement ;
rdf:subject ;
rdf:predicate ks:prevents ;
rdf:object ;
schema:description "寿命の短い変数を指す値を寿命の長いアクセス型に保存することを、静的に分かればコンパイルエラーで、匿名アクセス型の引数のように実行時まで分からなければProgram_Errorで止める。Unchecked_Deallocationで解放した領域を指すアクセス値は、この検査では防げない。"@ja ;
ks:evidence ;
ks:verifiedAt "2026-11-01" ;
ks:certainty "context-dependent" .
[] a rdf:Statement ;
rdf:subject ;
rdf:predicate ks:prevents ;
rdf:object ;
schema:description "SPARKはアクセス型に所有権の規則を課し、確保した領域に読み書きできるアクセス値を同時に1つに限る。本記事の例では、所有権がBに移ったAを解放しようとした行を、GNATproveが--mode=check_allの検査でエラーにした。"@ja ;
ks:evidence ;
ks:verifiedAt "2026-11-01" ;
ks:certainty "context-dependent" .
[] a rdf:Statement ;
rdf:subject ;
rdf:predicate ks:uses ;
rdf:object ;
schema:description "SPARKのコードの検査と証明にはGNATproveを使う。本記事ではGNATprove 15.1で所有権の規則を検査した。"@ja ;
ks:evidence ;
ks:verifiedAt "2026-11-01" ;
ks:certainty "established" .
[] a rdf:Statement ;
rdf:subject ;
rdf:predicate ks:verifiedBy ;
rdf:object ;
schema:description "本記事の例では、解放済みの領域をダングリング参照で読んでもGNATは例外を出さず、ValgrindのMemcheckがInvalid readとして報告した。"@ja ;
ks:evidence ;
ks:verifiedAt "2026-11-01" ;
ks:certainty "context-dependent" .
[] a rdf:Statement ;
rdf:subject ;
rdf:predicate ks:verifiedBy ;
rdf:object ;
schema:description "本記事の例では、前の値を指すアクセス値を失うループで確保した領域を、ValgrindのMemcheckがdefinitely lostとして報告した。"@ja ;
ks:evidence ;
ks:verifiedAt "2026-11-01" ;
ks:certainty "context-dependent" .
[] a rdf:Statement ;
rdf:subject ;
rdf:predicate ks:implements ;
rdf:object ;
schema:description "Controlled型のFinalizeはスコープを出るときや例外で抜けるときにも呼ばれるため、解放をFinalizeに書くと、C++でデストラクタに解放を書くRAIIと同じく、呼び出し側が解放を書かずに済む。"@ja ;
ks:evidence ;
ks:verifiedAt "2026-11-01" ;
ks:certainty "established" .
[] a rdf:Statement ;
rdf:subject ;
rdf:predicate ks:uses ;
rdf:object ;
schema:description "本記事のBuffer型は、Limited_ControlledのFinalizeの中でUnchecked_Deallocationのインスタンスを呼び、持っている配列を解放する。"@ja ;
ks:evidence , ;
ks:verifiedAt "2026-11-01" ;
ks:certainty "context-dependent" .
[] a rdf:Statement ;
rdf:subject ;
rdf:predicate ks:mitigates ;
rdf:object ;
schema:description "解放をFinalizeに書くと、呼び出し側が解放を書き忘れることがなくなる。本記事の例では、数えるプールを使ったBuffer型でブロックを出ると確保と解放の回数がそろい、使用量が0に戻った。"@ja ;
ks:evidence ;
ks:verifiedAt "2026-11-01" ;
ks:certainty "context-dependent" .
[] a rdf:Statement ;
rdf:subject ;
rdf:predicate ks:requires ;
rdf:object ;
schema:description "サブプールは1つのストレージプールを複数に分けたもので、newで確保先のサブプールを指定でき、サブプールごとまとめて解放できる。"@ja ;
ks:evidence , ;
ks:verifiedAt "2026-11-01" ;
ks:certainty "established" .
[] a rdf:Statement ;
rdf:subject ;
rdf:predicate ks:mitigates ;
rdf:object ;
schema:description "Ada.Containersは要素の確保と解放をコンテナの側で行うので、利用者がnewや解放を書かずに済む。本記事のIndefinite_Vectorsの例では、Valgrindで終了時の使用量が0バイトだった。"@ja ;
ks:evidence ;
ks:verifiedAt "2026-11-01" ;
ks:certainty "context-dependent" .