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

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

基本信息

批准号：
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编写的程序模块和实现它们的功能程序的规范后者满足前者。今年的任务是基于所设计的方法开发验证支持系统，并通过验证实验评估其在验证程序开发效率和验证应用限制方面的有效性。我们设计了面向对象的F#框架的验证方法，并基于它实现了验证支持系统。具体来说，考虑到面向对象的设计，我们重点关注（1）面向对象程序中对象的不变量（类不变量）。，（2）支持完整的正确性证明，（3）量词标签的推导。 (1)不仅可以轻松支持主流的面向对象设计，而且通过采用类不变量提高了描述的便利性，简化了属性描述。(2)提高了程序的可靠性。写作能力将通过(3)得到提高。另外，目标语言是微软的.NET通过使用框架之一的F#，可以将其基于组件的设计方法和基于模块的设计方法相结合，从而大大增加可以创建的程序的类型。已经检查了现有的组件。即使与现有组件相结合，也能够创建高度可靠的系统。最后，我们可以提供该方法的正式介绍也被认为是一个优点。