形式手法の一つであるBメソッドは仕様と実装間の無矛盾性を機械的に検証し保証する。我々はBメソッドを用いたソフトウェア自動生成手法を提案している。本手法では既存ソフトウェアから得られた部品を再利用することでソフトウェアを合成するが、部品が存在しない場合は人が手で記述をしていた。本研究は不足部品を機械が可能な限り自動生成することで人の負担の低減を目標とする。不足部品の生成は以下のように行う。既に取得されている部品群から詳細化情報を収集し、仕様と実装の変数間の関係を抽出する。抽出した情報と仕様の操作を基に、実装での操作を機械的に生成する。本稿では特定の詳細化がされた変数から成る不足部品の自動生成手法について提案する。