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

代数的手法を用いたプログラムの階層的設計と開発環境に関する研究

利用代数方法进行程序和开发环境的层次化设计研究

基本信息

批准号：
05680273
负责人：
谷口健一
金额：
$ 1.15万
依托单位：
Osaka University
依托单位国家：
日本
项目类别：
Grant-in-Aid for General Scientific Research (C)
财政年份：
1993
资助国家：
日本
起止时间：
1993 至无数据
项目状态：
已结题

项目摘要

種々の実用プログラムが順序機械型プログラムとして記述できる.本研究では主に,代数的手法を用いた順序機械型プログラムの階層的設計の正しさの証明(設計検証)の計算機支援環境を考案する.代数的言語の使用により,検証は項書換え等の単純な手法の組合せで行えるが,従来は,種々の手法を人間が複雑に組合せて適用しており,自動化が困難であった.1.本研究では,仕様記述スタイルに制限を設けて,検証を自動化できる検証手順を考案した,記述スタイルの制限により,証明対象式を(恒真性判定可能な)加減算を含む整数上の理論式に帰着でき,一定の検証手段の組合せ方で検証を行える.この記述スタイルでは,整数配列等を用いても論理式の恒真性判定が可能となり,実用上有効である.2.構造的帰納法を用いる場合,証明に必要な補題の選定や代入を検証者が検証過程を管理しながら行うのは非常に繁雑である.そこで以下のように計算機支援の方法を定めた.構造的帰納法では,必要な言明を着目する状態に与えるが,この際,図表示された状態遷移図上で言明を与えられるようにGUIを設計した.証明に必要な補題の選定や代入に関しては,計算機が候補を自動的に選出し,検証者が最終的に指定する.そのもとで支援系は必要な証明対象式を自動生成し,証明に行う.また,証明過程を管理し,言明の変更に対して再度証明すべき個所を表示する.3.少ない労力で検証可能であることを実証するため,GUIを用いて上記2.に基づく機能を与える検証支援系を作成した.4.本支援系を用いて,マックスソートプログラムの設計検証を,試行錯誤を含め2日程度で行った.その証明では式長が1000トークン程度の論理式の恒真性判定が必要であるが、恒真性を高速に判定する方法を考案したことにより,数秒程度で判定できた.5.これらの結果,本検証手順及び支援系が有効であることが分かった.記述クラスの拡張およびそれらの検証法を考案すること等が今後の課題である.

This kind of practical application program is described in detail in the sequential mechanical program. In this paper, we study the design of hierarchical design of sequential mechanical model by using the main algebraic method and the computer support environment. The use of algebraic speech is difficult to automate. 1. This study describes the use of algebraic speech in the design of algebraic speech control. 2. The use of algebraic speech in the design of algebraic speech control is difficult to automate. 3. The use of algebraic speech control is difficult to automate. Prove that the corresponding formula (constant truth judgment possibility) addition and subtraction contains the theoretical formula on the integer, and the combination of certain verification means can be verified. 2. The structural inclusion method is used in the case where the proof is necessary, the selection of the supplementary problem, the substitution of the verifier, the verification process, the management of the operation, and the complexity of the verification process. The following methods of computer support are defined. The structure of the method of inclusion is necessary to express the state of the eye, and at the same time, the expression of the state transition is clear and the GUI is designed. The computer automatically selects the candidate for the test and specifies the candidate for the test. The support system is necessary to prove that the object formula is automatically generated and the proof is executed. 2. Basic functions and verification support system are created. 4. This support system is used to create design verification and trial errors. The proof is necessary to determine the authenticity of a logical formula that is as long as 1000 tokokens, and the method for determining the authenticity at a high speed is considered. The determination can be made in seconds. 5. As a result, this verification manual and support system are effective. This paper describes the research on the method of identification and the problems in the future.