(57)【要約】      （修正有）【課題】仕様にそのまま合致するプログラムが蓄積データに存在しない場合でも、蓄積プログラムを加工することで適合プログラムとして出力できる機会を増やし、また利用自体によって蓄積プログラムを増強する。【解決手段】プログラムの言語要素に対応してあらかじめＨｏａｒｅ論理の規則を格納するＨｏａｒｅ論理規則格納手段と、適合するプログラムコードが蓄積されていなかったときに、Ｈｏａｒｅ論理の各規則にしたがって仕様を部分プログラムの仕様に分解する仕様分解手段と、分解に用いた規則と付随するパラメータをスタックの形で格納する仕様構造格納手段と、分解して得られる仕様（部分仕様）を新たな検索キーとして検索し、得られたコードを分解前の仕様を満たすよう順次組み立て、当初の検索キーに適合するコードを合成して出力するプログラム合成手段と、合成されたコードを蓄積データに追加するプログラム登録手段を備える。【選択図】図１
2010238062.tif 000002
【特許請求の範囲】
【請求項１】
論理的仕様とともに蓄積したプログラムコード群から、検索キーとして与えられた論理的仕様に適合するプログラムコードを検索し、そのコードの正しさを検証した上で提示するデータベースのデータ蓄積／検索手段において、適合するプログラムコードが蓄積されていなかったときに、Ｈｏａｒｅ論理の合成規則の逆にしたがって仕様を部分プログラムの仕様に分解して得られるもの（部分仕様）を新たな検索キーとして検索するという動作をあらかじめ定めた深さを限度に再帰的に繰返し、限度内にコードが見つかった場合に、そのコードを分解時の規則を用いて再合成し、当初の検索キーに適合するコードを合成して出力するとともに蓄積データに追加することを最も主要な特徴とするプログラムのデータベース。
【請求項２】
請求項１において適合するプログラムの検索に失敗した場合、仕様のみを未解決データベースに登録し登録情報を周知する機構と、未解決要求に対する解としてのコードの送信を受け付け、正しさを検査のうえ解決済コードとしてコードのデータベースに登録する機構を備えていることを特徴とするプログラムのデータベース。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、プログラムのデータベースにおいて蓄積データの利用度を向上させることと、蓄積データを増強する方法に関する。
【背景技術】
【０００２】
情報資源を共有して有効利用するにはデータベースをインターネットを介して利用するなどの方法が用いられる．自然言語で記述された文書であれば全文をキーワードで検索する方法が採られる。
【０００３】
しかし、この方法は対象となる資源がプログラムのソースコードの場合、本質的に所望のものであっても、用いる場面・文脈・言語が異なるために変数名や関数名などが違い検索にかからないという欠点があった。また逆にたまたま意図した検索語をコメントなどに含むプログラムがヒットしたからといって所望の仕様を満たす保証がないという欠点があった。
【０００４】
ソースコードを共有して再利用する用途において、この２つの欠点は利用度と安全性の点で致命的である。
【０００５】
この改善策として、仕様を検索キーとし、プログラムを検証証明つきで蓄積する方法がある。この方法ではプログラムを、論理式で記述された仕様およびその正しさのＨｏａｒｅ論理による証明と組にして蓄積し、検索キーとして仕様が与えられた際に、論理的に適合する仕様と組になったプログラムをその証明とともに出力する。この方法によれば論理式で記述された仕様で検索することで利用度が向上するとともに、利用者が別途検証器によって証明をチェックすることで安全性が保証される。しかしながらこの方法では検索にヒットするコードは蓄積されたコードがそのまま論理的仕様に合致するものだけに限られる。また検証証明つきのプログラムデータを手動で入力して完備することは困難かつ非能率的である。
【特許文献１】特開２００６−０８５２０６号公報
【発明の開示】
【発明が解決しようとする課題】
【０００６】
解決しようとする問題点は、蓄積したプログラムを組み合わせたり少し加工することで所望のプログラムが得られるはずであるにも関わらず、仕様に直接適合しないがゆえに棄却されてしまう点である。利用度の観点からは、そのままでは仕様に適合していなくても、わずかの加工で所望の論理的仕様に適合するようになるプログラムを見い出し利用する方法が望まれる。さらに資源を人手による証明にもとづくデータのみに依存する非効率を改善し、利用を重ねること自体によって自動的データを拡充できる学習機構が望まれる。
【課題を解決するための手段】
【０００７】
本発明は、論理的仕様とともに蓄積したプログラムコード群から、検索キーとして与えられた論理的仕様に適合するプログラムコードを検索し、そのコードの正しさを検証した上で提示するプログラムのコード蓄積／検索手段において、プログラムの言語要素に対応してあらかじめＨｏａｒｅ論理の規則を格納するＨｏａｒｅ論理規則格納手段と、適合するプログラムコードが蓄積されていなかったときに、Ｈｏａｒｅ論理の各規則にしたがって仕様を部分プログラムの仕様に分解する仕様分解手段と、分解に用いた規則と付随するパラメータをスタックの形で格納する仕様構造格納手段と、分解して得られる仕様（部分仕様）を新たな検索キーとして検索するという動作をあらかじめ定めた深さを限度に再帰的に繰返し、限度内にコードが見つかった場合に、見つかった／得られたコードを分解時の規則を用いて分解前の仕様を満たすよう順次組み立て、当初の検索キーに適合するコードを合成して出力するプログラム合成手段と、合成されたコードを蓄積データに追加するプログラム登録手段を備えることを最も主要な特徴とする。
【発明の効果】
【０００８】
本発明のプログラムのデータベースは、検索キーとして与えられた仕様に適合するコードが蓄積データのなかに見つからない場合でも、蓄積されたコードを部分プログラムとしてあらかじめ定めたステップ数の加工によって適合化できる場合も解プログラムを出力させることができるという利点がある。加えて、このようにして新たに得られたコードを蓄積データに追加して蓄えることで次回以降の検索を高速化し、かつ適合化できるコードも漸増的に増やすことができる。
【発明を実施するための最良の形態】
【０００９】
インターネットでの利用を最大限に効率化するためにデータベースはWeb上のサービスとして実装し、仕様、プログラム、検証証明の組はＸＭＬ文書として記録／格納した。また出力結果はＸＳＬＴによってサーバまたはクライアント上で具体的なプログラミング言語のコードに変換される。
【実施例１】
【００１０】
図１は、本発明装置の１実施例の構成図である。検索キー入力器１はクライアントプログラムまたはデータベースサーバに入力されたクエリを構文解析してＸＭＬ文書に変換しプログラム検索器３に送る。仕様つきプログラム格納器２にはプログラムとプログラムの論理的仕様、およびその正しさの証明（検証証明）の組がＸＭＬ文書として格納されている。プログラム検索器３はＸＭＬ文書の形で入力された仕様を仕様つきプログラム格納器２の各文書中の仕様と照合し、適合するものを探す。もし見つかれば当該文書中のコードと検証証明を組にしてプログラム合成器７に送る。もし見つからなければ、その仕様を仕様分解器４に送る。仕様分解器４はあらかじめＨｏａｒｅ論理規則格納器５に登録したＨｏａｒｅ論理の（文法規則ごとの）規則の１つを順に選び、その規則にしたがって部分プログラムに分解した場合の各々の部分プログラムの仕様（部分仕様）に分解する。このとき同時に当該の規則と（部分プログラムの個数を含む）パラメータをスタックとして実装される仕様構造格納器６にプッシュする。プログラム合成器７はプログラム検索器３からの出力を順次内部スタックにプッシュするたびに仕様構造格納器６に最後にプッシュされたデータ（トップデータ）を参照して必要な部分プログラムの個数を取得し、プログラム合成器７の内部スタックに当該の個数のプログラムが積まれていればそれらをポップし、仕様構造格納器６のトップデータに記録された規則およびパラメータにしたがってプログラムを合成し、それを内部スタックに積む。このとき、仕様構造格納器６のトップデータもポップされる。もし仕様構造格納器６が空になっていれば最後に合成されたプログラムは当初入力された仕様に対応するものであり、プログラム出力器９に送られると同時に、新しいデータとしてプログラム登録器８にも送られる。
【００１１】
プログラム登録器８は送られたデータ（プログラムおよび仕様）を仕様つきプログラムの書式のＸＭＬ文書に変換して仕様つきプログラム格納器２に格納する。プログラム出力器９は入力されたＸＭＬ文書をターゲット言語用変換書式ＸＳＬＴにしたがって変換（レンダリング）し具体的なコードを生成する。
【００１２】
Ｈｏａｒｅ論理規則格納器５に格納される規則はＩＦ文の規則、ＷＨＩＬＥ文の規則、複合文の規則、代入文の規則、再帰手続きの規則、帰結規則とそれぞれ呼ばれるよく知られたもので、当該の言語要素をもつプログラミング言語に典型的である。
【００１３】
仕様分解器４はこれらの言語要素にしたがってその部分をとりだす。たとえば複合文の場合などのようには分割の方法は一般には一意ではないが、最初の部分プログラムの後条件は（前条件は与えられた仕様の前条件と同じ。）前条件と組にしてすでに蓄積されている場合に限る。また、再帰手続きの場合は、部分仕様に自分と同じものが見つかった場合にその箇所を再帰と仮定して探索を止める。
【００１４】
プログラム検索器３では検索キーおよび蓄積データの仕様の同一性として一般にはα同値をもちいるのが通例であるが、ＸＭＬによる木表現に変換する時に変数の標準化を行なうので実際にプログラム検索器３で行なう処理は木のラベルを含めた同値性のみである。
【００１５】
仕様構造格納器６は実際には仕様分解過程の履歴スタックとして機能する。すなわち分解の細部に行くにしたがってその記録がスタックの上部に積まれる。一度に積まれるデータ構造にはＨｏａｒｅ論理の規則、部分プログラムの個数（たとえば、複合文の規則であれば２）、そのほか分解結果を再構成して復元するのに必要な情報が格納されている。
【００１６】
プログラム合成器７は仕様構造格納器６のトップデータを参照することで、分解途中、次にプログラム探索器から送られる結果はどのルールで再構成処理すべきかを決定している。
【実施例２】
【００１７】
図２は合成に失敗した場合に人間が対話的に証明を入力する余地を残した実装を示したものである。探索に失敗した仕様は未解決仕様格納器１０に格納され、利用者グループに公開される。利用者の一人が証明を試み証明入力器１１に入力するとやはりＸＭＬの木に変換されて証明検査器１２に送られ、当該の仕様を満たすか否かが検査される。この検査は証明の各ステップがＨｏａｒｅ論理の推論規則通りであるか否かを検査することで行なわれる． 
【産業上の利用可能性】
【００１８】
ソフトウエア開発環境から本サービスを利用することで仕様に沿ったソフトウエア開発を支援することができる。
【図面の簡単な説明】
【００１９】
【図１】プログラムのデータベースの実施方法を示した構成図である。（実施例１）
【図２】プログラムのデータベースの実施方法を示した構成図である。（実施例２）
【符号の説明】
【００２０】
１    検索キー入力器
２    仕様つきプログラム格納器
３    プログラム検索器
４    仕様分解器
５    Ｈｏａｒｅ規則格納器
６    仕様構造格納器
７    プログラム合成器
８    プログラム登録器
９    プログラム出力器
１０    未解決仕様格納器
１１    証明入力器
１２    証明検査器
【図１】
2010238062.tif 000003
【図２】
2010238062.tif 000004