契約に基づいた関数型プログラム設計に対する正当性保証に関する研究

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

本研究ではDbCに基づき記述したプログラムモジュールの仕様とそれを実装した関数型プログラムに対し,後者が前者を満たすことを形式的に保証するための検証方法を,申請者の従来の研究成果を踏まえて考案し,その有用性を,考案した手法に基づく検証支援系の試作と検証実験を通じて,検証付きプログラム開発の効率,検証の適用限界などの点から評価することを目的とする.本年度は.net framework上F#を対象に,オブジェクト指向向けの検証法を考案し,それに基づいた検証支援系を実装した.具体的にはオブジェクト指向設計を意識して,(1)オブジェクト指向プログラムのオブジェクトに対する不変式(クラス不変式)の導入,(2)全正当性証明への対応,(3)限量子タグの導入を行った.(1)によって主流であるオブジェト指向設計に容易に対応できるほか,性質記述もクラス不変式の採用による記述め容易性向上,簡潔化が見込まれる.(2)よりプログラムの信頼性保証が大きくなり,(3)より記述能力の向上が期待される.また,対象とする言語をMicrosoftの.NET Frameworkの一つであるF#とすることで,そのコンポーネントベースの設計手法とモジュールベースの設計手法を組み合わせ,作成できるプログラムの種類を大幅に増やすことが可能となる.既存コンポーネントはすでにチェックがされており,多くの場合信頼性が高い.F#で記述したシステムを本手法で検証すれば,既存コンポーネントとの組み合わせでも信頼性が高いものが作成できる利点がある.最後に手法の形式的紹介ができることも利点として挙げられる.