@prefix schema: .
@prefix skos: .
@prefix rdf: .
@prefix ks: .
schema:about , ;
schema:mentions , , , , , , , , , , , .
a skos:Concept ;
skos:prefLabel "SPARK"@ja ;
skos:definition "プログラムの性質を数学的に証明できるように設計された、Adaのサブセット(部分言語)とそのツール群。"@ja ;
skos:altLabel "SPARK Ada" ;
skos:altLabel "GNATprove" ;
ks:uses ;
ks:implements ;
ks:uses ;
ks:uses ;
ks:uses .
a skos:Concept ;
skos:prefLabel "形式検証"@ja ;
skos:definition "プログラムがすべての入力に対してある性質を満たすことを数学的に証明する、テストとは異なる品質保証の手法である。"@ja ;
skos:altLabel "Formal Verification" .
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 "契約による設計(Pre/Post)"@ja ;
skos:definition "サブプログラムの入口での前提条件(Pre)と、出口で保証する性質(Post)を宣言的に記述する、Ada 2012の契約機構である。"@ja ;
skos:altLabel "Design by Contract" ;
skos:altLabel "事前条件・事後条件"@ja ;
skos:broader ;
ks:verifiedBy .
a skos:Concept ;
skos:prefLabel "GNATprove"@ja ;
skos:definition "AdaCoreが提供する、SPARKコードの契約や表明を自動証明器で検証するコマンドラインツールである。"@ja ;
skos:altLabel "gnatprove コマンド"@ja ;
skos:broader ;
ks:requires ;
ks:uses .
a skos:Concept ;
skos:prefLabel "Why3"@ja ;
skos:definition "演繹的プログラム検証のための中間言語とプラットフォームで、証明課題を複数の自動証明器へ振り分ける。"@ja ;
skos:altLabel "Why3プラットフォーム"@ja ;
ks:uses .
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" .
a skos:Concept ;
skos:prefLabel "ループ不変条件(Loop Invariant)"@ja ;
skos:definition "ループの各反復の開始時点で成り立つ性質を宣言し、ループに関する性質の証明を可能にするSPARKのプラグマである。"@ja ;
skos:altLabel "Loop_Invariant" ;
skos:broader .
a skos:Concept ;
skos:prefLabel "データフロー契約(Global/Depends)"@ja ;
skos:definition "サブプログラムが読み書きするグローバル変数と、変数間の依存関係を宣言するSPARKの契約である。"@ja ;
skos:altLabel "Global契約"@ja ;
skos:altLabel "Depends契約"@ja ;
skos:broader ;
ks:verifiedBy .
a skos:Concept ;
skos:prefLabel "証明レベル(Stone〜Platinum)"@ja ;
skos:definition "SPARKでソフトウェア保証の厳しさをStone・Bronze・Silver・Gold・Platinumの5段階で定義する、証明対象の目標設定の考え方である。"@ja ;
skos:altLabel "Levels of Software Assurance" ;
skos:broader .
a skos:Concept ;
skos:prefLabel "Ravenscarプロファイル"@ja ;
skos:definition "動的タスク生成やselect文などを禁止し、Adaのタスク機能を静的解析可能で決定論的なサブセットに制限するプロファイル。"@ja ;
skos:altLabel "Ravenscar" .
a skos:Concept ;
skos:prefLabel "Alire"@ja ;
skos:definition "Ada/SPARKのパッケージマネージャー兼ビルドツールで、ツールチェーン(GNAT)の取得・管理も担う。"@ja ;
skos:altLabel "alr" .
a skos:Concept ;
skos:prefLabel "AUnit"@ja ;
skos:definition "Adaの単体テストフレームワークで、SPARKで証明できなかった部分の振る舞いをテストする用途で併用される。"@ja ;
skos:altLabel "Ada Unit Testing Framework" ;
ks:recommendedFor .
a skos:Concept ;
skos:prefLabel "Silverレベル(AoRTE)"@ja ;
skos:definition "範囲外アクセス・オーバーフロー・ゼロ除算などの実行時エラーが起きないことを証明する、証明レベルのうち実務上の既定目標とされる段階である。"@ja ;
skos:altLabel "Absence of Run-time Errors" ;
skos:altLabel "AoRTE" ;
skos:broader ;
ks:recommendedFor ;
ks:verifiedBy .
[] a rdf:Statement ;
rdf:subject ;
rdf:predicate ks:uses ;
rdf:object ;
schema:description "SPARKはAdaの言語仕様、特にAda 2012で追加された契約(Pre/Post)機能を土台として作られている"@ja ;
ks:evidence ;
ks:verifiedAt "2026-08-01" ;
ks:certainty "established" .
[] a rdf:Statement ;
rdf:subject ;
rdf:predicate ks:implements ;
rdf:object ;
schema:description "SPARKはAdaのサブセットとして、契約に書いた性質を数学的に証明する形式検証を実装として提供する"@ja ;
ks:evidence ;
ks:verifiedAt "2026-08-01" ;
ks:certainty "established" .
[] a rdf:Statement ;
rdf:subject ;
rdf:predicate ks:requires ;
rdf:object ;
schema:description "SPARKの証明のうち、書いた性質の証明はPre/Postで書かれた契約を証明の入力とすることを前提とする。ただしオーバーフロー・範囲外アクセス・ゼロ除算などの実行時エラー不在(AoRTE)の証明は、明示的なPre/Post契約を書かなくても型の範囲制約などから成立し得る"@ja ;
ks:evidence ;
ks:verifiedAt "2026-08-01" ;
ks:certainty "context-dependent" .
[] a rdf:Statement ;
rdf:subject ;
rdf:predicate ks:uses ;
rdf:object ;
schema:description "SPARKコードの検証には、AdaCoreが提供するGNATproveというツールを使う"@ja ;
ks:evidence ;
ks:verifiedAt "2026-08-01" ;
ks:certainty "established" .
[] a rdf:Statement ;
rdf:subject ;
rdf:predicate ks:requires ;
rdf:object ;
schema:description "GNATproveはGNATツールチェーンに同梱されて提供され、Adaのコンパイル環境を前提とする"@ja ;
ks:evidence ;
ks:verifiedAt "2026-08-01" ;
ks:certainty "established" .
[] a rdf:Statement ;
rdf:subject ;
rdf:predicate ks:uses ;
rdf:object ;
schema:description "GNATproveは契約や表明をいったんWhy3の中間言語に変換してから証明器に渡す"@ja ;
ks:evidence ;
ks:verifiedAt "2026-08-01" ;
ks:certainty "established" .
[] a rdf:Statement ;
rdf:subject ;
rdf:predicate ks:uses ;
rdf:object ;
schema:description "Why3は複数の自動証明器(SMTソルバ)へ証明課題を振り分けるプラットフォームである"@ja ;
ks:evidence ;
ks:verifiedAt "2026-08-01" ;
ks:certainty "established" .
[] a rdf:Statement ;
rdf:subject ;
rdf:predicate ks:requires ;
rdf:object ;
schema:description "ループを含む性質を証明する場合、SPARKはLoop_Invariantでループの各反復で成り立つ性質を示すことを前提とする"@ja ;
ks:evidence ;
ks:verifiedAt "2026-08-01" ;
ks:certainty "context-dependent" .
[] a rdf:Statement ;
rdf:subject ;
rdf:predicate ks:uses ;
rdf:object ;
schema:description "SPARKは副作用を管理するため、Global/Depends契約でグローバル変数の読み書きと依存関係を明示する"@ja ;
ks:evidence ;
ks:verifiedAt "2026-08-01" ;
ks:certainty "established" .
[] a rdf:Statement ;
rdf:subject ;
rdf:predicate ks:uses ;
rdf:object ;
schema:description "SPARKは証明の厳しさをStoneからPlatinumまで段階的に定義する証明レベルの考え方を使う"@ja ;
ks:evidence ;
ks:verifiedAt "2026-08-01" ;
ks:certainty "established" .
[] a rdf:Statement ;
rdf:subject ;
rdf:predicate ks:requires ;
rdf:object ;
schema:description "SPARKでタスクを扱う場合、並行処理をRavenscar(または後継のJorvik)プロファイルの範囲に限定することを前提とする"@ja ;
ks:evidence ;
ks:verifiedAt "2026-08-01" ;
ks:certainty "context-dependent" .
[] a rdf:Statement ;
rdf:subject ;
rdf:predicate ks:configuredBy ;
rdf:object ;
schema:description "GNATツールチェーンを使う場合、Ada/SPARKはAlireというソースベースのパッケージマネージャーで導入・構成できる"@ja ;
ks:evidence ;
ks:verifiedAt "2026-08-01" ;
ks:certainty "context-dependent" .
[] a rdf:Statement ;
rdf:subject ;
rdf:predicate ks:recommendedFor ;
rdf:object ;
schema:description "SPARKで型と契約を固めたうえでAUnitによる単体テストを組み合わせることが実践的な運用として推奨される"@ja ;
ks:evidence ;
ks:verifiedAt "2026-08-01" ;
ks:certainty "established" .
[] a rdf:Statement ;
rdf:subject ;
rdf:predicate ks:recommendedFor ;
rdf:object ;
schema:description "実行時エラーが起きないことを証明するSilverレベルは、SPARK導入における実務上の既定の目標として推奨される"@ja ;
ks:evidence ;
ks:verifiedAt "2026-08-01" ;
ks:certainty "established" .
[] a rdf:Statement ;
rdf:subject ;
rdf:predicate ks:verifiedBy ;
rdf:object ;
schema:description "Silverレベルが達成されている(範囲外・オーバーフロー・ゼロ除算が起きない)ことはGNATproveの証明で確認できる"@ja ;
ks:evidence ;
ks:verifiedAt "2026-08-01" ;
ks:certainty "established" .
[] a rdf:Statement ;
rdf:subject ;
rdf:predicate ks:verifiedBy ;
rdf:object ;
schema:description "Global/Depends契約が意図通りであることはGNATproveのフロー解析(Bronzeレベル)で確認できる"@ja ;
ks:evidence ;
ks:verifiedAt "2026-08-01" ;
ks:certainty "established" .
[] a rdf:Statement ;
rdf:subject ;
rdf:predicate ks:verifiedBy ;
rdf:object ;
schema:description "Pre/Post契約が満たされることはGNATproveの証明で確認できる"@ja ;
ks:evidence ;
ks:verifiedAt "2026-08-01" ;
ks:certainty "established" .