Using CafeOBJ to Mechanise Refactoring Proofs and Application
リファクタリングのルールが正しいことの証明を CafeOBJ を使って半自動的に行おうという論文。ROOL という Refinement Calculus をベースにした言語に対し、条件付きの書き換えとしてリファクタリングを定義。その書き換えが正しいことを言語の意味論と補題を使って証明している。第三著者の博論で展開された議論を CafeOBJ を使って再現したみたい。この論文では「メソッド抽出およびインライン化」と「フィールドのカプセル化」が例に挙げられている。
ここで定義されたリファクタリングを行ってもプログラムの結果が変わらないことはわかるけど、なんとなく違和感があるのは意味論が公理系のようなものだからかな。
author="Antonio Carvalho Junior and Leila Silva and Marcio Cornelio",
title="{Using CafeOBJ to Mechanise Refactoring Proofs and Application}",
booktitle="Brazilian Symposium of Formal Methods",
page="32--46",
year="2005"
A Theorem Proving Approach to Analysis of Secure Information Flow
定理証明器を使って情報流解析しようという論文。機密度の低いデータが高いデータに依存しないことを論理式で表して、プログラムが満たしているか定理証明器を使って確かめる。満たしていれば安全な情報流であるといえる。この論文では論理式に Java Card DL (Dynamic Logic) を、定理証明器に KeY を使っている。
author="Adam Darvas and Reiner Haehnle and Dave Sands",
title="{A Theorem Proving Approach to Analysis of Secure Information Flow}",
booktitle="Proceeding of 2nd International Conference on Security in Pervasive Computing",
volume="3450",
series="LNCS",
publisher="Springer",
page="193--209",
year="2005"
Changing Programs Correctly: Refactoring with Specifications
リファクタリング操作がプログラムの振舞いを変更しないことを形式的に保証しようという研究。プログラムの状態を、変数、ヒープ、IO 操作の 3 項組とし、ステートメント単位で状態遷移を定義してプログラムを形式化。リファクタリング操作を、元のプログラムとリファクタリング後のプログラムの対応として定義して、それぞれの IO 操作が同じであれば振舞いが同じであるとする。プログラムの振舞いを IO 操作の列として定義しているのが特徴的。論文では「フィールドの移動」を例として挙げて、リファクタリング操作が IO 操作を変更しないことを示している。
この論文はカンファレンスに投稿された論文で、基になったテクニカルレポートも読まないといけない感じ。190 ページあるけど。
author="Fabian Bannwart and Peter Muellar",
title="Changing Programs Correctly: Refactoring with Specifications",
booktitle="Formal Methods 2006",
publisher="Springer",
volue="4085",
series="LNCS",
pages="492--507",
year="2006"
カンファレンスは今年の 8 月で、プロシーディングはまだ出版されていないので volume と pages は不明。
Downgrading Policies and Relaxed Noninterference
機密度を下げる仕組みを導入した情報流解析に関する論文。従来の手法では機密度は上がりこそすれ下がることはなく、非干渉性は非常に強い性質になっていたため現実的ではなかった。そこで、どのようにすれば機密度を下げる（downgrading）ことができるかその仕様を与え、プログラムがそれを守っているか静的に解析する。仕様をラベルとしてプログラムに付け、型システムにかける。非干渉性は、仕様で与えられたよりも低い機密度を持つデータに影響しないことと緩められる。
author="Peng Li and Steve Zdancewic",
title="{Downgrading Policies and Relaxed Noninterference}",
booktitle="POPL'05",
pages="158--170",
year="2005"