例外処理付きオブジェクト指向プログラムにおける情報流の安全性解析のための型システム

摘要

本論文では，例外処理機能をもつオブジェクト指向プログラムの安全性を情報流解析に基づいて検証するための型システムを提案する．例外処理による情報流は，スローされる例外とそれを捕そくする箇所に依存して変化する．この情報流を解析するためには，プログラム中の各文についてどの例外からの制御依存が存在するか把握しなければならない．我々は文がスローし得る例外の集合と文に出現する情報流のあるデータの機密度からなる安全型を導入する．この安全型に基づいて従来の型システムを拡張し，本型システムが非干渉性に対し健全であることを示す．健全性により型付け可能なプログラムは機密データを外部に漏えいしないことが保証される.