netail.net

_ [論文] 副作用のないメソッドの自動検出 ▲

Alexandru Salcianu and Martin Rinard: Purity and Side Effect Analysis for Java Programs.

Proceedings of the 6th International Conference on Verification, Model Checking and Abstract Interpretation. Paris, France January 2005.

外部に副作用を残さないメソッドを JML などでは pure メソッドと呼んで，アサーションの定義に使えるようにしているが，@pure の指定は手作業になる．それを自動的に検出する方法を提案している．既存の研究と異なる点は，メソッド内で新しいオブジェクトを確保したとき（一時使用のイテレータなど），そのオブジェクトに対するデータの書き込みは許容するところ．

各メソッドごとにどの変数がどのオブジェクトを指すかを示す Points-To グラフを構築しておき，メソッド呼び出し関係をたどるときに呼び出し側の Points-To グラフのノードと，呼び出し先のグラフとで，対応する引数やthis参照を接続することで，呼び出し先まで含んだ解析グラフにしていくらしい．末端にnativeメソッドが入ってしまうと解析できないので，いくつかには手であらかじめ定義したグラフを与えている．

_ 皮膚科 ▲

背中にあった1cmくらいのほくろから出血があったので，蛍池駅前の奥野皮膚科まで出かけてきた．てきぱきと診察されて，液体窒素らしきものでほくろの部分を焼かれる．けっこう痛い．