| 研究概要 |
cardinality analysisに関しては、様相論理式・とグラフの変換操作・(x:=y,x:=y.f,x.f:=yのいずれかの形)に対して、局所的最弱前条件(local weakest precondition)wp(・,・)の定式化を行った。この定式化を用いて、論理式・を満たすノードの数が減少するための十分条件を与えた。すなわち、様相論理式[o](wp(・,・)・・)および・o・(wp(・,・・)・・)が成り立つとき、・を満たすノードの数が真に減少する。この十分条件を用いて、リスト処理を行う具体的なプログラムの停止性を示した。
また、グラフ構造とその変換操作の表現力を向上させるために、階層的な様相論理の定式化を行った。この様相論理の枠組のもとでは、階層的なグラフ構造(グラフの中にグラフを入れ子として含むことのできる構造)とその変換操作を自然に表現することができる。各変換操作に対する最弱前条件の定式化も行った。
停止性解析および活性解析に関しては、遷移述語抽象化に対する既存手法の効率化と高精度化を、その実装も含めて行った。効率化に関しては、遷移述語をノードとする有向グラフを強連結成分に分解し、内側の強連結成分から順に解析を行うことにより、全体の解析の効率を大幅に向上させることができた。
以上に加えて、cardinality analysisを一般化するため、様相論理式をmin-plus代数を用いて解釈する方法を着想し、次年度の主たる研究テーマとする計画を立てた。この解釈のもとでは、様相論理式を満たすノードの数だけでなく、たとえばノードからノードへの最短経路の長さなども様相論理式によって表現できるため、cardinalityだけでなく、さまざまな尺度による停止性解析および活性解析が可能になる。
|
