酒井政裕

ForgeはDennisらによって開発されているプログラム検査エンジンであり、ヒープ操作を含むようなプログラム及び仕様を関係論理と呼ばれる論理で表現し、プログラムが仕様を満たしているかをSAT ソルバを用いた有界モデル検査(Bounded Model Checking)によって検査することが出来る。しかし、ForgeはJaveに適用することを念頭に作られているため、C言語のようなポインタ演算を持つ言語へはそのまま適用できない。我々はForge を用いてC言語プログラムの検査を行うツールCForgeの開発を試みた。本稿ではその実装方法と評価について述べる。 我々は、C 言語特有のポインタ演算を関係論理で表現するためにFat Pointer に基づいた方法を用い、仕様記述言語としてはJML 風の言語を用いた。また、CForge を用いてC 言語の標準ライブラリの一部や初等的なアルゴリズム...

純粋関数型言語の最適化手法としてプログラムの代数的性質に基づいた推論と変換は重要な位置を占めており、特に再帰的なデータ型を始代数とみなすことによって得られる融合変換のための手法が知られている。 しかし、一方で非正格な言語では始代数とみなせないデータ型が存在し得る。そのためこれらの手法を非正格な言語に適用するには、従来は適用対象の関数が正格である場合に限定する必要があった。 本論文ではこの問題について論じ、非正格な言語のデータ型に対応する始代数が存在する為の十分条件を示す。これにより関数の正格性を条件とせずに、始代数の存在を前提とした変換が可能になる。この条件は単純かつ一般的なもので、通常の関数型言語で用いられる多くのデータ型に対して適用できる。