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

基于契约的功能程序设计正确性保证研究

基本信息

批准号：
17700032
负责人：
岡野浩三
金额：
$ 2.3万
依托单位：
Osaka University
依托单位国家：
日本
项目类别：
Grant-in-Aid for Young Scientists (B)
财政年份：
2005
资助国家：
日本
起止时间：
2005 至 2006
项目状态：
已结题

项目摘要

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

这项研究旨在设计基于DBC编写的程序模块的规格，并根据申请人先前的研究结果，正式确保后者与实施它们的功能程序相遇的验证方法，并根据程序开发的效率与验证方法的申请限制进行了验证化学的验证实验，并从程序开发的效率效率上评估其有用性。今年，我们将介绍.net。在框架上为F＃设计了针对对象的F＃的验证方法，并根据其实现了验证支持系统。具体而言，（1）在意识到面向对象的设计的情况下，在面向对象的程序中引入了对象不变（类不变），（2）响应了完整性有效性证明，（3）引入了极限量子标签。（1）使得与主流面向对象的设计变得容易处理，并且期望角色描述可以提高写作的易度性和简化。（2）提高了程序的可靠性，（3）提高了写作能力。此外，目标语言由Microsoft.net设置。通过结合F＃，一个框架，可以通过将基于组件的设计方法与基于模块的设计方法相结合，可以显着增加可以创建的程序数量。现有组件已经被检查，在许多情况下它们非常可靠。如果使用此方法验证了用F＃编写的系统，则可以通过与现有组件相结合来创建它的优势。最后，可以提及该方法的正式介绍。