HOME>組織の紹介>ツール開発>Agda

Agda

Agdaを用いた数理的技法に基づく検証の普及に向けて

CVSでは、数理的技法に基づく種々の検証技術の普及と発展を目的とし、統合検証環境の研究開発を行っています。

数理的技法

数理的技法は、ユーザの指示次第で広範囲の問題に適用可能な定理証明と、全自動で定型的問題を解く自動検証に大別されます。これらの両方の長所を実際の現場で利用可能にするような検証環境の整備により、社会におけるディペンダビリティの飛躍的向上が見込まれています。

▲ページ先頭へ

Agdaとは

Agdaはシステムを正しく開発するための環境で、定理証明による検証を支援するソフトウェアシステムです。Agda言語を使うと、プログラム、プログラムの仕様、プログラムが仕様を満たすことの証明を、Martin-Lof 型理論という汎用プログラミング言語の枠組ひとつで記述することができます。

CVSでは、Agda処理系について2004年からスウェーデンのシャルマース工科大学と研究協力し、また独自にAgdaと自動検証を組み合わせた「統合検証環境」の研究開発を行ってきました。Agdaを用いた企業共同研究として、鉄道運賃計算プログラムや通信プロトコル処理といった組込みシステムを題材とした複数の事例開発なども行っています。

▲ページ先頭へ

Agdaを使う利点

Agdaを使うと、以下のものが利用できます。

Agda言語
Agdaシステムは、Agda言語による記述の構文エディタ、Agda言語による証明記述の証明検査器、Agda言語によるプログラム記述のコンパイラなどを提供します。Agda言語は汎用であり記述力も高いため、例えばシステムLSIの仕様を書いて、その内部矛盾を自動的に検出することもできます。
定理証明
定理証明による検証というのは、システムが仕様をみたすことを、論理的な推論を積み重ねた形式的証明というものを作ることで確かめる、という方法です。自動検証の技法として広く知られているモデル検査が定型的な問題しか扱えないのと比べて、より汎用性が高いという利点があります。しかしその分自動化はより難しく、ボタン一発で証明が出てくる、というわけにはいきません。
対話型支援
Agdaは対話型支援を提供してくれます。これは、作りかけの証明やプログラムを、ユーザからのコマンドとそれに対するAgdaの応答という対話で完成させていくものです。各ステップの正しさをAgdaが保証してくれるので、完成品は必ず正しい、ということになります。

▲ページ先頭へ

統合検証環境の研究開発

  統合検証というのは、対話型検証と自動検証を組み合わせるものです。典型的なシナリオは次のようになります。もともとの検証問題全体を自動検証ツールで検証しようとしても、しばしば問題が複雑すぎる、あるいは大きすぎるなどの理由で、ツールによる答えは「正しいかどうかわからない」となります。ここで人間が知恵を使い、対話型検証で正しさを確保しつつ問題を分割するなり変形するなりします。自動で検証できる検証と人間の知恵を要する証明をこのように組み合わせるのが統合検証です。
  対話型証明はデータを入れれば結果が出るという押しボタン式ツールより手間がかかりますが、実は押しボタン式ツールを使う場合にも、手元の問題をツールが扱える形にする部分で、ユーザの知恵と手間が非常にかかっているのです。汎用性の高い対話型支援は、この人が知恵を使う部分を確実にしてくれるという利点があります。CVSでは、対話型証明の途中で柔軟にモデル検査器などの自動検証ツールを呼び出すことを可能にする統合検証環境の研究開発を行ってきました。

▲ページ先頭へ

仕様安定版処理系の開発

  CVSでは、Agdaを用いた検証技術が実問題の検証において効果的に使用できることを数々の実験により確かめてきていますが、それと同時に本検証技術の普及には、処理系の流動性に起因するいくつかの障壁があることも明らかになってきました。そこで現在CVSでは、安定した仕様をもつ処理系Agda-Aの開発を進めています。本処理系は、研究用プロトタイプであった従来のAgda処理系の仕様を安定化したものであり、Agda言語による仕様や証明などの記述を、長期間にわたって継続的に使用可能にすることを目的としています。同時に、処理系の使い方に関するドキュメント類の蓄積を行うことも可能にします。また、実用的な問題に現れる大規模データが処理できるように処理系を抜本的に高速化することも目的の一つです。 本処理系の開発により、Agdaを用いた統合検証環境の技術移転活動での使用を可能にし、社会における情報システムのディペンダビリティ向上に貢献することを目指しています。

▲ページ先頭へ

関連サイト

◆ 関連サイト
Agda Wiki  http://wiki.portal.chalmers.se/agda/pmwiki.php
 
 

▲ページ先頭へ