構成的型理論に基づいた定理証明プログラムの試作
スポンサーリンク
概要
- 論文の詳細を見る
情報化社会においてソフトウェアの迅速で妥当な開発技術が強く求められているが,その要求に答えるにはソフトウェア開発方法の見直しが必要である。その1つの方法として,構成的プログラミングの考えに基づいてソフトウェアの仕様からその妥当性の検証とプログラムの導出を同時に実現し,更に,順次に追加される仕様の要求に対して,ソフトウェアを内部で矛盾を解消しながら拡大・発展させる見方がある。本稿では,このような枠組みの中で必要となる仕様からプログラムを導出するための定理証明プログラムを構成的型理論に基づいてRuby言語を用いて試作した。