(57)【要約】      （修正有）【課題】  要求仕様を保証つきで満たし，修正／翻訳なしでそのまま利用可能なプログラムコードを，意味仕様そのものから容易に検索できるようなプログラム蓄積・利用方法を提供する。【解決手段】  意味仕様から所望のプログラムコードを検索すること可能にするためにプログラムにその形式的意味仕様を，またプログラムの正しさ（仕様充足性）を保証するために仕様を満たすことの検査可能な形式的証明を，プログラムに同時に蓄積する。仕様から所望のプログラムを検索するには該蓄積媒体を走査し要求仕様に合致する仕様と組になったプログラムを出力する。また利用度を高めるためにはプログラムを抽象コードとして蓄積し，利用時に各言語へ翻訳する機構を設ける。【選択図】図１
2006085206.tif 000002
【特許請求の範囲】
【請求項１】
プログラムコードを各部分の形式的意味仕様との組にして蓄積する方法と，該蓄積媒体を走査して所与の要求仕様を満たす仕様に該当するプログラムコードを検索結果として出力することで要求プログラムを得る方法を特徴とする蓄積・再利用方法．
【請求項２】
請求項１の蓄積方法における蓄積内容に加えて，プログラムの正しさ（仕様充足）の証明をも同時に蓄積することで信頼性のための情報を付与・蓄積する方法と，請求項１の検索結果に加えて出力プログラムの正しさの証明をも同時に出力することで出力プログラムの信頼性を保証する方法と，出力された証明の各ステップを確認することで出力プログラムが正しいことを検査する方法を特徴とするプログラム蓄積・再利用方法．
【請求項３】
請求項１と請求項２の各々に加えて出力プログラムをあらかじめ指定した記述言語に自動的に翻訳することで結果の利用度を向上させる方法を特徴とするプログラム蓄積・再利用方法．
【請求項４】
請求項１〜請求項３に加えてプログラムの形式的意味仕様において可変個数のデータの集まりを表すデータを集合論における集合に対応させる機構を設けることによって集合論だけによる要求仕様記述を可能にする方法．
【請求項５】
請求項１〜請求項４の利用方法をインターネットなど通信回線上のサービスとして提供することで遠隔分散利用を可能にしたプログラム蓄積・再利用方法．
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は，検索と利用が容易なプログラムのデータベースに関するものである．
【背景技術】
【０００２】
インターネットによってプログラム（コード）を共有することはネットワーク上でソフトウエアを共同作成したり，プログラム資産を再利用する場合に有効である．
【０００３】
しかし，WWWでソースコードを公開したとしても，通常利用されるキーワード検索では利用者が所望のプログラムを探し出すことが困難あり，運良くプログラムの候補が見出されたとしても期待する言語で記述されているとは限らず，さらに所望の仕様を満たすかどうか，あるいは（バグのない）正しく安全なプログラムかどうかは保証されていない．
【０００４】
形式的仕様による検索を可能にするプログラムのデータベースも提案されているが，得られるプログラムがその仕様を満たし正しいことは保証されない．このようなシステムは信頼できる組織内など限定された利用環境ではある程度有効であるものの，インターネットを通じた開放的な環境では得られるプログラムの品質や安全性が保証できず破綻する．
【非特許文献１】川北誠 酒井正彦 山本晋一郎 阿草清滋「形式的仕様を用いた再利用モデル」情報処理学会論文誌vol.36 No.05, ２００２年
【０００５】
特定のプログラミング言語により記述されたプログラムをそのまま蓄積・利用するデータベースシステムは提案されているが，要求するものと記述言語が異なる場合，あらためて翻訳する必要が生じ利用度が低下する．
【非特許文献２】武田智弘,土居範久, 磯田定宏 「C++のためのプログラムベース」情報処理学会ソフトウェア再利用技術シンポジウム論文集 １９９２年
【発明の開示】
【発明が解決しようとする課題】
【０００６】
解決しようとする課題は，所望のプログラムをその意味によって検索することが可能であり，得られるプログラムが仕様を満たしかつ正しいことが保証でき，また言語によらず直ちに利用できるようなプログラム資産蓄積・利用方法である．
【課題を解決するための手段】
【０００７】
本発明は，意味仕様から所望のプログラムコードを検索することを可能にするための形式的意味仕様と，プログラムの正しさ（仕様充足性）を保証するための仕様充足証明を添付するプログラム蓄積方法と，利用度を高めるためにプログラムを抽象コードとして蓄積して利用時に各言語へ翻訳する機構を主な特徴とする．
【発明の効果】
【０００８】
本発明のプログラムベースの利用者は所望のプログラムを意味仕様から容易に検索でき，正しさが保証された安全なプログラムを得ることができる．さらに，あらかじめ記述言語を指定しておくことにより，利用者が作成中のプログラムの一部として検索結果をそのまま利用することができる．
【発明を実施するための最良の形態】
【０００９】
インターネット上でプログラムベースを遠隔共有利用する場合を想定し，プログラムベースサーバー（リモート）にプログラムを蓄積し，証明にもとづく検査器を利用者側（ローカル）に配置することにより安全性を実現した．仕様記述言語としては標準的にもちいられる形式的集合論にもとづくものが望ましい．
【実施例】
【００１０】
図１は、本発明の１実施例の概念図である．本実施例はプログラムを蓄積する媒体および検索処理などをおこなうデータ管理システムと，利用者側にあって利用者の要求を発信し得られた結果を提示するためのクライアントアプリケーションと，データ管理システムとクライアントのなかだちをするサービスを提供するサーバからなる．
【００１１】
蓄積データのエントリはHoare論理の証明の形で蓄積される．これはプログラムと仕様の情報を含む．ここで証明の部分証明もまたエントリとなることに注意せよ．これにより部分的なコード資産が利用可能になる．
【００１２】
本実装ではプログラムコードとして帰納的定義付きの型理論，仕様記述言語として該型理論のリスト型データを集合として含む集合論を用いている．リスト型に関する集合の公理は数１にあげた．
【非特許文献３】萩谷昌巳 「帰納的定義つき型理論における簡約と射影について」情報処理学会論文誌，９１巻，１９号
【００１３】
【数１】
2006085206.tif 000003
【００１４】
Hoare論理の言明はプログラムPと仕様Aの組でありプログラムPが仕様Aを満たすことを意味し，P{A}のようにあらわす．数２はHoare論理の証明の１ステップの一般形であって，P1{A1},...,Pn{An} が成り立つとき，Q{B}が成り立つことを表す．
【００１５】
【数２】
2006085206.tif 000004
【００１６】
図２は本実装例で用いる証明のための体系（検証系）に用いる推論規則である．この検証系による証明をデータエントリとして蓄積し，またクライアントアプリケーションはサーバーから検索結果として取得した証明をこの規則にしたがって検査する．推論規則においてin, out, value はそれぞれプログラムの入力，出力，値を表す変数である．εは（何もしない）空のプログラムを表す．自然数型Nを含むそのほかプログラムの記述言語の記法は萩谷の非特許文献３にならう．
【００１７】
利用者がたとえば集合の最大値を返すＪａｖａ（登録商標）プログラムを所望したとしよう．利用者は仕様として数３のような要求仕様をクライアントアプリケーションに投入する．クライアントアプリケーションはこれを検索キーとしてサーバに送り，サーバはこれを受けとり蓄積データ管理システムに渡す．蓄積データ管理システムでは集合SetをListやVectorなどデータの集まりとなりうるデータ型に変換して数４のような仕様に書き換えて検索を行ない，該当する仕様をもつプログラムの証明が見つかればそれを返し，なければエラーを返す．クライアントアプリケーションはこの結果を受けとり，図２の推論規則にてらして検査する．検査を通過した証明からプログラムの部分だけをとりだして，対象言語に翻訳し．対象言語が関数名を要求する場合は対話的に利用者に問い合わせることで最終的に所望のプログラム（数５）を得る．
【００１８】
【数３】
2006085206.tif 000005
【００１９】
【数４】
2006085206.tif 000006
【００２０】
【数５】
2006085206.tif 000007
【００２１】
なおWWWにおける利用を前提とした実装では蓄積に際してXMLやSemistructured Dataをもちいることでプログラムないしは証明の木構造を簡便に表現・蓄積し転送することができる．
【産業上の利用可能性】
【００２２】
本発明は，ソフトウエア再利用を支援する機構としてソフトウエア生産性向上に寄与する．また，その安全性保証の機構により，インターネット上の不特定多数のプログラムベースサーバで提供されるプログラム達を複数の利用者が安全に利用することができるので教育用または開発用サービスとしての商用利用が期待できる．
【図面の簡単な説明】
【００２３】
【図１】本発明のプログラムベースの実施例の概念図である．（実施例）
【図２】検証系で用いるの推論規則である．（実施例）
【符号の説明】
【００２４】
１    プログラム蓄積媒体およびデータ管理システム
２    サーバー（要求処理）
３    クライアント（利用者側アプリケーション）
【図１】
2006085206.tif 000008
【図２】
2006085206.tif 000009