权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

二分決定グラフを用いたプログラム検証の自動化に関する研究

基于二元决策图的程序验证自动化研究

基本信息

批准号：
09780231
负责人：
近藤久
金额：
$ 1.6万
依托单位：
Ibaraki University
依托单位国家：
日本
项目类别：
Grant-in-Aid for Encouragement of Young Scientists (A)
财政年份：
1997
资助国家：
日本
起止时间：
1997 至 1998
项目状态：
已结题

项目摘要

今年度は、前年度に得られた結果を項書換え系完備化手続きに応用する研究を行なった。その概要は以下のようにまとめられる。1. KnuthとBendixによって提案された完備化手続きは与えられた等式集合と等価で完備な項書換え系の生成を試みる(半)アルゴリズムである。等式集合を代数的仕様とすれば、完備化手続きは仕様から実行可能なプログラムを生成するコンパイラとみなすことができる。また、定理自動証明など種々の応用において非常に有用な手法でもある。しかし、完備化手続きの結果は与えられた簡約順序に大きく依存する。少なくとも以下の問題点が挙げられる。(a) 生成される項書換え系の停止性を保証するための簡約順序を利用者に要求する。(b) 簡約順序が不適当な場合、手続きが無限に継続する場合がある。(c) 簡約順序が適当な場合にも(完備な項書換え系が存在するにもかかわらず)失敗する場合がある。研究代表者は(b)の問題点を解決するために、平成6、7年度の研究において複数の簡約順序を同時に扱う完備化手続きを提案、実現し、その成果を学術論文誌等に発表している。しかし、提案した手法では(a)の問題点が解決できていなかった。2. 1(a)で述べた問題を解決するため、前年度提案した停止性検証のための二分決定グラフの利用法を平成6、7年度に研究した複数の簡約順序を同時に扱う完備化手続き対して適用し、新たな完備化推論規則を得た。3. 2.で得た完備化推論規則を多くの項書換え系に適用し、その効果を確認した。4. 現在も継続して、計算機上での実現及び改良を行っている。これまでの研究業績を国内全国大会、国際会議にて発表し、論文誌に投稿(採録決定)した。

This year, the results of the previous year's study were changed to complete the manual study. A summary of the following is provided. 1. Knuth Bendix is a complete set of equations and a complete set of equations. The set of equations is algebraic, complete, and can be generated. The theorem is automatically proved by a very useful method. The result of the completion of the manual is dependent on the order of reduction. The following questions are answered: (a)To ensure the continuity of the system, the user must have a simple order of operation. (b)Simple order is not appropriate, hand is not infinite, and so on. (c)The order of reduction is appropriate for the occasion. The research representative presented the proposal, implementation, and results of the research on the problem of (b) in the sixth and seventh years of Heisei, including the reduction order of the plurality, and the completion of the manual. The solution to the problem is to propose a solution to the problem. 2. 1.(a) To solve the above problems, the previous year's proposal was stopped, and the binary decision was made. The utilization method was studied in the sixth and seventh years, and the multiple reduction order was simultaneously completed. The new completion inference rules were obtained. 3. 2. Complete inference rules are applied to a variety of systems, and results are confirmed. 4. Now it's time for you to go to the computer, and it's time for you to improve it. The research achievements are presented at national conferences and international conferences, and papers are submitted (accepted and recorded).