データフロー契約(Global/Depends)

サブプログラムが読み書きするグローバル変数と、変数間の依存関係を宣言するSPARKの契約である。

概念URI

https://comcomponent.com/knowledge/dataflow-contract/

別名・表記

Global契約 / Depends契約

上位概念

SPARK

最終確認日

2026-08-01

機械可読データ

JSON-LD

この概念が関わる関係

• SPARKはデータフロー契約(Global/Depends)を利用します。SPARKは副作用を管理するため、Global/Depends契約でグローバル変数の読み書きと依存関係を明示する / 確度: 確立した関係 / 確認日: 2026-08-01 出典
• データフロー契約(Global/Depends)はGNATproveで確認できます。Global/Depends契約が意図通りであることはGNATproveのフロー解析(Bronzeレベル)で確認できる / 確度: 確立した関係 / 確認日: 2026-08-01 出典

この概念を扱う記事

• SPARKによる形式検証入門 ── Adaの契約から数学的証明へ(言及)

一次資料

• https://docs.adacore.com/spark2014-docs/html/ug/

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