(57)【要約】【課題】  プログラムの所望の振る舞いを定義した形式仕様および進化的アルゴリズムを用いて、プログラムを仕様に合った、即ち正当性証明可能なプログラムに進化させる方法およびシステムを提供する。【解決手段】  正当性証明可能なコンピュータプログラムは、遺伝的プログラミング技術を用いて生成する。所望のプログラム振る舞いを用いて形式仕様を定義する。プログラムの初期集団を作成し、各プログラムに形式化技術を用いて定義されうる意味を備える。適合度関数を適用してプログラムの意味、すなわち実際の振る舞いと仕様との間の距離を求める。プログラムの意味と仕様との間の距離の値がゼロのプログラムが定められ、正当性証明可能なプログラムとなる。現在のプログラム世代のうちいくつか、またはすべてのプログラムの適合度を計算した後、現在の世代に正当性証明可能なプログラムが見つからない場合、現在の世代におけるもっとも適合度の高い個別のプログラムの少なくとも一部に突然変異および／または交差技法が実施され、次のプログラム世代を作成する。【選択図】  図１
2005182806.tif 000002
【特許請求の範囲】
【請求項１】
遺伝的プログラミング技術を用いてコンピュータプログラムを生成する方法であって、
プログラムの所望の振る舞いを定義する仕様を提供し、
各プログラムが実際の振る舞いを有する、プログラムの現在の個体群を作成し、
現在の個体群における各プログラムについて、プログラムがいかに仕様を満たしているか計算する適合度関数を使用してプログラムの適合度を計算する
ことを含む方法。
【請求項２】
前記各プログラムの適合度の計算が、プログラムの実際の振る舞いと仕様との間の距離の大きさを判定する、請求項１に記載の方法。
【請求項３】
前記適合度の計算が、更に、適合度関数により許容値内の距離が得られたとき、そのプログラムが仕様を満たしていると判定する、請求項２に記載の方法。
【請求項４】
前記適合度の計算が、更に、適合度関数により距離ゼロが得られたとき、そのプログラムが仕様を満たしていると判定する、請求項２に記載の方法。
【請求項５】
個体群におけるすべてのプログラムの適合度が十分に仕様を満たしていないと分析された場合、プログラムの個体群において選択した少なくとも一つのプログラムに突然変異操作と交差操作の少なくとも一つを行うことによって、プログラムの新たな個体群を作成することを更に含む、請求項１に記載の方法。
【請求項６】
各プログラムを表示的意味論技術を用いて分析し、そのプログラムの実際の振る舞いを形式化することを更に含む、請求項１に記載の方法。
【請求項７】
遺伝的プログラミング技術を用いてプログラミングコードを生成するシステムであって、
少なくとも一つの所望のプログラム振る舞いを定義する仕様を受け取る仕様受信回路、ルーチンまたはアプリケーションと、
各プログラムが実際の振る舞いを有する、コンピュータプログラムの一個体群を生成する現在プログラム個体群生成回路、ルーチンまたはアプリケーションと、
受信した仕様および定義した適合度関数に基づいて、仕様を満たしているかという点についてプログラムの適合度を判定する適合度判定回路、ルーチンまたはアプリケーションと、
を備えるシステム。
【請求項８】
前記適合度判定回路、ルーチンまたはアプリケーションが、プログラムの実際の振る舞いと仕様との間の距離の大きさを判定するために、プログラムに適合度関数を適用する、請求項７に記載のシステム。
【請求項９】
前記適合度判定回路、ルーチンまたはアプリケーションが、プログラムが許容値内の距離値を有するとき、そのプログラムが仕様を満たすと判定する、請求項８に記載のシステム。
【請求項１０】
前記適合度判定回路、ルーチンまたはアプリケーションが、プログラムが距離値ゼロを有するとき、そのプログラムは仕様を満たしていると判定する、請求項８に記載のシステム。
【請求項１１】
現在の個体群におけるすべてのプログラムの適合度がどのプログラムも仕様を十分に満たしていないと分析された場合、プログラムの現在の個体群において選択した少なくとも一つのプログラムに突然変異操作と交差操作の少なくとも一つを行うことによって、プログラムの新たな個体群を作成する、新個体群生成回路、ルーチンまたはアプリケーションを更に備える、請求項７に記載のシステム。
【請求項１２】
前記適合度判定回路、ルーチンまたはアプリケーションが、表示的意味論技術を用いて各プログラムの実際の振る舞いを形式化する、請求項７に記載のシステム。
【請求項１３】
前記適合度判定回路、ルーチンまたはアプリケーションが、テストケースを利用して、プログラムが一つまたは複数のテストケースを満たすことができるか否か判定することによってプログラムの適合度を判定する、請求項８に記載のシステム。
【請求項１４】
データ処理装置で実行可能であり、前記データ処理装置に遺伝的プログラミング技術を用いてコンピュータプログラムを生成させる処理を実行させる一組の命令が含まれる、コンピュータにより読み取り可能なプログラムであって、前記命令が、
プログラムの所望の振る舞いの仕様を受信する命令と、
各プログラムが意味を有する、コンピュータプログラムの現在の個体群を作成する命令と、
適合度関数を適用して、仕様を満たすという点においてプログラムの適合度を分析する命令と、
を含むプログラム。
【請求項１５】
前記適合度関数を適用して、仕様を満たすという点においてプログラムの適合度を分析する命令が、適合度関数を適用してプログラムの実際の振る舞いと仕様との間の距離値の大きさを判定する命令を含む、請求項１４に記載のプログラム。
【請求項１６】
適合度関数により求めた距離値が許容値内のときそのプログラムが仕様を満たすと判定する命令を更に含む、コンピュータによる読み取り可能な、請求項１５に記載のプログラム。
【請求項１７】
適合度関数により求めた距離値がゼロであるときそのプログラムが仕様を満たすと判定する命令を含む、請求項１５に記載のプログラム。
【請求項１８】
現在の個体群におけるすべてのプログラムが適合度において十分に仕様を満たしているプログラムがないと分析された場合、プログラムの現在の個体群において選択した少なくとも一つのプログラムに突然変異操作と交差操作の少なくとも一つを行うことによって、プログラムの新たな個体群を作成する命令を更に含む、請求項１４に記載のプログラム。
【請求項１９】
表示的意味論技術を用いて、プログラムの実際の振る舞いを形式化する命令を更に含む、請求項１４に記載のプログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、進化的アルゴリズムを使用して、正当性証明可能なコードを生成するための方法およびシステムに関する。
【背景技術】
【０００２】
進化的アルゴリズムは、より小さいプログラムのランダムな個体群（population）からコンピュータプログラムを作成し、進化させるための、遺伝学技術の応用である。進化的アルゴリズムの一つの目的は、時間を費やして人間がプログラムコードを生成することなく、自動的にコンピュータプログラムを生成することにある。
【０００３】
進化的技術は、染色体に類似したランダムなプログラムの初期集団（initial population）を生成することから始まる。この初期集団は、遺伝的操作を通じて新たな集団（新たな世代）即ち個体群に繰り返し進化していき、その進化はプログラムが進化してテストケースで正しい解を戻すまで行われる。プログラムは個別にテスト用に個体群から選択される。個体群から選択された個別プログラムの適合度が、一つまたは複数のテストケースでプログラムを実行させることにより判定される。個別のプログラムの、テストケースを正確に実行する能力を計ることで、個体群から最も適合度の高い個体を選択することができる。次いで、個体が選択され、突然変異操作および交差操作がされて、次世代の別のプログラム個体群を形成する。適合度のより高い個別のプログラムが、より高い確率で選択される。このプロセスは、個体群が、すべてのテストケースあるいは十分な数のテストケースをパスする個体を少なくとも一つ有するまで繰り返される。
【０００４】
このような進化的または遺伝的アルゴリズムをコンピュータ等に実装して用いた技術として、特許文献１には、非線型遺伝的アルゴリズムを使用して、コンピュータシステムにおいて複数の機能を最適に構成する等の問題解決を行う技術が開示されている。また、特許文献２には、遺伝的プログラミングを使用して電子回路等の複雑な構造の最適な設計を自動的に行う技術が開示されている。
進化的アルゴリズムは、いくつかの分野、特に、テストを通じて個別のプログラムの適合度を容易に数値化できる分野で成功することが証明されている。しかしながら、手書きのコードのように、個別プログラムそれぞれの適合度がテストで評価されるからといって、その選択したプログラムがテストの適用範囲（domain）外でうまく働くという保証はない。進化したプログラムには元来オーバーフィット（over-fitting）してしまう傾向があるため、進化的アルゴリズムでは適合度の制約が、人間が生成したコードに比べてより厳しいものとなりうる。したがって、遺伝的プログラミング技術の実用化は、テストでプログラムが単体で完全に正当性を立証できる適用範囲に大きく限られている。
【特許文献１】米国特許第５１３６６８６号公報
【特許文献２】米国特許第５８６７３９７号公報
【発明の開示】
【発明が解決しようとする課題】
【０００５】
本発明は、プログラムの所望の振る舞いの形式仕様を用いて、プログラムをその仕様に合ったプログラムに進化させる方法およびシステムを提供する。
【０００６】
本発明は、所定の仕様に対して個別のプログラムの適合度を測定するのに使用できる適合度関数を作成するシステムおよび方法を別途提供する。
【０００７】
本発明は、進化的アルゴリズムを使用して、プログラムコードを、テストの域を超えて、正当性を立証可能なプログラムコードに進化させるシステムおよび方法を別途提供する。
【課題を解決するための手段】
【０００８】
上記課題を解決するために、請求項１に記載の発明は、遺伝的プログラミング技術を用いてコンピュータプログラムを生成する方法であって、プログラムの所望の振る舞いを定義する仕様を提供し、各プログラムが実際の振る舞いを有する、プログラムの現在の個体群を作成し、現在の個体群における各プログラムについて、プログラムがいかに仕様を満たしているか計算する適合度関数を使用してプログラムの適合度を計算することを含むことを特徴とする。
【０００９】
請求項２に記載したように、前記各プログラムの適合度の計算は、プログラムの実際の振る舞いと仕様との間の距離の大きさを判定することを特徴とする。
【００１０】
請求項３に記載したように、前記適合度の計算は、更に、適合度関数により許容値内の距離が得られたとき、そのプログラムが仕様を満たしていると判定することを特徴とする。
【００１１】
請求項４に記載したように、前記適合度の計算は、更に、適合度関数により距離ゼロが得られたとき、そのプログラムが仕様を満たしていると判定することを特徴とする。
【００１２】
請求項５に記載したように、本発明は、個体群におけるすべてのプログラムの適合度が十分に仕様を満たしていないと分析された場合、プログラムの個体群において選択した少なくとも一つのプログラムに突然変異操作と交差操作の少なくとも一つを行うことによって、プログラムの新たな個体群を作成することを更に含むことを特徴とする。
【００１３】
請求項６に記載したように、本発明は、各プログラムを表示的意味論技術を用いて分析し、そのプログラムの実際の振る舞いを形式化することを更に含む、請求項１に記載の方法。
【００１４】
また、請求項７に記載の発明は、遺伝的プログラミング技術を用いてプログラミングコードを生成するシステムであって、少なくとも一つの所望のプログラム振る舞いを定義する仕様を受け取る仕様受信回路、ルーチンまたはアプリケーション、即ち仕様受信手段と、各プログラムが実際の振る舞いを有する、コンピュータプログラムの一個体群を生成する現在プログラム個体群生成回路、ルーチンまたはアプリケーション、即ち現在プログラム個体群生成手段と、受信した仕様および定義した適合度関数に基づいて、仕様を満たしているかという点についてプログラムの適合度を判定する適合度判定回路、ルーチンまたはアプリケーション、即ち適合度判定手段と、を備えることを特徴とする。
【００１５】
請求項８に記載したように、前記適合度判定回路、ルーチンまたはアプリケーション、即ち適合度判定手段は、プログラムの実際の振る舞いと仕様との間の距離の大きさを判定するために、プログラムに適合度関数を適用することを特徴とする。
【００１６】
請求項９に記載したように、前記適合度判定回路、ルーチンまたはアプリケーション、即ち適合度判定手段は、プログラムが許容値内の距離値を有するとき、そのプログラムが仕様を満たすと判定することを特徴とする。
【００１７】
請求項１０に記載したように、前記適合度判定回路、ルーチンまたはアプリケーション、即ち適合度判定手段は、プログラムが距離値ゼロを有するとき、そのプログラムは仕様を満たしていると判定することを特徴とする。
【００１８】
請求項１１に記載したように、本発明は、現在の個体群におけるすべてのプログラムの適合度がどのプログラムも仕様を十分に満たしていないと分析された場合、プログラムの現在の個体群において選択した少なくとも一つのプログラムに突然変異操作と交差操作の少なくとも一つを行うことによって、プログラムの新たな個体群を作成する、新個体群生成回路、ルーチンまたはアプリケーション、即ち新個体群生成手段、を更に備えることを特徴とする。
【００１９】
請求項１２に記載したように、前記適合度判定回路、ルーチンまたはアプリケーション、即ち適合度判定手段は、表示的意味論技術を用いて各プログラムの実際の振る舞いを形式化することを特徴とする。
【００２０】
請求項１３に記載したように、前記適合度判定回路、ルーチンまたはアプリケーション、即ち適合度判定手段は、テストケースを利用して、プログラムが一つまたは複数のテストケースを満たすことができるか否か判定することによってプログラムの適合度を判定することを特徴とする。
【００２１】
また、請求項１４に記載の発明は、データ処理装置で実行可能であり、前記データ処理装置に遺伝的プログラミング技術を用いてコンピュータプログラムを生成させる処理を実行させる一組の命令が含まれる、コンピュータにより読み取り可能なプログラムであって、前記命令が、プログラムの所望の振る舞いの仕様を受信する命令と、各プログラムが意味を有する、コンピュータプログラムの現在の個体群を作成する命令と、適合度関数を適用して、仕様を満たすという点においてプログラムの適合度を分析する命令と、を含むことを特徴とする。
【００２２】
請求項１５に記載したように、前記適合度関数を適用して、仕様を満たすという点においてプログラムの適合度を分析する命令は、適合度関数を適用してプログラムの実際の振る舞いと仕様との間の距離値の大きさを判定する命令を含むことを特徴とする。
【００２３】
請求項１６に記載したように、本発明は、適合度関数により求めた距離値が許容値内のときそのプログラムが仕様を満たすと判定する命令を更に含むことを特徴とする。
【００２４】
請求項１７に記載したように、本発明は、適合度関数により求めた距離値がゼロであるときそのプログラムが仕様を満たすと判定する命令を含むことを特徴とする。
【００２５】
請求項１８に記載したように、本発明は、現在の個体群におけるすべてのプログラムが適合度において十分に仕様を満たしているプログラムがないと分析された場合、プログラムの現在の個体群において選択した少なくとも一つのプログラムに突然変異操作と交差操作の少なくとも一つを行うことによって、プログラムの新たな個体群を作成する命令を更に含むことを特徴とする。
【００２６】
請求項１９に記載したように、本発明は、表示的意味論技術を用いて、プログラムの実際の振る舞いを形式化する命令を更に含むことを特徴とする。
【００２７】
本発明によるシステムおよび方法の様々な実施形態において、適合度関数を用いてプログラムそれぞれの適合度を求める。個別プログラムの適合度は、適合度関数で求められる、個別プログラムの実際の振る舞いと所望の振る舞いの間の距離で表わされる。様々な実施形態において、実際の振る舞いが所望の振る舞いに等しいことが証明できる場合、この適合度関数の値はゼロになる。これは、プログラムが、たとえ異なる入力が無限にあったとしても、すべての起こりうる入力あるいはテストケースについて要求されたように振舞うことを意味する。
【００２８】
本発明によるシステムおよび方法の様々な実施形態において、所定の仕様を満たすようにプログラムを進化させるために、プログラムの初期集団（個体群）が作成される。様々な実施形態において、個別のプログラムはランダムプログラムあるいは準ランダムプログラムを含むことができる。個体群における各プログラムの適合度を、適合度関数を使用して各プログラムの意味あるいは振る舞いと所定の仕様との間の距離（distance）を計算することで判定する。距離の値が小さいプログラムほど適合度が高くなる。適合度を計算している間のどの時点であっても、適合度がゼロ、つまり距離がゼロであるプログラムが個体群において見つかれば、進化を止めて、関数はそのプログラムを返す。別の方法では、適合度の計算を個体群における各プログラムに対して実行し、その結果を順位付けする。順位付けによって判定された、現在の世代のより適合度の高いプログラムの一つまたは複数に対し、突然変異操作および／または交差操作の組み合わせを繰り返し実施することによって、新たな個体群のプログラムを作成する。新たな個体群が作成されると、それぞれの適合度を再度評価して、距離がゼロとなるプログラムに進化するまでこのプロセスが繰り返される。
【００２９】
様々な実施形態において、本発明によるシステムおよび方法を、プログラムの実際の振る舞いと所望の振る舞いとの間の距離による適合度関数を用いるプログラムテストと、そのプログラムテストの結果に基づく従来の適合度関数と組み合わせて使用することができる。
【００３０】
本発明によるシステムおよび方法の様々な実施形態の、これらおよび他の特長および利点は、本発明によるシステムおよび方法の様々な実施形態についての、以下の記載から明らかになろう。
【発明の効果】
【００３１】
本発明により、プログラムの所望の振る舞いを定義した形式仕様および進化的アルゴリズムを用いてプログラムを進化させることにより、正当性証明可能なプログラムを得ることができる。
【発明を実施するための最良の形態】
【００３２】
本発明によるシステムおよび方法の様々な実施形態を、添付の図面を参照して詳細に説明する。
【００３３】
図１は、本発明による遺伝的プログラミング技術を使用して、正当性証明可能なコードを生成する方法の一実施形態を概説するためのフローチャートである。図１に示すように、本方法の操作は、ステップＳ１００から始まり、ステップＳ２００に進み、そこで形式仕様を定義する。様々な実施形態では、形式仕様が、進化したプログラムによって解決すべき問題を明記する。様々な実施形態では、仕様が数式で表されている。他の様々な実施形態では、仕様がより抽象的な表現で表されたり、または複雑なシステムの振る舞いを指定したりすることもある。次に、ステップＳ３００において、プログラムの初期集団を現在のプログラム世代として作成する。次いで、ステップＳ４００において、現在のプログラム世代における個々のプログラムを現在のプログラムとして、適合度を評価するために選択する。次いで、ステップＳ５００の操作に移る。
【００３４】
ステップＳ５００では、現在のプログラムを分析して、現在のプログラムの振る舞いと、定義された仕様に基づく所望の振る舞いとの間の距離を求める。次いで、ステップＳ６００において、現在のプログラムの距離が所望の値以下かどうか判定する。所望の値以下である場合、操作はステップＳ１１００へ飛ぶ。所望の値以下でない場合、操作はステップＳ７００へ移行し、そこで現在のプログラム世代の個体すべてについて適合度を計算したかどうか判定する。すべてについて計算していない場合、処理はステップＳ４００へ戻る。すべてについて計算した場合、ステップＳ８００へ進む。
【００３５】
ステップＳ８００において、現在のプログラム世代から所定数のプログラム、好ましくは、距離の値が小さいプログラムをリストより選択する。様々な実施形態において、これらのプログラムはリストよりランダムに選択される。次いで、ステップＳ９００において、現在のプログラム世代から選択したプログラムに対し突然変異および／または交差操作を行い、次のプログラム世代を作成する。次に、ステップＳ１０００において、次プログラム世代が新たな現在のプログラム世代として現在のプログラム世代に置き換えられる。次いで、操作は再びステップＳ４００に戻る。一方、ステップＳ１１００では、距離がゼロのプログラムを、定義した仕様を満たすプログラムとして特定する。次いで、操作はステップＳ１２００へ続き、そこで本発明による方法の操作は終了する。
【００３６】
様々な実施形態において、ステップＳ３００で生成されたプログラムは人間が作成したコードである。他の様々な実施形態においては、これらのプログラムはコンピュータによって生成されるコードである。初期集団の各プログラムは単一の機能を実行するか、あるいは一つまたは複数のプログラムが多数の機能を実行することもできる。プログラムを作成する分野においては多くの技術が知られている。本発明によるシステムおよび方法は、プログラムの初期集団を生成するために、いかなる周知の技術あるいはこれから発展する技術を利用することもできる。さらに、本発明によるシステムおよび方法を、いかなる周知のあるいはこれから発展するプログラミング言語および／または設計言語で書かれたプログラムを進化させる際にも利用することができることを理解されたい。たとえば、Ｃ、Ｃ＋＋、Ｆｏｒｔｒａｎ、ＬＩＳＰなどの一般に使用されているプログラミング言語、または有限オートマトン、正規表現あるいはプロセスの記述に使用されるより抽象的な設計言語を、そのプログラミングあるいは設計言語に意味（semantics）の形式的定義がある限り、本発明によるシステムおよび方法に使用することもできる。
【００３７】
様々な実施形態において、プログラム個体の適合度を、プログラムの意味、すなわちプログラムの実際の振る舞いと、仕様で定義された所望のプログラムの振る舞いとの差異で定量化する。様々な実施形態において、適合度は適合度アルゴリズムに基づいて判定される。適合度アルゴリズムは、プログラムの実際の振る舞いが規定の振る舞いといかに異なるかを測定する距離関数を定める。このアルゴリズムは、プログラムがすべてのケースにおいて仕様を満たす場合にのみ距離ゼロを戻す。
【００３８】
様々な実施形態において、ステップＳ６００で使用した所定の閾値はゼロである。他の実施形態では、距離がゼロの許容値内であれば十分であることも多い。
【００３９】
図２は、プログラム個体の実際の振る舞いと仕様の所望の振る舞いとの間の距離を判定するための方法の一実施形態をより詳細に説明するためのフローチャートである。図２に示すように、操作はステップＳ５００から始まり、ステップＳ５１０へ進み、そこで、現在のプログラムを分析してプログラムの意味、すなわちプログラムの実際の振る舞いを判定する。次いで、ステップＳ５２０において、意味、すなわち実際の振る舞いと、仕様で定義された所望の振る舞いとの間の距離を測定する。様々な実施形態において、適合度関数によってプログラムの意味と、プログラムの所望の振る舞いの形式仕様との差異を、距離を単位として定量化する。次いで、ステップＳ５３０において、判定された距離値を現在のプログラムに関連付けし、次にステップＳ５４０で、処理はステップＳ６００に戻る。
【００４０】
一般に、プログラムの振る舞いが同じであることを判定するのは難しい。したがって、様々な実施形態において、プログラムが完全に仕様を満たしている場合、その場合にのみ距離値ゼロを戻す適合度アルゴリズムを実行することは、仕様が非常に限定的である場合を除いて、不可能であろう。したがって、本発明によるシステムおよび方法の様々な実施形態において、必ずしもすべてではなくいくつかの仕様を十分に満たすプログラムについて距離の値がゼロであるとして、距離の値を決定すれば十分であろう。さらに、様々な実施形態において、プログラムの実際の振る舞いが所望の振る舞いに等しい場合の距離の値をゼロとする限り、おおよその距離値を求めることも可能である。
【００４１】
本発明によるシステムおよび方法の様々な実施形態において、プログラムの意味と形式仕様の間の距離を使用するのにいくつか有用なものがある。まず、操作するのに適当なプログラミングあるいは設計言語を選択することが有用である。プログラミング言語はＣ、Ｃ＋＋、Ｆｏｒｔｒａｎあるいは他の適当な言語等の一般に使用されているプログラミング言語のいずれでもよく、あるいは有限オートマトン、正規表現あるいはプロセス（プロセス代数、ＣＨＳＭ、ＣＣＳ、ＣＳＰを含む）の記述に使用されるより抽象的な設計言語を使用することも可能である。プログラミング言語あるいは設計言語は明確に定義され、その意味（semantics）に形式的定義を持つものとする。次に、プログラムの所望の振る舞いの形式仕様を提供することとする。この形式仕様は、進化したプログラムの所望の振る舞いを定義するものである。最後に、距離関数を定めるのに使用することができる適合度アルゴリズムを作成する。距離関数は、プログラムの実際の振る舞いと仕様に規定された振る舞いとの差を適切な精度で測定できるものである。様々な実施形態において、このアルゴリズムは、プログラムがあらゆる点で仕様を満たす場合に限り距離値ゼロを戻す。
【００４２】
個別のプログラムの適合度を判定するために本発明によるシステムおよび方法の様々な実施形態で使用できる技術が、少なくとも三つある。モデル検査技術（model checking）においては、時相論理式（temporal logic formulas）を通じて仕様を提示する。形式分析技術（formal analysis）は、所定のプログラムを減じて有限状態表現とするものである。その仕様が減じた表現のすべての状態に当てはまるとすると、所定のプログラムはその仕様を満たしていることとなる。適合度測定はモデルチェッカーが発見した反例の数を数える、あるいはその近似値を求めることによって定義することができる。
【００４３】
公理的意味論技術（axiomatic semantics）においては、意図する振る舞いの仕様を、プログラムテキストの様々な箇所を注釈する、事前条件（pre-condition）、事後条件（post-condition）および不変条件（invariant condition）と呼ばれる論理式で表現する。検証条件と呼ばれる一組の論理式を効率よく生成して、すべての検証条件が真であると証明できれば、その仕様に関してプログラムが正確であるとするものである。公理的意味論技術に基づく距離の測定では、特定の検証条件がいかに真から離れているか判定することが必要であろう。ここで注意したいのは、論理式は含意について順序付けすることができることである。したがって、様々な実施形態において、かかる公理的意味論技術で式に数値を割り当てて、数値の順序を含意順序とおおよそ一致させることとする。
【００４４】
表示的意味論技術（denotational semantics）も距離の測定に使用することができる。表示的意味論技術では、コンピュータプログラムの意味を形式化（formalize）する。表示的意味論技術では一般に、コンピュータ言語、アーキテクチャおよびプログラムを記述するために関数型プログラミングの技術を利用する。表示的意味論技術では、プログラムを関数に変換し、プログラムの特性を関数の標準的な数学理論、とくにドメイン理論を使用して証明することができる。この技術において、プログラムの意味は、適切な数学的構造の要素を各個別のプログラム要素に割り当てるマッピングによって定義される。この技術において、仕様は単なる、この構造の一特定要素の記述にすぎない。意味が特定の要素の意味に等しいならば、その個別のプログラムは仕様に対して正しいとする。もう一つの方法として、仕様を一組の可能なあるいは正当な表示（denotation）として定義することができる。この場合、プログラムの意味がその組の表示の一つに等しい場合、その仕様に対してそのプログラムは正しいとする。プログラムと仕様との間の距離は、基礎となる数学的構造においてプログラムの意味と仕様の間の距離の近似値を求めることによって定めることができる。これは表示が距離空間を形成するときに可能である。
【００４５】
本発明によるシステムおよび方法の応用の一実施形態において、正当性証明可能なコンピュータコードを生成するために表示的意味論技術を使用する。この実施形態に使用されるプログラミング言語には、数学演算子である、加算（＋）、減算（−）および乗算（・）と変数ｘと定数１からなるバイナリ式が含まれる。個別のプログラムの評価結果を単に所定式の値とし、その式においてｘがプログラムの入力を表す。この言語における個別プログラムの意味はｘの多項式となる。そのプログラムを実行すると所定値のｘについて多項式の値が戻される。そのプログラムの意味のモデル化に適した定義域（ドメイン）は、整数係数の一組の有限非有界タプル（finite unbound tuples）である。たとえば、タプル（１，０，１，３）において、各整数はｘの累乗の係数であり、タプルの一番左のｘ0から開始して、そこから右へ一つずつ加算してそれぞれｘ1、ｘ2、ｘ3の係数を表し、そのタプルがプログラム［（ｘ＋ｘ＋ｘ＋１）・ｘ・ｘ＋１］つまり［（３ｘ＋１）・ｘ2＋１］の意味となる。しかしながら、これと同じ意味を有するプログラムが他にも無限にある。このドメインにおいて、ユークリッド距離は、二つの同じプログラムの意味が距離０となる性質の距離（metric）である。その仕様は整数のタプルで表現することができる。個別のプログラムの意味論は、式を表示にマッピングすることによって定義することができる。本実施形態において、この例に好適な関数Ｓは以下の通りである。
【００４６】
2005182806.tif 000003
式中、＋および−はタプル毎にかかる要素（componentwise）として定義し、・による二つのタプルの積を以下のように定義する。
【００４７】
2005182806.tif 000004
言語、意味論的定義Ｓおよびタプルのユークリッド距離に基づいて、個体群の大きさを１０００としていくつかの異なる仕様のプログラムを生成した。エリート保存を用いて、確実に、一世代における最良のプログラム個体を次の世代に複製した。初期プログラムの最大値を１０個の記号として初期プログラムをランダムに生成した。５パーセントの率で突然変異を行い、ランダムに選択した部分木を新たなランダム木に置き換え、またはランダムな部分木を突然変異の結果として選択した。交差を用いて、二つの親プログラムからなるランダムな部分木を交換した。突然変異の候補と交差の親についてはトーナメントサイズ７として、トーナメント選択により選択した。表１に仕様、正当性証明可能なプログラムが見つかったときの世代番号、および正当性証明可能なプログラムそのものを示す。
【００４８】
【表１】
2005182806.tif 000005
この例における「正しさ（正当性）」は、単に仕様によって定められたとおりの正確な多項式を式が計算することを意味する。「正しさ」は式の大きさや計算の効率などの他のことに関わらない。式の大きさを考慮するために、たとえば、適合度関数を変更して、単にプログラムの意味と仕様との間の距離を得るのではなく、その距離とプログラムの大きさ、たとえば、式における演算子の数を共に「正確さ」の判定に使用することができる。適合度の値の順番付けは、辞書編集式であり、意味的な距離がより重要となる。表１には、三つの仕様と、正確なプログラムが見つかった世代と、正確なプログラムそのものが挙げられている。表１では、各仕様が、定義したｘの累乗の係数を表しており、左からｘ0で始まり、１ずつ増えている。
【００４９】
本発明によるシステムおよび方法の一応用である第二の実施形態は、通信ソフトウェアを合成するものである。この実施形態において、交互ビットプロトコル（alternating bit protocol）の送信プロセスを実行するプログラムを開発した。この実施形態において、プロセス代数のＣＣＳ（Calculus of Communicating Systems）を、プログラミング言語と仕様言語の両方に用いた。この実施形態において、プロセス代数言語の表示的意味論技術を距離空間として用いている。この空間における距離を適合度関数として用いる。言語の構文がプロセス代数である。プロセス代数ＣＣＳを用いて内部および外部通信動作を行うプロセスを記述する。プロセス代数ＣＣＳは、二方向通信の正確なモデリングを可能にするプロセスの並列実行の動作をサポートする。プロセス代数ＣＣＳはまた、抽象化、すなわち観測可能な動作を隠蔽して観測不可能な内部動作とすることをサポートしている。抽象化は、出力ほど細部が重要でない内部操作を実行する「ブラックボックス」をモデリングするのに有用である。
【００５０】
図３は、通信システムの要素の一実施形態を示す図であり、本発明によるシステムおよび方法の様々な実施形態を用いて生成した通信ソフトウェアプログラム３００の進化部分３２０で使用される仕様３６０を定義する。図３に示すように、通信システム３００には、プロセス３２０が含まれ、プロセス３２０は、環境３３０と対話して、仕様３６０と同等に振る舞う。図３はまた、抽象化や並列実行の機構の一実施形態を示している。図３に示すように、双方向多損失（lossy）通信チャネル３４０を、並列に動作する二つの一方向チャネル３４２および３４４で構成する。また、受信プロセス３５０が双方向多損失通信チャネル３４０と同時に動作する。双方向多損失通信チャネル３４０と受信プロセス３５０は共に、環境３３０の少なくとも一部分をなす新たなプロセスを形成する。双方向多損失通信チャネル３４０と受信プロセス３５０の間のローカルな通信動作は隠蔽されており、環境３３０の外のいかなるプロセスにもアクセスすることができない。
【００５１】
プロセス３２０が環境３３０と並列に構成されるとき、本発明によるシステムおよび方法の様々な実施形態を使用してプロセス３２０を進化させて、このプロセス３２０と環境３３０の間の通信動作を隠蔽した後に、このプロセス３２０が仕様３６０で特定される損失のない可逆性通信を提供するようにする。仕様３６０は単に、入力メッセージのシーケンスが、推定される遅延時間後に出力メッセージのシーケンスに等しくなることを記述する。
【００５２】
図４は、図３に示す第二の実施形態に使用した染色体を示す樹形図である。図４では、一つの染色体が一本の木をなしており、木のエッジ（一辺）には、文字で表される何らかの通信動作が付されている。また各エッジの終端のノードには番号が付されている。同じノードで始まるすべてのエッジには異なる印を付す。本例で使用する遺伝的オペレータは交差と突然変異であり、それらは部分木を交換したり置き換えたりすることで作用する。様々な実施形態では、交差は、二つの親染色体からなるランダムに選択された二つの部分木を交換することであり、突然変異は、ランダムに選択された部分木をランダムに生成された部分木と置き換えることである。交差や突然変異の候補は、トーナメント選択により選択する。多くの実施例では、トーナメント選択におけるトーナメントサイズを７とする。しかしながら、トーナメントの大きさが７より大きくても小さくても、本発明の精神あるいは範囲を逸脱することなく使用することができることを理解されたい。染色体あるいは木は有限状態オートマトンの一表現である。
【００５３】
図５は、図４の樹形図に対応する有限状態オートマトンを示す図である。図５の循環図は、図４の木から、ｋの葉をｋ番目の親ノードで置き換えることによって形成されたものである。図のノードはぞれぞれオートマトンの状態を示している。木のルートがオートマトンの初期状態である。図５の循環図に示すように、初期状態で動作ａを行うと、ｃを行うことでルートノード（初期状態）に戻る状態になる。これに対して、初期状態で動作ｂを行うと動作ｄおよびｅが可能な状態になる。ｄを行うと、ルートノードに戻り、ｅを行うと、単に循環してそれ自身に戻る。この形のオートマトンはプロセス代数で記述可能なプロセスのサブセットである。生成される個々のプログラムはこのサブセットに限定される。
【００５４】
本例における染色体の初期集団には、ランダムに生成された木が含まれ、その木には平均８個のノードと各ノードにつき平均２つの後継が含まれている。印付けされた各エッジ、すなわち図４におけるエッジａからｅは何らかの通信動作を示している。様々な実施形態において、この通信動作は、メッセージを送ること、あるいは受け取ることとすることができ、さらに、別の様々な実施形態において、動作は信号に対して処理を行うことであり、たとえば信号をフィルタリングしたり変調したりすることである。各木の個々の動作が組み合わさって、通信プロセスが構築される。
【００５５】
この第二の実施形態において、個別の染色体の適合度を、まずその染色体に対応するプロセス３２０を計算することによって求める。個々の染色体に対応するプロセス３２０を決めるには、図５のサイクルを、各サブプロセスａからｅの振る舞いの数学式に変換する。このプロセス３２０を次いで、図３に示す周知の環境３３０に並行するように構成し、同時にプロセス３２０と環境３３０との間のすべての通信動作を隠蔽し、新たなプロセス３１０を形成する。次いで、この新たなプロセス３１０の意味と仕様プロセス３６０の意味との間の距離を、距離空間意味論を用いて求める。次に、新たなプロセス３１０を定義するのに使用した染色体のノードの数を求める。その染色体の適合度がｄとｋ／ｋ0・ｄの最大値となる。ここで、ｋ0は染色体の予想最大サイズ、ｋはその染色体の実際のサイズ、ｄは求めた距離である。ｋ0より大きな染色体には適合度ペナルティを課して、同じ振る舞いの染色体でもより単純構造の染色体が支持されるようにする。
【００５６】
図６は本発明によるプログラムを進化させるのに使用可能なコード生成システム１００の一実施形態を示すブロック図である。生成したコードは所定の仕様に対して正しさが証明できるものとなる。図６に示すように、コード生成システム１００には、入出力インターフェース１１０と、コントローラ１２０と、メモリ１３０と、仕様受信回路、ルーチンあるいはアプリケーション１４０（仕様受信手段）と、プログラム個体群生成回路、ルーチンあるいはアプリケーション１５０（現在プログラム個体群生成手段）と、プログラム分析回路、ルーチンあるいはアプリケーション１６０（プログラム分析手段）と、距離値判定回路、ルーチンあるいはアプリケーション１７０（距離値判定手段、即ち適合度判定手段）と、突然変異および／または交差実行回路、ルーチンあるいはアプリケーション１８０（突然変異および／または交差実行手段、即ち新個体群生成手段）とを備えており、それらは一つまたは複数のコントロールおよび／またはデータバスおよび／またはアプリケーションプログラムインターフェース１９０によって適切に相互接続されている。
【００５７】
図６に示すように、コード生成システム１００は、多くの実施形態において、プログラムされた汎用コンピュータを用いて実装される。しかしながらコード生成システム１００はまた、特定目的のコンピュータや、プログラムされたマイクロプロセッサあるいはマイクロコントローラおよび周辺集積回路素子（peripheral integrated circuit element）、ＡＳＩＣあるいは他の集積回路、デジタル信号プロセッサ、個別素子回路（discrete element circuit）等の論理回路あるいは配線電子回路、ＰＬＤ、ＰＬＡ、ＦＰＧＡ、ＰＡＬ等のプログラム可能な論理装置などを用いて実装することもできる。一般に、図１および図２に示したフローチャートを順に実行することのできる有限状態機械を実装することのできる装置はどれでも、コード生成システム１００の実装に使用することができる。
【００５８】
図６に示すように、メモリ１３０は、揮発性あるいは非揮発性の可変メモリ、または不変あるいは固定メモリを適切に組み合わせて実現することができる。可変メモリは、揮発性であっても非揮発性であっても、静的あるいは動的ＲＡＭ、フロッピー（登録商標）ディスクおよびディスクドライブ、書き込み可能なあるいは書き換え可能な光学ディスクおよびディスクドライブ、ハードドライブ、フラッシュメモリ等のいずれか一つまたは複数を用いて実装することができる。同様に、不変あるいは固定メモリは、ＲＯＭ、ＰＲＯＭ、ＥＰＲＯＭ、ＥＥＰＲＯＭ、ＣＤ−ＲＯＭあるいはＤＶＤ−ＲＯＭディスク等の光学ＲＯＭディスクとディスクドライブなどを使用することによって実装することができる。
【００５９】
図６に示す様々な回路、ルーチンあるいはアプリケーション１４０、１５０、１６０、１７０および１８０のそれぞれは、所定の機能をコンピュータに実行させる手段であり、適切にプログラムされた汎用コンピュータの一部として実装することができることを理解されたい。別の方法としては、図６に示す回路、ルーチンあるいはアプリケーションのそれぞれを、ＡＳＩＣ内に物理的に異なるハードウェア回路として、またはＦＰＧＡ，ＰＬＤ，ＰＬＡあるいはＰＡＬを用いて、または個別論理素子あるいは個別回路素子を用いて実現することができる。また別の方法としては、図５に示す回路、ルーチンあるいはアプリケーションのそれぞれを、コード生成システム１００のメモリ１３０に記憶された個々のアプリケーションユニット、オブジェクト、ルーチン、サブル−チン、プロシージャ等として実現することができる。図６に示す回路、ルーチン、アプリケーションあるいはプロシージャのそれぞれが取りうる特定の形は、設計上の選択事項であり、当業者には自明で予測できるものである。
【００６０】
個々のアプリケーションユニット、オブジェクト、ルーチン、サブル−チン、プロシージャ等、ここでは「プロシージャ」と総称することにするが、それらは、所望の結果へ導くコンピュータ処理されたステップからなる首尾一貫したシーケンスであることが望ましい。これらのステップは一つまたは複数のコンピュータ命令によって、および／またはそれらにおいて定義することができる。これらのステップは、ステップを定義する命令を実行するコンピュータで実行することができる。したがって、「プロシージャ」という言葉は、たとえば命令のシーケンス、プログラムされた手順（プロシージャ）あるいはプログラムされた機能（ファンクション）においてまとめられた命令シーケンス、および／または一台または複数台で実行されるプログラムされたプロセス内でまとめられた命令シーケンスを意味しうる。かかるプロシージャはまた、プロシージャを実行する回路構成内に直接実装することができる。さらに、コンピュータ制御された方法を、一つまたは複数の適切なプログラムを実行するコンピュータによって、その方法を実行するように設計された特定用途のハードウェアによって、あるいはこのようなハードウェア、ファームウェアおよび／またはソフトウェア要素のいかなる組み合わせによって実行することができる。
【００６１】
図６に示すように、一つまたは複数のユーザ入力装置１０２、一つまたは複数の出力装置１０６、データソース２００および／またはデータシンク（データ受信装置）２２０を、リンク１０４、１０８、２１０および２３０をそれぞれ使用して入出力インターフェース１１０へ接続することができる。
【００６２】
一つまたは複数のユーザ入力装置１０２をそれぞれは、多数の入力装置、たとえばキーボード、マウス、ジョイスティック、トラックボール、タッチパッド、タッチスクリーン、ペンシステム、マイクロフォンおよび関連する音声認識ソフトウェア、またはその他の、システム１００へのデータおよび／またはユーザコマンドを入力するための他の周知の装置やこれから開発される装置の一つ、またはいずれかの組み合わせとすることができる。図６の一つまたは複数のユーザ入力装置１０２は同じ種類の装置としなくてもよい。
【００６３】
一般に、図６に示すデータソース２００は、適切なデータをコード生成システム１００に提供することができる何らかの周知の装置あるいは今後開発される装置とすることができる。一般に、図６に示すデータシンク２２０は、コード生成システム１００が生成した、正しさを証明できるコードを受信することができる何らかの周知の装置あるいは今後開発される装置とすることができる。一般に、一つまたは複数の出力装置１０６は、生成された正しさを証明できるコードのようなデータをユーザや他の人に出力または表示することができる何らかの周知の装置あるいは今後開発される装置とすることができる。
【００６４】
ユーザ入力装置１０２、一つまたは複数の出力装置１０６、データソース２００およびデータシンク２２０をコード生成システム１００に接続するリンク１０４、１０８、２１０および２３０はそれぞれ、直結ケーブル、モデム、ローカルエリアネットワーク、広域ネットワーク、イントラネット、インターネット、他の分散型処理ネットワーク、また他の周知のあるいは今後開発される接続装置とすることができる。これらのリンク１０４、１０８、２１０および２３０はそれぞれ有線あるいは無線の部分を含みうることが理解されよう。一般に、リンク１０４、１０８、２１０および２３０はそれぞれ、それぞれの装置をコード生成システム１００に接続するのに使用することができる、周知のあるいは今後開発される接続システムあるいは構成を用いて実現することができる。ここで、リンク１０４、１０８、２１０および２３０が同じ種類のリンクである必要はないことを理解されたい。
【００６５】
様々な実施形態において、プログラム個体群生成回路、ルーチンあるいはアプリケーション１５０は、初期集団のプログラムを生成する。また別の様々な実施形態において、初期集団のプログラムは、一つまたは複数のユーザ入力装置１０２を通じてユーザが入力したり、データソース２００からアップロードしたりすることができる。プログラム分析回路、ルーチンあるいはアプリケーション１６０はその初期集団から個々のプログラムを選択し、それを分析して、その選択したプログラムの実際の振る舞いを判定する。距離値判定回路、ルーチンあるいはアプリケーション１７０は、プログラム分析回路、ルーチンあるいはアプリケーション１６０が求めた個別プログラムの意味と仕様の間の距離を計算することによって、適合度関数を実行する。
【００６６】
操作において、コード生成システム１００は、コード生成システム１００が進化させる特定のプログラムの所望の振る舞いを形式化した仕様を入力するか、あるいは受け取る。様々な実施形態において、仕様は、データソース２００から仕様受信回路、ルーチンあるいはアプリケーション１４０に供給されてもよい。他の多くの実施形態において、仕様は一つまたは複数のユーザ入力装置１０２を介し、データソース２００からのデータを含めて、仕様受信回路、ルーチンあるいはアプリケーション１４０に入力することができる。
【００６７】
ひとたび現在のプログラムについて距離値が得られると、その値は現在のプログラムと関連付けられ、プログラムと値はメモリ１３０に記憶される。プログラム分析回路、ルーチンあるいはアプリケーション１６０は個体群における各プログラムの分析を続け、その分析は距離値判定回路、ルーチンあるいはアプリケーションが、現在のプログラムの距離値がゼロであると判定するまで行われる。現在の個体群の一プログラムの距離値がゼロであることがわかると、そのプログラムを別途記憶して、正しさが証明できるプログラムに進化したことを示す信号を一つまたは複数の出力装置１０７を介してオペレータに送る。距離値判定回路、ルーチンあるいはアプリケーション１７０が個体群におけるプログラム個体をそれぞれ評価して、距離値がゼロとなるプログラムが見つからない場合、突然変異および／または交差実行回路、ルーチンあるいはアプリケーション１８０を呼び出す。
【００６８】
突然変異および／または交差実行回路、ルーチンあるいはアプリケーション１８０は、距離値判定回路、ルーチンあるいはアプリケーション１７０で測定された前世代の最も適合度の高い個体に対し突然変異および／または交差操作を組み合わせて行い、次の世代用に現在の個体群のプログラムを作成する。様々な実施形態において、次の世代用の現在のプログラム個体群がこれまでの個体群に取って代わる。突然変異および／または交差実行回路、ルーチンあるいはアプリケーション１８０によって作成された個体群はメモリ１３０あるいはデータシンク２００に記憶される。様々な実施形態において、突然変異および／または交差実行回路、ルーチンあるいはアプリケーションで作成されたそれぞれの新しいプログラム個体群で、メモリに記憶されたこれまでのプログラム個体群が上書きされる。新しい個体群プログラムは現在の個体群プログラムとなり、コード生成システム１００のプロセスは、プログラム分析回路、ルーチンあるいはアプリケーション１６０が現在の個体群の各プログラムを選択実行することから始まり繰り返される。正当性証明可能なコード生成システム１００はこのようにして繰り返し、一プログラムが仕様を満たすよう進化するまで動作し続ける。
【００６９】
本発明を上述の実施形態と合わせ説明してきたが、様々な代替形態、修正形態、変形形態、改良および／または実質的な同等物が、周知のものでも現在予定外のものでも、あるいは予定外とおもわれるものでも、少なくとも当業者には明らかであろう。したがって、上述してきたような本発明の実施形態は、説明のためのものであり、本発明を限定するものではない。本発明の精神および範囲を逸脱することなく様々な変形が可能である。したがって、本発明は、周知のあるいはこれから開発されるすべての代替形態、修正形態、変形形態、改良および／または実質的な同等物を包含するものとして解釈されるものである。
【図面の簡単な説明】
【００７０】
【図１】本発明によるコンピュータコードを進化させるための方法の一実施形態を概説するフローチャートである。
【図２】本発明による個別プログラムの適合度を判定するための方法の一実施形態をより詳細に説明するフローチャートである。
【図３】通信ソフトウェアを合成するための仕様を定義する通信システムの要素を示すブロック図である。
【図４】有限状態オートマトンの状態を示す樹形図である。
【図５】決定性有限状態オートマトンを定義する循環グラフである。
【図６】本発明による、正当性証明可能なプログラムコードを生成するためのシステムの一実施形態を示すブロック図である。
【符号の説明】
【００７１】
１００  コード生成システム
１４０  仕様受信回路、ルーチンあるいはアプリケーション
１５０  プログラム個体群生成回路、ルーチンあるいはアプリケーション
１６０  プログラム分析回路、ルーチンあるいはアプリケーション
１７０  距離値判定回路、ルーチンあるいはアプリケーション
１８０  突然変異および／または交差実行回路、ルーチンあるいはアプリケーション
３００  通信ソフトウェアプログラム
【図１】
2005182806.tif 000006
【図２】
2005182806.tif 000007
【図３】
2005182806.tif 000008
【図４】
2005182806.tif 000009
【図５】
2005182806.tif 000010
【図６】
2005182806.tif 000011