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 は不明。