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

点击翻译按钮获取中文摘要

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