我々は形式手法の1つであるBメソッドを用いたソフトウェア自動合成手法を提案している。この手法では既存ソフトウェアを部品化し、これを再利用することで要求仕様を満たすソフトウェアを自動合成する。従来では不足部品を可能な限り自動生成していたが、抽象データ型に詳細化されるべき変数を含む不足部品は実装における操作を決定できず、対応していなかった。本研究ではライブラリで定義された抽象データ型の変数を含む不足部品の自動生成を目標とする。要求仕様の操作と抽象データ型の操作の事前条件と事後状態の整合性を定理証明器で検証することで、抽象データ型のどの操作が要求仕様を満たすかを決定する手法を提案する。