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

1989 Fiscal Year Annual Research Report

• Project/Area Number: 01550286
• Research Institution: Osaka University
• Principal Investigator: 谷口 健一 大阪大学, 基礎工学部, 教授 (00029513)
• Co-Investigator(Kenkyū-buntansha): 松浦 敏雄 大阪大学, 基礎工学部, 助手 (40127296) ; 東野 輝夫 大阪大学, 基礎工学部, 講師 (80173144) ; 杉山 裕二 岡山大学, 工学部, 教授 (50116050)
• Keywords: 代数的手法 / 仕様記述 / 詳細化 / 証明 / 証明支援システム / 証明書

Research Abstract

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

Research Products

• [Publications] 日高博: "ASLシステムを用いたプログラム開発と証明書作成" 1989年電子情報通信学会 秋季全国大会講演論文集(分冊6). SD-7-1. 248-249 (1989)
• [Publications] 日高博: "代数的言語ASLで記述されたプログラムの正しさの証明と証明書の作成" 電子情報通信学会 技術研究報告. SS89-23. 45-54 (1989)
• [Publications] 大蘆雅弘: "スクリ-ンエディタの仕様記述と抽象的順序機械型プログラム" 電子情報通信学会 技術研究報告. SS89-24. 55-64 (1989)
• [Publications] 大蘆雅弘: "代数的言語ASLにおける抽象的順序機械型プログラムとその処理系" 電子情報通信学会論文誌D-1、投稿中. (1990)
• [Publications] 日高博: "代数的言語ASLで記述されたプログラムの正しさの証明" 電子情報通信学会 論文誌D-1、投稿予定.
• [Publications] 岡野浩二: "酒屋在庫管理の仕様記述とそのプログラムの正しさの証明" 電子情報通信学会 技術研究報告、発表予定. (1990)