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

代数的手法によるプログラムの正しさ証明システムの作成に関する研究

利用代数方法创建程序正确性证明系统的研究

基本信息

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

来源：
https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-01550286/
关键词：
代数的手法仕様記述詳細化証明証明支援システム証明書

项目摘要

1.従来から開発中であった代数的言語ASLの仕様記述の証明支援システムを用いて、クイックソ-トプログラムの正しさ証明を一部行ってみて、新たに必要な機能等の抽出を行った。2.従来作成していた証明支援のための基本機能に、1.で検討した支援機能を付加し、代数的言語ASLのための新しい「プログラム証明システム」を試作した。新しいシステムでは、場合分け管理機能の充実や、試行錯誤的に行った証明過程の履歴(証明を行う人が入力したコマンドやシステムからの出力の履歴)から「証明書」(証明の過程を必要な部分だけ簡潔に自然語で記述したもの)を機械的に記述する機能、等を実現した。証明書の文は自由に指定できるように工夫した。証明システムはC言語で作成され、サイズは約15000行である。3.上述のクイックソ-トプログラムの他に、酒屋の在庫管理、スクリ-ンエディタ等の仕様をASLで記述し、段階的に関数型プログラムあるいは抽象的順序機械型プログラムまで詳細化し、実行した。又、上述の証明システムを用いてそれらのプログラムの正しさの証明を行った。クイックソ-トプログラムは文法40行、公理50行、仕様も加えるとそれぞれ50行、110行であるが(略記法等を用いている)、証明に要したコマンド操作回数はSUN3規模の計算機で1000回強でるった。証明書の長さは2000〜5000行程度になる。証明に要した期間は院生で2〜3か月であった。このように証明支援システムを用いて、実際にプログラムの正しさの証明が可能であることが確かめられた。4.関数型プログラム及び抽象的順序機械型プログラムを効率よく実行するためのコンパイラを作成し、本研究での証明システムと合わせ、ASLプログラム設計開発システムを構築中である。今後は、仕様の詳細化過程及びその過程全体の支援に関する研究が望まれている。

1. To extract the necessary functions from the speech ASL description of the development of the language ASL, to support the use of the language ASL description, to verify the correct language ASL description, and to implement the new language ASL description. 2. To create the basic functions of the support system; 1. To search for the support system; 2. To add the new functions of the algebraic language ASL; 3. To create the basic functions of the support system. The function of management in case of new problems, the function of trial error, the function of proving process (proving process), the function of mechanical description, etc. are realized. The certificate is free to specify the time The proof is that the C language is about 15000 lines long. 3. The description of the above-mentioned problems, such as the management of the liquor store, the management of the liquor store, the description of the relevant numerical type of the liquor store, and the description of the abstract sequential mechanical type of the liquor store are detailed and implemented. In addition, the above-mentioned proof system is used to prove the correctness of the system. The syntax of the system is 40 lines, the axioms are 50 lines, the characters are 50 lines, the characters are 110 lines, the proof is 1000 lines, and the number of operations is SUN3. The length of the certificate is 2000 ~ 5000 degrees. The proof is that the period of birth is 2 ~ 3 months. The proof of this is that it is possible to verify the validity of the application. 4. In this study, we demonstrated that the system design and development of ASL system is under construction. In the future, the detailed process and the overall support of the process are expected to be studied.