プログラム生成システム PAPYRUS

スポンサーリンク

概要

• 論文の詳細を見る

• Curry-Howard Isomorphismに基づくプログラム生成法では,論理式に対しプログラムの仕様としての解釈を定義し,論理式の証明から誤りのないプログラムの生成方式をあたえる.PAPYRUS(PArallel Pro-grams sYnthesis by Reasoning Upon formal System)は,このような方法をベースとしたプログラム生成実験システムであり,大まかには以下の2つの機能を提供する.1つは,論理や表記法,プログラム生成規則の管理と,これらの定義のもとでの証明チェックやプログラム生成の機能で,型論理の1つであるCC(Calculus of Constructions)における型推論機能とTRS(Term Rewriting System)の技術により実現される.これらの定義を変更することにより,プログラム生成のためのさまざまな論理や表現方法,実現可能性解釈を利用することができる.もう1つは,証明作成の簡単化を目的とする証明エディタ機能であり,(1)適用可能な推論規則の表示と,選択された規則による自動証明展開機能,(2)部分証明が構成されるたびに行われる自動証明チェック機能(この機能により完成した証明はその時点で正しさが保証される),(3)未証明部をプルーバに証明させる機能などがある.本稿ではPAPYRUSの原理と構成,機能について述べる.

• 一般社団法人情報処理学会の論文
• 1994-01-15

著者

• 藤田 正幸

  三菱総合研究所

• 藤田 正幸

  株式会社三菱総合研究所

• 藤田 正幸

  (株)三菱総合研究所

• 藤田 正幸

  三菱総研

• 川田 秀司

  (財)新世代コンピュータ技術開発機構 (株)東芝システム・ソフトウェア生産技術研

• 坂井 公

  筑波大学電子・情報工学系

• 白井 康之

  (財)新世代コンピュータ技術開発機構

• 大坪 透

  (株)ヴァンリッチ,にっかつ芸術学院映像科

• 大坪 透

  (株)ヴァンリッチ にっかつ芸術学院映像科

関連論文

• 反証による代数的仕様記述の検証支援
• プロフィーリング法に基づくクレジット入会審査エキスパート・システム(QCとAI)
• プログラム生成システム PAPYRUS
• Metis-AS における代数的仕様の検証手続き
• 等式論理の帰納的定理を証明する手続き
• Universal Algebra for Computer Scientists, Wolfgang Wechler, Springer-Verlag, 1992
• 市場金利変動分布とLevy-Flightモデル
• MGTP による有限代数の新事実の発見
• PIM上の並列定理証明系MGTP
• インターネットのおとし穴 (インターネットのおとし穴)

スポンサーリンク