代数的仕様の実用プログラムへの適用に関する考察

概要

論文の詳細を見る
コンピュータが社会の幅広い領域に浸透するにつれ、信頼性の高いプログラムを作成する必要性が高まっている。この必要性を満足する可能性のあるプログラム開発法の一つとして、代数的仕様記述法が注目され始めている。代数的仕様記述法は、数学的に厳密な定義が与えられた形式性を持ち、これを基に、機械的な仕様の検証やソースコードの生成が可能になる。また、等式論理を基礎にしているため、検証系や実現系を作りやすいという長所もある。しかし、現場レベルで使用するには、仕様を記述する立場からみると、(1)基礎となる理論を理解しないと仕様が書けないが、これが難しい。(2)理論に従って厳密に仕様を記述すること自体が、難解な作業である。(3)仕様が冗長になり、記述に時間がかかる、仕様に誤りが入りやすい。などの問題がある。一方、仕様を見る立場からは(4)仕様を理解しにくい。という問題がある。しかし、代数的仕様記述法は、信頼性の高いプログラムを開発する上で、原理的に優れた方法なので、上記の問題を解決して現場レベルで利用できるようになることが望まれる。
一般社団法人情報処理学会の論文
1990-03-14