日々の流転

λ. “State of the Union: Type Inference via Craig Interpolation” by Ranjit Jhala, Rupak Majumdar and Ru-Gang Xu

• <URL:http://www.cse.ucsd.edu/~rjhala/papers/state_of_the_union.html>
• <URL:http://www.springerlink.com/content/h601x44p4379h410/>

<URL:http://fixedpoint.jp/2007/02/10/state_of_the_union.html> より。

Cの共用体は、どの型がいま共用体に格納されているかを覚えていないので、通常タグフィールドと組み合わされて利用される。ので、安全なアクセスであることを検証するために、共用体に対するアクセス時にタグフィールドに関する条件が成り立っていることを静的にチェックすることが考えられる。

条件はアノテーションとして与えることが考えられるけど、ここでは自動的に発見していて面白い。 どうやるかというと、共用体へのアクセスをコントロールフローグラフ(CFG)上で支配するような条件文を集めてきて、各型でアクセスするための条件はdisjointであるはずといった制約を仮定し、Craig Interpolation を使って条件を発見している。 実装は、Cのソースコードの操作やコントロールフローグラフの作成に CIL を、Craig Interpolation に FOCI を利用。

Craig Interpolation が何故こういうことに使えるのか、私はまだ理解できていないので、An interpolating theorem prover を読んでみたいところ。