Constructive Data Refinementの証明技法の改善

スポンサーリンク

概要

• 論文の詳細を見る

• プログラムを実装する際,仕様(抽象的仕様)をプログラム(具体的仕様)に変換することが行われている.このような仕様の変換を詳細化と呼ぶ.Honsellらは仕様のモデル間に,Pre-logical Relationを用いることにより,詳細化の正しさを保証する証明技法を提案した.しかし,実際に証明を行うときには,モデルやモデル間のPre-logical Relationを考察するのは,非常に複雑である.本発表では,仕様間の詳細化が正しいことを保証するための,仕様の構文上での関係を考察する.このことにより,仕様の構文上での関係を利用した詳細化の正しさを定式化することが可能となった.

• 社団法人情報処理学会の論文
• 2002-09-15

著者

• 佐藤 雅彦

  京都大学大学院情報学研究科

• 松河 雅宏

  京都大学大学院情報学研究科

• 佐藤 雅彦

  Department Of Information Science Faculty Of Science University Of Tokyo

• Sato Masahiko

  Graduate School Department Of Mathematics Kyoto University

• Sato Masahiko

  Department Of Information Science Kyoto University

• 佐藤 雅彦

  京都大学大学院エネルギー科学研究科

関連論文

• 計算と論理のための自然枠組NF/CAL(システム検証の科学技術)
• フレーゲの計算機科学への影響 (特集 フレーゲの現代性)
• 数学記号の認知速度 : 実験心理学的計測方法と実例
• Polyvariant Specializationon Type-directed Partial Evaluation
• Constructive Data Refinementの証明技法の改善
• 二階文脈計算(プログラミング及びプログラミング言語)
• 定理証明システムCoq上でのPre Logical Relationを用いた詳細化の正しさの証明
• 型情報を一部明示した環境計算体系
• A Second Order Typed Context Calculus
• 型付きλ計算の拡張によるMobile計算の定式化
• オメガ正規言語の測度が有理数であること
• プログラム理論 A Type-Free Context Calculus
• 適切さの論理を用いた帰納論理プログラミング
• 発見科学の構想と展開(発見科学)
• 参照透明な代入を持つ純関数型言語
• 自己反映的証明体系RPTの理論と実現
• ソフトウェア科学会第3回大会
• 17aRA-6 非線形抵抗性壁モードのモデリング
• 構成的理論に基づいたプログラミング言語Zとその実装
• 22pXG-13 負磁気シアートカマクにおける非線形ダブルテアリングモード
• 情報学科シンポジウム
• A Formal Theory of Symbolic Expressions(LOGIC AND THE FOUNDATIONS OF MATHEMATICS)
• Algebraic Structure of Symbolic Expressions (Mathematical Studies of Information Processing)
• ニセ金発見パズルについて (計算機によるパズル・ゲームの研究)
• On Formal Fractions Associated with the Symmetric Groups (組合せ構造とグラフ理論)
• 2個の生成元を持つFree IN-Algebra及びFree ICN-Algebraの決定 (数理論理とモデル理論)
• Lゲームの計算機による分類 (計算機によるゲームとパズルをめぐる諸問題研究会報告集)
• Nonlinear Double Tearing Mode in Negative Shear Cylindrical Tokamaks
• Classical Brouwer-Heyting-Kolmogorov interpretation
• A Classical Catch/Throw Calculus with Tag Abstractions and its Strong Normalizability(Type Theory and its Applications to Computer Systems)
• On the Periods of Certain Pseudorandom Sequences
• ACUTE MYOCARDIAL INFARCTION IN FUKUSHIMA AREA OF JAPAN
• Nonlinear Double Tearing Mode in Negative Shear Cylindrical Tokamaks
• 8aSS-1 簡約化MHDモデルによる新古典テアリングモードの解析((理論・数値解析),磁場閉じ込め,領域2)

もっと見る 閉じる

スポンサーリンク