GeneSysによるプログラム生成例とIntroduction規則の追加

摘要

プログラム生成系GeneSysは一階述語論理で記述された仕様からの実行可能なプログラム生成を目的とした手法である．本論文では，よく知られたいくつかのプログラム合成例にGeneSysが適用できることを示す．また，GeneSysでは実行可能なプログラムを生成できない仕様の一例を挙げ，等式を追加する新たな変換規則Introductionによりこの仕様からのプログラム生成が可能になることを示す．