| 研究概要 |
プログラムの安全性向上のために型理論に基づいたプログラム解析・検証・変換などの研究を行っている.本年度の主な研究成果は以下のとおり.
1.型に基づく並行プログラムの解析手法の改良
型に基づいて並行プログラムのデッドロックなどの解析を行う手法を改良し,再帰を用いて記述されたプロセスのデッドロックの有無を従来よりも精度よく解析できるようにした.
2.順序付き線形型に基づくXMLストリーム処理プログラム生成手法の改良
順序付き線形型に基づいてXML処理プログラムを効率のよいストリーム処理プログラムに安全に変換する従来の手法を改良し,バッファリング操作の自動挿入を可能にした.それにより,プログラマが順序付き線形型を意識しなくてもストリーム処理プログラムの生成することが可能になった.
3.資源使用法解析の拡張
ファイルやメモリなどの計算資源が正しく使用されているかどうかを検証する手法の拡張し,並行プリミティブや例外処理機構の入ったプログラムを扱うことを可能にした.
4.プログラムの等価性の検証手法の研究
プログラムの等価性を示す手法として,論理関係や双模倣などの手法があるが,現実のプログラムで必要となる再帰関数・再帰データ型・抽象データ型などを扱える手法が確立していなかった.本研究では双模倣の概念を発展させ,それらを扱える健全かつ完全な手法をはじめて与えた.また,プログラム等価性の一種である,情報流解析の正当性の基準として用いられる非干渉性についても論理関係を用いて証明する技法を考案した
|
