一般に、プログラムが与えられた仕様を満たしていると保証することは難しい。一方、計算によって仕様からプログラムを導出するダイクストラの方法が1990年代で既に考えられている。しかし、未だエンドユーザが手軽に利用できる標準ツールが実現されているとは言い難い。本研究では、この手法に基づくプログラム生成の自動化がどの程度実現できるか、ユーザとのインタラクションによって半自動的にプログラムを生成するツールの設計・実装を試みる。本発表では、簡単な整数演算プログラムの導出を題材に、ツールをどのように実現するか、プログラムの実例を挙げながら考察する。