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

• Item type: Journal(1)
• 公開日: 1994-01-15
• タイトル: プログラム生成システムPAPYRUS
• タイトル / 言語: en
• タイトル: PAPYRUS : A System for Program Synthesis and Verification by Constructive Logics
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: 論文
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_6501
• 資源タイプ: journal article
• その他タイトル / その他のタイトル: ソフトウェア工学
• 著者所属: （財）新世代コンピュータ技術開発機構／現在 （株）東芝システム・ソフトウェア生産技術研究所
• 著者所属: 筑波大学電子・情報工学系
• 著者所属: （株）三菱総合研究所
• 著者所属: （財）新世代コンピュータ技術開発機構
• 著者所属: （株）ヴァンリッチ／現在 にっかつ芸術学院映像科
• 著者所属(英): en
• 著者所属(英): Institute for New Generation Computer Technology/Presently with System and Software Engineering Laboratoriy, Toshiba Co., Ltd
• 著者所属(英): en
• 著者所属(英): Institute of Information Science and Electronics, University of Tsukuba
• 著者所属(英): en
• 著者所属(英): Mitsubishi Research Institute, Inc.
• 著者所属(英): en
• 著者所属(英): VanRich Corporation
• 著者名: 川田, 秀司; 坂井, 公; 藤田, 正幸; 白井, 康之; 大坪透
• 著者名(英): Hideji, Kawata; Ko, Sakai; Masayuki, Fujita; Yasuyuki, Shirai; Toru, Ohtubo
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: Curry-Howard Isomorphismに墓づくプログラム生成法では、諭理式に対しプログラムの仕様としての解釈を定義し、諭理式の証明から誤りのないプログラムの生成方式をあたえる。PAPYRUS（PArallel Programs sYnthesis by Reasoning Upon System）は、このような方法をべ一スとしたプログラム生成実験システムであり、大まかには以下の2つの機能を提供する。1つは、諭理や表記法、プログラム生成規則の管理と、これらの定義のもとでの証明チェックやプログラム生成の機能で、型諭理の1つであるCC（Calculus of Constructions）における型推諭機能とTRS（Term Rewriting System）の技術により実現される、これらの定議を変更することにより、プログラム生成のためのさまざまな諭理や表現方法、実現可能性解釈を利用することがで妻る。もう1つは、証明作成の簡単化を目的とする証明エディタ機能であり、（1）適用可能な推論規測の表示と、選択された規則による自動証明展開機能、（2）部分証明が構成されるたびに行われる自動証明チェック機能（この機能により完成した証明はその時点で正しさが保証される）、（3）未証明部をプルーバに証明させる機能などがある。本稿ではPAPYRUSの原理と構成、機能について述ぺる。
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AN00116647
• 書誌情報: 情報処理学会論文誌; 巻 35, 号 1, p. 127-142, 発行日 1994-01-15
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7764