@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:implements ;
ks:uses .
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 "形式検証"@ja ;
skos:definition "プログラムがすべての入力に対してある性質を満たすことを数学的に証明する、テストとは異なる品質保証の手法である。"@ja ;
skos:altLabel "Formal Verification" .
a skos:Concept ;
skos:prefLabel "GNATprove"@ja ;
skos:definition "AdaCoreが提供する、SPARKコードの契約や表明を自動証明器で検証するコマンドラインツールである。"@ja ;
skos:altLabel "gnatprove コマンド"@ja ;
skos:broader ;
ks:uses ;
ks:uses ;
ks:configuredBy .
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:verifiedBy .
a skos:Concept ;
skos:prefLabel "ループ不変条件(Loop Invariant)"@ja ;
skos:definition "ループの各反復の開始時点で成り立つ性質を宣言し、ループに関する性質の証明を可能にするSPARKのプラグマである。"@ja ;
skos:altLabel "Loop_Invariant" ;
skos:broader .
a skos:Concept ;
skos:prefLabel "pragma Assume"@ja ;
skos:definition "SPARKで、GNATproveに確かめさせずに、指定した性質が成り立つものとして以降の解析に使わせるプラグマ。アサーションを有効にしてコンパイルすると、実行時にも検査される。"@ja ;
skos:altLabel "Assume" ;
skos:broader .
a skos:Concept ;
skos:prefLabel "pragma Annotate(GNATprove)"@ja ;
skos:definition "GNATproveの検査メッセージを、理由を添えて誤検知(False_Positive)または意図したもの(Intentional)として正当化するプラグマ。直前の項目に掛かり、正当化した理由は解析結果の記録に残る。"@ja ;
skos:altLabel "検査メッセージの正当化"@ja ;
skos:altLabel "False_Positive" ;
skos:altLabel "Intentional" ;
skos:broader .
a skos:Concept ;
skos:prefLabel "SPARK_Mode"@ja ;
skos:definition "コードをSPARKとして扱うかを指定するアスペクトとプラグマ。Onの部分はSPARKの制限に従ってGNATproveが解析し、Offの部分は解析されず、SPARKの制限にも従う必要がない。"@ja ;
skos:altLabel "SPARK_Mode => Off" ;
skos:altLabel "SPARK_Mode => On" ;
skos:broader .
a skos:Concept ;
skos:prefLabel "コードレビュー(プルリクエストレビュー)"@ja ;
skos:definition "プルリクエスト単位でコードの変更内容を他者が確認する開発プロセスである。"@ja ;
skos:altLabel "プルリクエストレビュー"@ja ;
skos:altLabel "Pull Request Review" ;
ks:recommendedFor ;
ks:recommendedFor ;
ks:recommendedFor .
a skos:Concept ;
skos:prefLabel "ユニットテスト"@ja ;
skos:definition "分離された1責務の正しさを、外部資源を切り離して確かめるテストの層のこと。"@ja ;
skos:altLabel "Unit Test" ;
skos:altLabel "単体テスト"@ja .
[] a rdf:Statement ;
rdf:subject ;
rdf:predicate ks:implements ;
rdf:object ;
schema:description "SPARKはAdaのサブセットとして、契約に書いた性質を数学的に証明する形式検証を提供する"@ja ;
ks:evidence ;
ks:verifiedAt "2026-11-01" ;
ks:certainty "established" .
[] a rdf:Statement ;
rdf:subject ;
rdf:predicate ks:uses ;
rdf:object ;
schema:description "SPARKのコードの証明にはGNATproveを使う。この記事では gnatprove -P p.gpr --level=2 --report=fail で実行した"@ja ;
ks:evidence ;
ks:verifiedAt "2026-11-01" ;
ks:certainty "established" .
[] a rdf:Statement ;
rdf:subject ;
rdf:predicate ks:verifiedBy ;
rdf:object ;
schema:description "事前条件を満たすすべての入力について事後条件が成り立つことを、GNATproveで確かめられる。確かめるのは本体が契約を満たすことで、契約が仕様どおりかは確かめない"@ja ;
ks:evidence ;
ks:verifiedAt "2026-11-01" ;
ks:certainty "established" .
[] a rdf:Statement ;
rdf:subject ;
rdf:predicate ks:verifiedBy ;
rdf:object ;
schema:description "SPARKの範囲の本体で整数の演算があふれ得る箇所を、GNATproveが overflow check might fail として反例の値つきで報告する。反例は実行できる入力に対応するとは限らない"@ja ;
ks:evidence ;
ks:verifiedAt "2026-11-01" ;
ks:certainty "established" .
[] a rdf:Statement ;
rdf:subject ;
rdf:predicate ks:requires ;
rdf:object ;
schema:description "ループの後で成り立つ事後条件を証明するには、Loop_Invariantでループの各回で成り立つ性質を示す必要がある。本体が正しくても、不変条件がないと証明できないことがある"@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 "GNATproveはpragma Assumeの性質を確かめずに、以降の解析の前提として使う。使った場所は gnatprove.out に一覧される"@ja ;
ks:evidence ;
ks:verifiedAt "2026-11-01" ;
ks:certainty "established" .
[] a rdf:Statement ;
rdf:subject ;
rdf:predicate ks:uses ;
rdf:object ;
schema:description "GNATproveはpragma Annotateで正当化された検査メッセージを、失敗ではなく正当化済みとして扱い、理由を解析結果の記録に残す"@ja ;
ks:evidence ;
ks:verifiedAt "2026-11-01" ;
ks:certainty "established" .
[] a rdf:Statement ;
rdf:subject ;
rdf:predicate ks:configuredBy ;
rdf:object ;
schema:description "GNATproveが解析する範囲はSPARK_Modeで決まり、SPARK_Mode => Offにした本体は解析されない"@ja ;
ks:evidence ;
ks:verifiedAt "2026-11-01" ;
ks:certainty "established" .
[] a rdf:Statement ;
rdf:subject ;
rdf:predicate ks:recommendedFor ;
rdf:object ;
schema:description "AIが書いたコードを証明する場合、人は本体より先に、事前条件が業務上の入力を締め出していないかと、事後条件が結果を決め切っているかを読む"@ja ;
ks:evidence ;
ks:verifiedAt "2026-11-01" ;
ks:certainty "established" .
[] a rdf:Statement ;
rdf:subject ;
rdf:predicate ks:recommendedFor ;
rdf:object ;
schema:description "pragma Assumeは確かめられずに前提として使われるので、追加されたら理由をレビューで確かめる"@ja ;
ks:evidence ;
ks:verifiedAt "2026-11-01" ;
ks:certainty "established" .
[] a rdf:Statement ;
rdf:subject ;
rdf:predicate ks:recommendedFor ;
rdf:object ;
schema:description "検査メッセージの正当化はすべてレビューする。誤った正当化は、実際に失敗し得る検査を隠す"@ja ;
ks:evidence ;
ks:verifiedAt "2026-11-01" ;
ks:certainty "established" .
[] a rdf:Statement ;
rdf:subject ;
rdf:predicate ks:recommendedFor ;
rdf:object ;
schema:description "事後条件が弱いと誤った本体でも証明が通るため、具体的な期待値を書いたユニットテストを証明と併せて使う。記事の例では、常に下限を返す本体が証明を通り、具体的な値で実行すると誤りが分かった"@ja ;
ks:evidence ;
ks:verifiedAt "2026-11-01" ;
ks:certainty "context-dependent" .