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"