プログラムの変換方法
【課題】プログラムを、命令型言語（imperative language）から宣言型言語（declarative
language）へ形式的に変換することに伴う問題を解決すること。
【解決手段】本発明は、コンピュータ用の命令型言語Ｌ１で表された所定のプログラムＰ中の変数Ｖ（Ｐ） を定義する第１のステップであって、該Ｐは一群の単語定義によって特定され、該単語定義の各々は一意的な単語に関するものである第１のステップと、所定の構文法及び意味論に基づいて、前記Ｐ中の演算式もしくは論理式であるｅを置換する第２のステップと、前記プログラムＰの各単位を対応する演算式もしくは論理式である式ｅに変換するための関数Ｄを、前記Ｖ（Ｐ）、ｅ、前記所定の構文法及び意味論に基づいて規定する第３のステップと、所定の規則に基づき、前記第３のステップで規定された関数Ｄを変換して宣言型言語Ｌ２で表されるプログラムＰ２を生成する第４のステップとを具備する。
language）へ形式的に変換することに伴う問題を解決すること。
【解決手段】本発明は、コンピュータ用の命令型言語Ｌ１で表された所定のプログラムＰ中の変数Ｖ（Ｐ） を定義する第１のステップであって、該Ｐは一群の単語定義によって特定され、該単語定義の各々は一意的な単語に関するものである第１のステップと、所定の構文法及び意味論に基づいて、前記Ｐ中の演算式もしくは論理式であるｅを置換する第２のステップと、前記プログラムＰの各単位を対応する演算式もしくは論理式である式ｅに変換するための関数Ｄを、前記Ｖ（Ｐ）、ｅ、前記所定の構文法及び意味論に基づいて規定する第３のステップと、所定の規則に基づき、前記第３のステップで規定された関数Ｄを変換して宣言型言語Ｌ２で表されるプログラムＰ２を生成する第４のステップとを具備する。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、プログラムの変換方法に関するものである。
【背景技術】
【０００２】
ソフトウェア開発およびメンテナンスは、経済において非常に重要な活動となっている。何千億ドルもが、毎年、ソフトウェアの開発およびメンテナンスに使用され、この金額は年々増加している。ソフトウェア開発とメンテナンスに対するニーズのこうした増大に対処するために、言語、方法論、ツールが数多く提唱された。今日、我々の推定では、２０００以上の異なるプログラミング言語が存在し、こうした言語は、プログラミング言語のパラダイムと呼ばれる様々な原理 (命令型、オプジェクト指向型、関数型、論理型、並列型、など) に基づいている。
【０００３】
しかし、ソフトウェア・エンジニアリング分野における近年のめざましい進展にもかかわらず、ソフトウェア開発プロジェクトにおける失敗の数は非常に憂慮される状態にある、という統計が多い。つまり、支払いを受けただけで納入されなかったソフトウェア、納入されただけで使用されなかったソフトウェア、作り直したり放棄されたりしたソフトウェア、また、度重なる変更後にやっと使用されたソフトウェアなどが数多く存在する。基本的に、このことは、ソフトウェアそのものが複雑なために、その開発およびメンテナンスに必要な時間と費用の見積りが誤っている可能性が高いということに原因がある。また、今日のニーズに適切に見合う言語および方法論が不足していることにも原因がある。さらに、ソフトウェア開発が成功するかどうかは、どのプログラミング言語方法論を選択するかにも非常に左右され、この選択が、ソフトウェア開発およびメンテナンスの費用に重大な影響を及ぼしている。
【非特許文献１】エイ・ベイトマン、ジェイ・マーフィ著、「レガシーシステムの移築」、作業報告ＣＡ−２８９４、ダブリン市立大学コンピュータ応用学科
【非特許文献２】エル・エイ・べラディ、エム・エム・レーマン著、「巨大プログラム開発モデル」、ＩＢＭシステムズ・ジャーナル、１５（３）：ｐ．２２５−２５２、１９７６年
【非特許文献３】エム・ブローディ、エム・ストンブレイカ著、「ダーウィン：レガシー情報システムの段階的移行について」、技術レポートＴＲ−０２２２−１０−９２−１６５、分散オブジェクト・コンピューティング・グループ、１９９３年３月
【非特許文献４】フレミング・ニールソン、ハンネ・リース・ニールソン著、「アプリケーションについての意味論：公式紹介」、ワイリー・プロフェッショナル・コンピューティング、ＩＳＢＮ０ ４７１ ９２９８０ ８、ワイリー、１９９２年
【非特許文献５】根来 文生著、「Lyee ソフトウェアの原理」、２１世紀（ IS2000 ）における情報社会についての国際会議会報pp121- 189、日本、福島県会津、２０００年１１月
【非特許文献６】根来文生、アイ・ハミド（I.Hamid）著、「意思工学の提案」、データベースと情報システムの進歩に関する第５回東ヨーロッパ会議研究（ＡＤＢＩＳ’２００１）、リトアニア、ヴィルニウス、２０００年９月
【非特許文献７】ピー・プロトキン著、「プログラミング言語として考えられるＬｅｆ」、理論的コンピュータ科学 、５：２２３−２５５、１９７７年
【非特許文献８】ディー・スコット著、「ＩＳＷＩＭ、ＣＵＣＨ、ＯＷＨＹのタイプ理論的代替案」、理論的コンピュータ科学 、１２１（１−２）：４１１−４４０、１９９３年１２月６日
【非特許文献９】ビー・ウー、ディー・ローレス、ジェイ・ビスバル、ジェイ・グリムソン、ヴィ・ウェイダ、アール・リチャードソン、ディ・オサリバン著、「ちぎり方法論：レガシー情報システムの移住のためのゲートウェイ・フリー・アプローチ」、複雑なコンピュータ・システム技術についての第３回ＩＥＥＥ会議（ＩＣＥＣＣＳ Ｓ９７）予稿集、イタリア、コモ、ヴィラ・オルモ
【発明の開示】
【発明が解決しようとする課題】
【０００４】
その結果として、驚くほど数多くのプログラミング言語 (ツール、方法論など) が存在するにもかかわらず、より単純で表現力に富み、かつ、効果的な新しいプログラミング言語を作り出そうとする研究分野は、今でもとても活発であり、その研究結果は非常に高く評価されている。特に、ソフトウェア消費者と開発者の両者にとって非常に興味深いのは、プログラムをある言語から別の言語へ変換することを可能にすることである。実は、こういったことが可能になると、組織の多くが、ソフトウェア・エンジニアリング分野の発展から恩恵を受け、新しいソフトウェア
(頻繁にアップデートを必要とするもの) を時代遅れの古い言語 (Cobol （商標）や Pascal （商標）など) を使って開発するのに多大な費用がかかるという問題を解決することが可能になる。
【０００５】
本発明は、プログラムを、命令型言語（imperative language）から宣言型言語（declarative
language）へ形式的に変換することに伴う問題を解決することを目的とする。そのために、簡単な命令型言語Ｌ１を定義する。Ｌ１は、命令型パラダイムに見受けられる基本的な命令文（statements）、つまり、代入、ループ、選択、条件分枝などをサポートする。また、宣言型言語
Ｌ２も定義する。Ｌ２では、プログラムが独立変数の定義の集合によって構成されており、この定義には、特別な算術式 (条件式あるいは再帰的式)
が含まれている。例えば、x = 5 + if (a < 3, 2 * a, a - 1) は、Ｌ２ の定義でありえる。ここでは、x
の値が、a < 3 の場合には 5 + 2 * a の値となり、それ以外の場合には 5 + (a - 1) の値となる。それぞれの言語に付随する意味論は表示的（denotational）で、そこでは、与えられた環境
(メモリー状態) におけるプログラムの意味論が、１つの環境となる。本発明は、最後に、Ｌ１ によるプログラムを、 (意味論的に) 同等なＬ２のプログラムに移行（migrate）する形式的変換関数（formal
translation function）を提案し、その正しさ (いかなるプログラムでも、元のバージョンの意味論が、変換されたバージョンの意味論と同等であること)
を証明することを目的とする。
【課題を解決するための手段】
【０００６】
本発明は、コンピュータ用の命令型言語Ｌ１で表された所定のプログラムＰ中の変数Ｖ（Ｐ） を定義する第１のステップであって、該Ｐは一群の単語定義によって特定され、該単語定義の各々は一意的な単語に関するものである第１のステップと、所定の構文法及び意味論に基づいて、前記Ｐ中の演算式もしくは論理式であるｅを置換する第２のステップと、前記プログラムＰの各単位を対応する演算式もしくは論理式である式ｅに変換するための関数Ｄを、前記Ｖ（Ｐ）、ｅ、前記所定の構文法及び意味論に基づいて規定する第３のステップと、所定の規則に基づき、前記第３のステップで規定された関数Ｄを変換して宣言型言語Ｌ２で表されるプログラムＰ２を生成する第４のステップとを具備する。
【０００７】
本発明では、標準的な命令型言語の単純なバージョンであるＬ１ を使用する。この言語には、代入（affectation）、条件命令、ループ、および、シーケンス、といった、基本的かつ重要な構文が含まれている。宣言型言語Ｌ２
は、Lyee （商標） から触発されたもので、ソフトウェアを変数定義の集合によって指定する。しかしながら、Lyee のアプローチとは異なり、変数の定義は、ループなどの特別な算術式を含む。また、Ｌ２
によるプログラムの定義は、全て互いに独立である。それぞれの言語に付随する意味論は表示的であり、そこでは、ある環境 (メモリー状態) におけるプログラムの意味論もまた
1つの環境となる。さらに、形式的変換関数 Ｄも提案する。この関数は、いかなるＬ１ プログラムも、同等なＬ２ プログラムに移行することが可能であり、この正しさを証明する。これにより、プログラムを命令型言語から宣言型言語に移行することを可能にする形式的方法が実現される。
【発明の効果】
【０００８】
本発明によれば、プログラムを単語定義の集合により要件指定する宣言型言語Ｌ２を定義した。各定義は、それぞれ1つのユニークな変数に関したもので、かつ、他の定義から完全に独立である。さらに、古典的命令型言語Ｌ１を提案し、言語Ｌ１によるどんなプログラムも、言語Ｌ２による同等なプログラムに変換する関数Ｄを定義した。関数Ｄの正しさは、図１が変換可能であることを示すことにより証明された。これにより、プログラムを、命令型言語（imperative
language）から宣言型言語（declarative language）へ形式的に変換することに伴う問題が解決され、命令型言語から宣言型言語への機械的な変換が可能となる。
【発明を実施するための最良の形態】
【０００９】
［本発明の概要］
プログラムを、命令型言語（imperative language）から宣言型言語（declarative
language）へ形式的に変換することに伴う問題の研究について述べる。そのために、簡単な命令型言語Ｌ１を定義する。Ｌ１は、命令型パラダイムに見受けられる基本的な命令文（statements）、つまり、代入、ループ、選択、条件分枝などをサポートする。また、宣言型言語
Ｌ２も定義する。Ｌ２では、プログラムが独立変数の定義の集合によって構成されており、この定義には、特別な算術式 (条件式あるいは再帰的式)
が含まれている。例えば、x = 5 + if (a < 3, 2 * a, a - 1) は、Ｌ２ の定義でありえる。ここでは、x
の値が、a < 3 の場合には 5 + 2 * a の値となり、それ以外の場合には 5 + (a - 1) の値となる。それぞれの言語に付随する意味論は表示的（denotational）で、そこでは、与えられた環境
(メモリー状態) におけるプログラムの意味論が、１つの環境となる。最後に、Ｌ１ によるプログラムを、 (意味論的に) 同等なＬ２のプログラムに移行（migrate）する形式的変換関数（formal
translation function）を提案し、その正しさ (いかなるプログラムでも、元のバージョンの意味論が、変換されたバージョンの意味論と同等であること)
を証明する。
［1 ．序論］
ソフトウェアをあるプログラミング言語から他の言語へと移行するのに成功するためには、２つの条件が必須である。第一に、手法は完全に自動的である必要がある。なぜなら、人間が介入すると、一般的に、間違いが起こりやすく、仕事量が多く、かつ、費用がかかるからである。第二に、手法の正しさを証明する必要がある。言い換えれば、次のことを示す形式的証明 (正しそうに見える単なる非形式的論拠ではなく) が必要である。つまり、プログラムの変換されたバージョンが、その元のバージョンと、明確に定義された同等関係の観点からみて同等であること、である。移行手法が非特許文献
１、２、３及び９ に多数提案されているが、どれもたいした成功を納めてはいない。
【００１０】
本発明では、プログラムを命令型言語から宣言型言語に移行することを可能にする形式的方法を紹介する。そのために、標準的な命令型言語の単純なバージョンであるＬ１
を使用する。この言語には、代入（affectation）、条件命令、ループ、および、シーケンス、といった、基本的かつ重要な構文が含まれている。宣言型言語Ｌ２
は、Lyee（商標）（非特許文献５及び６） から触発されたもので、ソフトウェアを変数定義の集合によって指定する。しかしながら、Lyee のアプローチとは異なり、変数の定義は、ループなどの特別な算術式を含む。また、Ｌ２
によるプログラムの定義は、全て互いに独立である。それぞれの言語に付随する意味論は表示的であり、そこでは、ある環境 (メモリー状態) におけるプログラムの意味論もまた
1つの環境となる。さらに、形式的変換関数 Ｄも提案する。この関数は、いかなるＬ１ プログラムも、同等なＬ２ プログラムに移行することが可能であり、この正しさを証明する。
【００１１】
本明細書の残りの部分の構成は次のようになっている。２節では、単純で古典的な命令型言語であるＬ１ の構文規則と表示的意味論について述べる。３節では、宣言型言語であるＬ２
の構文規則と表示的意味論について提示する。４節では、変換関数Ｄについて紹介する。５節では、変換プログラムの例をいくつか提示し、関数Ｄがどのように機能するかを示す。６節では、Ｄの正しさ (つまり、プログラムの意味論が変換後も維持されていること) を証明する。７節では、言語Ｌ２ の重要な特徴について論議する。最後に、８節では、本研究についての最終的な所見および今後の研究について、結論として簡単に説明する。
［２．命令型言語］
この節では、命令型言語Ｌ１ の構文規則と表示的意味論について述べる。
２.１ 構文規則
言語Ｌ１の、メタ変数とカテゴリーは以下のようになっている。
●ｎの範囲は、値の集合Ｚの範囲である。
●ｘの範囲は、変数の集合Ｘの範囲である。
●a, a1 , a2 , . . . の範囲は、算術式の集合Ａ１の範囲である。
●b, b1 , b2
, . . . の範囲は、ブール式の集合Ｂ１の範囲である。
●P, P1 , P2 , . . . の範囲は、プログラムの集合Ｌ１の範囲である。
【００１２】
Ｌ１ の構文法は、ＢＮＦ（Backus Naur Form：バッカス・ナウア記法）の文法に従い、テーブル 1 のようになる。
＜テーブル１：Ｌ１の構文規則＞
算術式の構文規則：
a ::= n | x | a1 ＋
a2 | a1 * a2 | a1 − a2
ブール式の構文規則：
【００１３】
【数１】
プログラムの構文規則：
P ::= x = a
| if b then P
else P
| while b do P
| P; P
２.２ 意味論
● 算術式
算術式の意味論は、式に表れる変数を束縛する値に依存する。例えば、x が5に束縛される場合には、式 x +
2は7と評価される。したがって、算術式の意味を定義するための、環境 (または状態) の概念を導入する必要がある。環境は、変数を入力として取り、変数を束縛する値を出力として与える関数として定義される。つまり、Ｘ
→ Ｚである。s が環境である場合は、環境sにおける変数xを束縛する値を、s(x)、x s または s x と表す。その結果、可能な環境全ての集合をгと表示する。最後に、任意の環境 s における算術式の意味論をテーブル２に示す。そこでは、次のようになっている。
【００１４】
【数２】
＜テーブル２：Ｌ１の意味論＞
算術式の意味論：
【００１５】
【数３】
ブール式の意味論：
【００１６】
【数４】
プログラムの意味論：
【００１７】
【数５】
例えば、
【００１８】
【数６】
とすると、式
x + 1 の意味論は以下のようになる。
【００１９】
【数７】
●ブール式：
ブール式の意味論は、関数
【００２０】
【数８】
によって表され、ここで
bool = {true,
false}である。
【００２１】
テーブル２にあるように
【００２２】
【数９】
の定義は、
【００２３】
【数１０】
の定義の上に成り立っている。
● プログラム：
プログラムの意味論はテーブル２に示されたとおりである。そこでは次のようになっている。
【００２４】
【数１１】
【００２５】
【数１２】
は次のように定義する：
【００２６】
【数１３】
‐ μf は、関数 f の最小不動点 (この概念については後ほど詳しく述べる) である。
以下に、各種プログラムの意味論の背後にあるアイデアについて述べる。
‐ 所与の環境 s における 代入 « x = a » の意味論は、新しい環境
【００２７】
【数１４】
であり、そこでは x は、同じ環境 s における式 a の評価に束縛される。
‐ ２つのプログラムの逐次配列 « P1; P2 » の意味論は、その２つのプログラムの意味論の合成である。つまり以下のようになっている。
【００２８】
【数１５】
‐ 命令 « if » の意味論は次のようになる。
【００２９】
【数１６】
関数condを次のように定義する。
【００３０】
【数１７】
ここでは
【００３１】
【数１８】
である。よって次のようになる。
【００３２】
【数１９】
‐ « while » の意味論は次の方程式を満たすものとする。
【００３３】
【数２０】
言い換えれば、次のようになる。
【００３４】
【数２１】
さらに、
【００３５】
【数２２】
が次の方程式の解になる必要がある。
【００３６】
【数２３】
ここでは次のようになる。
【００３７】
【数２４】
λ計算の概念を使用し、関数fを次のように表すことができる。
【００３８】
【数２５】
【００３９】
【数２６】
、ここで⊥は未定義環境を示す。この記号を使うと、部分関数について触れなくて済むため、意味論の説明を単純化することができる。
【００４０】
【数２７】
は、定義されていなければ常に⊥を返す関数である。
【００４１】
while 命令に関連する意味論は f の最小不動点で、μf で示す。つまり次のようになる。
【００４２】
【数２８】
ここで留意すべきなのは、このような関数 f の不動点の存在 (非特許文献４参照) がよく知られているということである。この命令文の証明は、以下に示した不動点定理(非特許文献７及び８参照)に基づく。
定理２.１（不動点定理） f : D → D を、⊥で表す最小要素を持つ完備半順序集合（cpo：complete partial order）
【００４３】
【数２９】
における連続関数とすると、以下のようになる。
【００４４】
【数３０】
ここで、f 0 は恒等関数であり、
【００４５】
【数３１】
の場合は、
【００４６】
【数３２】
である。
［３.宣言型言語］
この節では、宣言型言語Ｌ２ の構文規則および表示的意味論について述べる。この言語では、プログラムは、独立変数 (単語)の 定義の集合により定義される。したがって、プログラムの変数を定義する際には順序は問わない。
３.１ 構文規則
言語Ｌ２ の、メタ変数とカテゴリーは以下のようになっている。
●nの範囲は、値の集合Ｚの範囲である。
●xの範囲は、変数の集合Ｘの範囲である。
●a, a1 , a2 , . . . の範囲は、算術式の集合Ａ２の範囲である。
●b, b1 , b2 , . . . の範囲は、ブール式の集合Ｂ２の範囲である。
●P, P1 , P2 , . . . の範囲は、プログラムの集合Ｌ２の範囲である。
【００４７】
Ｌ２の構文規則は、ＢＮＦの文法に従い、テーブル３のようになる。この言語の算術式とＬ１の算術式との主要な違いは、Ｌ２の算術式は、条件式または再帰的式もあるということである。例えば、以下はＬ２の算術式である。
【００４８】
【数３３】
＜テーブル３：Ｌ２の構文規則＞
算術式の構文規則：
【００４９】
【数３４】
ブール式の構文規則：
【００５０】
【数３５】
プログラムの構文規則：
【００５１】
【数３６】
３.２ 意味論
● 算術式：
算術式を評価するには、その式が扱う各変数の値を与える環境が必要である。算術式の結果は常に、値の集合Ｚの値である。さらに正確に言うと、算術式の意味論は、テーブル４に定義されている関数
【００５２】
【数３７】
により与えられる。
‐ 値nの意味論は、環境から独立であり、n自身である。
‐ 所与の環境s∈гにおける、変数xの意味論は、環境sにおいてxを束縛する値、すなわち、s
x である。
‐ 所与の環境s∈гにおける、２つの算術式の加算 (あるいは、それぞれ、減算、乗算) の意味論は、同じ環境 s における、１番目の式の意味論と、２番目の式の意味論の加算 (あるいは、それぞれ、減算、乗算) である。
‐ 所与の環境s∈гにおける条件式 «
if(b, a1, a2) » の意味論は、関数
【００５３】
【数３８】
の計算結果である。ここでは次のようになる。
【００５４】
【数３９】
‐ 所与の環境 s における、再帰的式
【００５５】
【数４０】
の意味論は、次のように計算される。
【００５６】
まず、環境
【００５７】
【数４１】
に適用した関数fb,Pの最小不動点を計算する。このステップの結果は新しい環境で、この環境をs'とする。最後に、環境s'におけるxを束縛する値を返す。再帰的定義の意味論に関連した完全な例が結果として得られる。
＜テーブル４：Ｌ２の意味論＞
算術式の意味論：
【００５８】
【数４２】
ブール式の意味論：
【００５９】
【数４３】
プログラムの意味論：
【００６０】
【数４４】
● ブール式：
Ｌ２のブール式の意味論は、Ｌ１のブール式に付随した意味論に類似する。
●プログラム：
‐ 所与の環境s における定義
【００６１】
【数４５】
の意味論は、sに類似した新しい環境s'であるが、異なっているのは、変数xが、s'において、sにおける式aの評価に束縛されているということである。
‐ ２つのプログラムの和集合の意味論は、それらプログラムの意味論の和集合である。ここで留意すべきことは、プログラムの適格（well formed）な合成のみを考察するということである。つまり、
【００６２】
【数４６】
であるならば、a1 = a2
である。
３.３ 例
例 1
以下のプログラム Pは言語Ｌ２によるので、変数「max」という、3 つの変数 a、b、c の最大値を定義している。
【００６３】
【数４７】
ここで、環境
【００６４】
【数４８】
におけるPの意味論を知りたいとする。テーブル４にある意味論の定義に従えば、以下のようになる。
【００６５】
【数４９】
例２
言語Ｌ２によるプログラムで、
【００６６】
【数５０】
を計算するものは、以下のように書くことが可能である。
【００６７】
【数５１】
ここで、
【００６８】
【数５２】
である。
【００６９】
P’の意味論の詳細については、後半 (Ａ 節参照) で述べる。
［４．Ｌ１からＬ２へ：形式的変換］
この節では、プログラムを言語Ｌ１から言語Ｌ２へ移行する関数Ｄを定義する。さらに、Ｄの正しさを証明する。すなわち、
【００７０】
【数５３】
であるなら、以下のようになる。
【００７１】
【数５４】
まず、いくつかの有用な定義を提示する。1 番目のものは、言語Ｌ１で記述された所与のプログラムにおける定義済み変数（defined variable）の概念を示している。
定義４.１ (定義済み変数)
P を言語Ｌ１のプログラムとする。Pによる定義済み変数の集合V(P )は次のようになる。
【００７２】
【数５５】
２番目の定義は、式 e∈A2∪B2を、いかにしてプログラム P∈Ｌ２に置換するかを示す。
定義４.２ (式置換)
【００７３】
【数５６】
が言語Ｌ２によるプログラムであるとし、e をA2∪B2に含まれる式とする。Pによるeの置換 P (a) または aP を、次のように定義する。
【００７４】
【数５７】
ここで、c∈Z∪Boolであり、かつ
【００７５】
【数５８】
である。
【００７６】
ここからは、変換関数（translation function）の定義について述べる。
定義４.３ (変換関数)
プログラムを言語Ｌ１から言語Ｌ２ へと変換する関数Ｄの定義を以降に示す。
【００７７】
【数５９】
次に、各変換の背後にあるアイデアについて述べる。
●代入 « x = a » の変換は、
【００７８】
【数６０】
である。
●２つのプログラムP1とP2の配列の変換は、P2の変換とP1の変換の合成関数である。例えば、P1 : x = x + 3 かつ P2 :
y = x + y ならば、以下のようになる。
【００７９】
【数６１】
●プログラム« if b then P1
else P2 »がＬ２に変換されると、変数の集合になり、各変数は条件定義に束縛される。例えば、P1: x = 2 * x;
y = 2 かつ P2 : y = x +
y ならば、以下のようになる。
【００８０】
【数６２】
●プログラム« while b do P » がＬ２に変換されると、変数の集合になり、各変数は再帰的定義に束縛される。例えば、P: x = x + 3; y = x + y
ならば、以下のようになる。
【００８１】
【数６３】
［５． 例］
以下に、プログラム変換の例をいくつか挙げる。
●例 1
【００８２】
【表１】
D(P) の計算は次のようになる。
【００８３】
【数６４】
●例 2
【００８４】
【表２】
D(P) の計算は次のようになる。
【００８５】
【数６５】
［６．Ｄの正しさ］
この節では、変換関数Ｄがプログラムの意味論を変更しないことを示す。言い換えれば、図 1 の図が変換（commute）可能であることを証明する。
【００８６】
図 1は、
【００８７】
【数６６】
に係る。
【００８８】
主要な結果は以下の定理で与えられる
定理 ６.１
【００８９】
【数６７】
であれば、以下のようになる。
【００９０】
【数６８】
証明：
この定理の証明は、後半 (B.3 参照) で述べる。
［７．考察］
この節では、言語Ｌ２および変換関数Ｄの重要な特徴についていくつか述べる。
●言語Ｌ２で記述された所与のプログラムの各定義は、他から完全に独立である。したがって、所与のプログラムの定義は全て並行に実行することができる。
●Ｌ２で記述されたプログラムのメンテナンスは、Ｌ１のような命令型言語で記述された前のプログラムよりも容易である。例えば、以下のようなことが挙げられる。
‐ Ｌ２で記述された所与のプログラムに新しい定義 (新しい機能性) を加えても、古い定義には影響しない。
‐ Ｌ２で記述された所与のプログラムから定義をいくつか削除あるいは更新しても、他の定義には影響しない。
‐ 言語Ｌ２は、保守演算子（operator）を多数含むように、容易に拡張することができる。例えば、以下のプログラムによって、Ｌ２を簡単に拡張できる。
* X を変数の集合であるとすると、拡張 P - Xを使って、Xに含まれる変数の定義を削除したプログラムPを表すことができる。
* X を変数の集合であるとすると、拡張 P/X を使って、X に含まれる変数の定義のみを含むプログラム P のスライスを表すことができる。
* P1 とP2を２つのプログラムであるとすると、拡張
P1†P2を使って、(P1−Var(P2))∪P2 から得られるプログラムを表すことができる。言い換えれば、プログラム P2により、P1における定義を更新することができる。
【００９１】
こういった拡張により、ユーザはプログラムのメンテナンスが容易になる。
●変換過程においては、定数伝播などの最適化が自動的に関数Ｄによって行われる。例えば、プログラム P: x:= 3; y = 2 * x + z は
【００９２】
【数６９】
に変換され、これは容易に
【００９３】
【数７０】
へ変換できる。
●Ｌ１によるプログラムに、入れ子ループがある場合は、Ｌ２における入れ子再帰的関数（nested recursive function）を持った定義へと変換される。しかし、次のことを念頭に入れておくことが重要である。それは、Ｌ１のような命令型言語におけるプログラムは、変換されると、whileの入っていない(while free、つまり、入れ子ループのない)while 命令を、最大で１つ含む同等なプログラムになるということである。以下のように変換される。
− 「while」命令の後に文がない場合
【００９４】
【数７１】
− 入れ子ループがない場合
【００９５】
【数７２】
［８．結論］
本稿では、プログラムを単語定義の集合により要件指定する宣言型言語Ｌ２を定義した。各定義は、それぞれ1つのユニークな変数に関したもので、かつ、他の定義から完全に独立である。さらに、古典的命令型言語Ｌ１を提案し、言語Ｌ１によるどんなプログラムも、言語Ｌ２による同等なプログラムに変換する関数Ｄを定義した。関数Ｄの正しさは、図１が変換可能であることを示すことにより証明された。
【００９６】
今後の課題としては、言語Ｌ１をCOBOL のような実際の言語に拡張し、画面やファイルからの入出力といった、欠けている機能を補うことが挙げられる。そのためには、言語Ｌ２を拡張し、変換関数およびその正しさの証明を更新する必要がある。さらに、プログラムを言語Ｌ１から言語Ｌ２ へ自動変換することが可能なツールを開発し、かつ、Ｌ１からＬ２ へ変換されたプログラムを理解し、メンテナンスすることがいかに容易か、を研究することを計画している。
［Ａ．ケース・スタディ］
Ｌ２によるプログラムで、
【００９７】
【数７３】
を計算するものは以下のように記述することができる。
【００９８】
【数７４】
ここで、
【００９９】
【数７５】
である。
【０１００】
Ｌ２の意味論によれば、式
【０１０１】
【数７６】
が表しているのは、以下のように定義される関数
【０１０２】
【数７７】
の最小不動点の、変数som上への、射影である。
【０１０３】
【数７８】
不動点定理(２.１) から、
【０１０４】
【数７９】
の最小不動点は次のようになる。
【０１０５】
【数８０】
以降に、
【０１０６】
【数８１】
がどう計算されるかを示す。
【０１０７】
【数８２】
【０１０８】
【数８３】
【０１０９】
【数８４】
【０１１０】
【数８５】
【０１１１】
【数８６】
は、次のようになる、と導き出せる。
【０１１２】
【数８７】
最後に、
【０１１３】
【数８８】
の最小不動点は次のようになる。
【０１１４】
【数８９】
ここで、環境
【０１１５】
【数９０】
における、Pの意味論を評価するとする。
【０１１６】
ここで、
【０１１７】
【数９１】
であるから、
【０１１８】
【数９２】
の定義から、以下のように導き出せる。
【０１１９】
【数９３】
さらに、次のようになる。
【０１２０】
【数９４】
［Ｂ．定理の証明］
この節では、変換関数Ｄがプログラムの意味論を変更しないことを示す。以下の補足概念を用いる。集合ε2はA2∪B2を表し、全ての E∈ε2
において
【０１２１】
【数９５】
は以下のようになる。
【０１２２】
【数９６】
ここで、有用な結果についていくつか述べる。
補助定理 Ｂ.１
【０１２３】
【数９７】
なら、次のようになる。
【０１２４】
【数９８】
証明：
この証明は E における構造的帰納法（structural induction）による。
●E = "c" 、ここで、c∈{n, true, false}である。
【０１２５】
【数９９】
●E = "x"
【０１２６】
【数１００】
●E = ”¬b”
【０１２７】
【数１０１】
●E = ”E 1 op E 2”、ここで
【０１２８】
【数１０２】
である。
【０１２９】
【数１０３】
●E = ”if(b, E 1, E2)” ならば、以下のようになる。
【０１３０】
【数１０４】
以下の定理では、言語Ｌ１の算術式およびブール式と、言語Ｌ２の算術式およびブール式の間のつながりを示している。
補足定理
Ｂ.２
次の結果が得られた。
【０１３１】
【数１０５】
証明：
この証明は以下のものの定義から直接得られる。
【０１３２】
【数１０６】
最後に、以下の定理で、変換関数が正しいことを詳述する。
補足定理
Ｂ.３
【０１３３】
【数１０７】
ならば、次のようになる。
【０１３４】
【数１０８】
証明：
この証明はPにおける構造的帰納法による。
●P = “x = e”
【０１３５】
【数１０９】
●P = ”P1; P 2”
【０１３６】
【数１１０】
●P = ”if b then P1 else P2”
【０１３７】
【数１１１】
●P = ”while b do P1”
【０１３８】
【数１１２】
以上詳細に説明したように、本発明では、標準的な命令型言語の単純なバージョンであるＬ１ を使用する。この言語には、代入（affectation）、条件命令、ループ、および、シーケンス、といった、基本的かつ重要な構文が含まれている。宣言型言語Ｌ２
は、Lyee （商標） から触発されたもので、ソフトウェアを変数定義の集合によって指定する。しかしながら、Lyee のアプローチとは異なり、変数の定義は、ループなどの特別な算術式を含む。また、Ｌ２
によるプログラムの定義は、全て互いに独立である。それぞれの言語に付随する意味論は表示的であり、そこでは、ある環境 (メモリー状態) におけるプログラムの意味論もまた
1つの環境となる。さらに、形式的変換関数 Ｄも提案する。この関数は、いかなるＬ１ プログラムも、同等なＬ２ プログラムに移行することが可能であり、この正しさを証明する。これにより、プログラムを命令型言語から宣言型言語に移行することを可能にする形式的方法が実現される。
【０１３９】
本発明によれば、プログラムを単語定義の集合により要件指定する宣言型言語Ｌ２を定義した。各定義は、それぞれ1つのユニークな変数に関したもので、かつ、他の定義から完全に独立である。さらに、古典的命令型言語Ｌ１を提案し、言語Ｌ１によるどんなプログラムも、言語Ｌ２による同等なプログラムに変換する関数Ｄを定義した。関数Ｄの正しさは、図１が変換可能であることを示すことにより証明された。これにより、プログラムを、命令型言語（imperative
language）から宣言型言語（declarative language）へ形式的に変換することに伴う問題が解決され、命令型言語から宣言型言語への機械的な変換が可能となる。
【産業上の利用可能性】
【０１４０】
本発明によれば、プログラムを単語定義の集合により要件指定する宣言型言語Ｌ２を定義した。各定義は、それぞれ1つのユニークな変数に関したもので、かつ、他の定義から完全に独立である。さらに、古典的命令型言語Ｌ１を提案し、言語Ｌ１によるどんなプログラムも、言語Ｌ２による同等なプログラムに変換する関数Ｄを定義した。関数Ｄの正しさは、図１が変換可能であることを示すことにより証明された。これにより、プログラムを、命令型言語（imperative
language）から宣言型言語（declarative language）へ形式的に変換することに伴う問題が解決され、命令型言語から宣言型言語への機械的な変換が可能となる。
【図面の簡単な説明】
【０１４１】
【図１】本発明の数６６に係り、変換関数Ｄがプログラムの意味論を変更しないことを示すための図である。
【符号の説明】
【０１４２】
Ｄ 変換関数
【技術分野】
【０００１】
本発明は、プログラムの変換方法に関するものである。
【背景技術】
【０００２】
ソフトウェア開発およびメンテナンスは、経済において非常に重要な活動となっている。何千億ドルもが、毎年、ソフトウェアの開発およびメンテナンスに使用され、この金額は年々増加している。ソフトウェア開発とメンテナンスに対するニーズのこうした増大に対処するために、言語、方法論、ツールが数多く提唱された。今日、我々の推定では、２０００以上の異なるプログラミング言語が存在し、こうした言語は、プログラミング言語のパラダイムと呼ばれる様々な原理 (命令型、オプジェクト指向型、関数型、論理型、並列型、など) に基づいている。
【０００３】
しかし、ソフトウェア・エンジニアリング分野における近年のめざましい進展にもかかわらず、ソフトウェア開発プロジェクトにおける失敗の数は非常に憂慮される状態にある、という統計が多い。つまり、支払いを受けただけで納入されなかったソフトウェア、納入されただけで使用されなかったソフトウェア、作り直したり放棄されたりしたソフトウェア、また、度重なる変更後にやっと使用されたソフトウェアなどが数多く存在する。基本的に、このことは、ソフトウェアそのものが複雑なために、その開発およびメンテナンスに必要な時間と費用の見積りが誤っている可能性が高いということに原因がある。また、今日のニーズに適切に見合う言語および方法論が不足していることにも原因がある。さらに、ソフトウェア開発が成功するかどうかは、どのプログラミング言語方法論を選択するかにも非常に左右され、この選択が、ソフトウェア開発およびメンテナンスの費用に重大な影響を及ぼしている。
【非特許文献１】エイ・ベイトマン、ジェイ・マーフィ著、「レガシーシステムの移築」、作業報告ＣＡ−２８９４、ダブリン市立大学コンピュータ応用学科
【非特許文献２】エル・エイ・べラディ、エム・エム・レーマン著、「巨大プログラム開発モデル」、ＩＢＭシステムズ・ジャーナル、１５（３）：ｐ．２２５−２５２、１９７６年
【非特許文献３】エム・ブローディ、エム・ストンブレイカ著、「ダーウィン：レガシー情報システムの段階的移行について」、技術レポートＴＲ−０２２２−１０−９２−１６５、分散オブジェクト・コンピューティング・グループ、１９９３年３月
【非特許文献４】フレミング・ニールソン、ハンネ・リース・ニールソン著、「アプリケーションについての意味論：公式紹介」、ワイリー・プロフェッショナル・コンピューティング、ＩＳＢＮ０ ４７１ ９２９８０ ８、ワイリー、１９９２年
【非特許文献５】根来 文生著、「Lyee ソフトウェアの原理」、２１世紀（ IS2000 ）における情報社会についての国際会議会報pp121- 189、日本、福島県会津、２０００年１１月
【非特許文献６】根来文生、アイ・ハミド（I.Hamid）著、「意思工学の提案」、データベースと情報システムの進歩に関する第５回東ヨーロッパ会議研究（ＡＤＢＩＳ’２００１）、リトアニア、ヴィルニウス、２０００年９月
【非特許文献７】ピー・プロトキン著、「プログラミング言語として考えられるＬｅｆ」、理論的コンピュータ科学 、５：２２３−２５５、１９７７年
【非特許文献８】ディー・スコット著、「ＩＳＷＩＭ、ＣＵＣＨ、ＯＷＨＹのタイプ理論的代替案」、理論的コンピュータ科学 、１２１（１−２）：４１１−４４０、１９９３年１２月６日
【非特許文献９】ビー・ウー、ディー・ローレス、ジェイ・ビスバル、ジェイ・グリムソン、ヴィ・ウェイダ、アール・リチャードソン、ディ・オサリバン著、「ちぎり方法論：レガシー情報システムの移住のためのゲートウェイ・フリー・アプローチ」、複雑なコンピュータ・システム技術についての第３回ＩＥＥＥ会議（ＩＣＥＣＣＳ Ｓ９７）予稿集、イタリア、コモ、ヴィラ・オルモ
【発明の開示】
【発明が解決しようとする課題】
【０００４】
その結果として、驚くほど数多くのプログラミング言語 (ツール、方法論など) が存在するにもかかわらず、より単純で表現力に富み、かつ、効果的な新しいプログラミング言語を作り出そうとする研究分野は、今でもとても活発であり、その研究結果は非常に高く評価されている。特に、ソフトウェア消費者と開発者の両者にとって非常に興味深いのは、プログラムをある言語から別の言語へ変換することを可能にすることである。実は、こういったことが可能になると、組織の多くが、ソフトウェア・エンジニアリング分野の発展から恩恵を受け、新しいソフトウェア
(頻繁にアップデートを必要とするもの) を時代遅れの古い言語 (Cobol （商標）や Pascal （商標）など) を使って開発するのに多大な費用がかかるという問題を解決することが可能になる。
【０００５】
本発明は、プログラムを、命令型言語（imperative language）から宣言型言語（declarative
language）へ形式的に変換することに伴う問題を解決することを目的とする。そのために、簡単な命令型言語Ｌ１を定義する。Ｌ１は、命令型パラダイムに見受けられる基本的な命令文（statements）、つまり、代入、ループ、選択、条件分枝などをサポートする。また、宣言型言語
Ｌ２も定義する。Ｌ２では、プログラムが独立変数の定義の集合によって構成されており、この定義には、特別な算術式 (条件式あるいは再帰的式)
が含まれている。例えば、x = 5 + if (a < 3, 2 * a, a - 1) は、Ｌ２ の定義でありえる。ここでは、x
の値が、a < 3 の場合には 5 + 2 * a の値となり、それ以外の場合には 5 + (a - 1) の値となる。それぞれの言語に付随する意味論は表示的（denotational）で、そこでは、与えられた環境
(メモリー状態) におけるプログラムの意味論が、１つの環境となる。本発明は、最後に、Ｌ１ によるプログラムを、 (意味論的に) 同等なＬ２のプログラムに移行（migrate）する形式的変換関数（formal
translation function）を提案し、その正しさ (いかなるプログラムでも、元のバージョンの意味論が、変換されたバージョンの意味論と同等であること)
を証明することを目的とする。
【課題を解決するための手段】
【０００６】
本発明は、コンピュータ用の命令型言語Ｌ１で表された所定のプログラムＰ中の変数Ｖ（Ｐ） を定義する第１のステップであって、該Ｐは一群の単語定義によって特定され、該単語定義の各々は一意的な単語に関するものである第１のステップと、所定の構文法及び意味論に基づいて、前記Ｐ中の演算式もしくは論理式であるｅを置換する第２のステップと、前記プログラムＰの各単位を対応する演算式もしくは論理式である式ｅに変換するための関数Ｄを、前記Ｖ（Ｐ）、ｅ、前記所定の構文法及び意味論に基づいて規定する第３のステップと、所定の規則に基づき、前記第３のステップで規定された関数Ｄを変換して宣言型言語Ｌ２で表されるプログラムＰ２を生成する第４のステップとを具備する。
【０００７】
本発明では、標準的な命令型言語の単純なバージョンであるＬ１ を使用する。この言語には、代入（affectation）、条件命令、ループ、および、シーケンス、といった、基本的かつ重要な構文が含まれている。宣言型言語Ｌ２
は、Lyee （商標） から触発されたもので、ソフトウェアを変数定義の集合によって指定する。しかしながら、Lyee のアプローチとは異なり、変数の定義は、ループなどの特別な算術式を含む。また、Ｌ２
によるプログラムの定義は、全て互いに独立である。それぞれの言語に付随する意味論は表示的であり、そこでは、ある環境 (メモリー状態) におけるプログラムの意味論もまた
1つの環境となる。さらに、形式的変換関数 Ｄも提案する。この関数は、いかなるＬ１ プログラムも、同等なＬ２ プログラムに移行することが可能であり、この正しさを証明する。これにより、プログラムを命令型言語から宣言型言語に移行することを可能にする形式的方法が実現される。
【発明の効果】
【０００８】
本発明によれば、プログラムを単語定義の集合により要件指定する宣言型言語Ｌ２を定義した。各定義は、それぞれ1つのユニークな変数に関したもので、かつ、他の定義から完全に独立である。さらに、古典的命令型言語Ｌ１を提案し、言語Ｌ１によるどんなプログラムも、言語Ｌ２による同等なプログラムに変換する関数Ｄを定義した。関数Ｄの正しさは、図１が変換可能であることを示すことにより証明された。これにより、プログラムを、命令型言語（imperative
language）から宣言型言語（declarative language）へ形式的に変換することに伴う問題が解決され、命令型言語から宣言型言語への機械的な変換が可能となる。
【発明を実施するための最良の形態】
【０００９】
［本発明の概要］
プログラムを、命令型言語（imperative language）から宣言型言語（declarative
language）へ形式的に変換することに伴う問題の研究について述べる。そのために、簡単な命令型言語Ｌ１を定義する。Ｌ１は、命令型パラダイムに見受けられる基本的な命令文（statements）、つまり、代入、ループ、選択、条件分枝などをサポートする。また、宣言型言語
Ｌ２も定義する。Ｌ２では、プログラムが独立変数の定義の集合によって構成されており、この定義には、特別な算術式 (条件式あるいは再帰的式)
が含まれている。例えば、x = 5 + if (a < 3, 2 * a, a - 1) は、Ｌ２ の定義でありえる。ここでは、x
の値が、a < 3 の場合には 5 + 2 * a の値となり、それ以外の場合には 5 + (a - 1) の値となる。それぞれの言語に付随する意味論は表示的（denotational）で、そこでは、与えられた環境
(メモリー状態) におけるプログラムの意味論が、１つの環境となる。最後に、Ｌ１ によるプログラムを、 (意味論的に) 同等なＬ２のプログラムに移行（migrate）する形式的変換関数（formal
translation function）を提案し、その正しさ (いかなるプログラムでも、元のバージョンの意味論が、変換されたバージョンの意味論と同等であること)
を証明する。
［1 ．序論］
ソフトウェアをあるプログラミング言語から他の言語へと移行するのに成功するためには、２つの条件が必須である。第一に、手法は完全に自動的である必要がある。なぜなら、人間が介入すると、一般的に、間違いが起こりやすく、仕事量が多く、かつ、費用がかかるからである。第二に、手法の正しさを証明する必要がある。言い換えれば、次のことを示す形式的証明 (正しそうに見える単なる非形式的論拠ではなく) が必要である。つまり、プログラムの変換されたバージョンが、その元のバージョンと、明確に定義された同等関係の観点からみて同等であること、である。移行手法が非特許文献
１、２、３及び９ に多数提案されているが、どれもたいした成功を納めてはいない。
【００１０】
本発明では、プログラムを命令型言語から宣言型言語に移行することを可能にする形式的方法を紹介する。そのために、標準的な命令型言語の単純なバージョンであるＬ１
を使用する。この言語には、代入（affectation）、条件命令、ループ、および、シーケンス、といった、基本的かつ重要な構文が含まれている。宣言型言語Ｌ２
は、Lyee（商標）（非特許文献５及び６） から触発されたもので、ソフトウェアを変数定義の集合によって指定する。しかしながら、Lyee のアプローチとは異なり、変数の定義は、ループなどの特別な算術式を含む。また、Ｌ２
によるプログラムの定義は、全て互いに独立である。それぞれの言語に付随する意味論は表示的であり、そこでは、ある環境 (メモリー状態) におけるプログラムの意味論もまた
1つの環境となる。さらに、形式的変換関数 Ｄも提案する。この関数は、いかなるＬ１ プログラムも、同等なＬ２ プログラムに移行することが可能であり、この正しさを証明する。
【００１１】
本明細書の残りの部分の構成は次のようになっている。２節では、単純で古典的な命令型言語であるＬ１ の構文規則と表示的意味論について述べる。３節では、宣言型言語であるＬ２
の構文規則と表示的意味論について提示する。４節では、変換関数Ｄについて紹介する。５節では、変換プログラムの例をいくつか提示し、関数Ｄがどのように機能するかを示す。６節では、Ｄの正しさ (つまり、プログラムの意味論が変換後も維持されていること) を証明する。７節では、言語Ｌ２ の重要な特徴について論議する。最後に、８節では、本研究についての最終的な所見および今後の研究について、結論として簡単に説明する。
［２．命令型言語］
この節では、命令型言語Ｌ１ の構文規則と表示的意味論について述べる。
２.１ 構文規則
言語Ｌ１の、メタ変数とカテゴリーは以下のようになっている。
●ｎの範囲は、値の集合Ｚの範囲である。
●ｘの範囲は、変数の集合Ｘの範囲である。
●a, a1 , a2 , . . . の範囲は、算術式の集合Ａ１の範囲である。
●b, b1 , b2
, . . . の範囲は、ブール式の集合Ｂ１の範囲である。
●P, P1 , P2 , . . . の範囲は、プログラムの集合Ｌ１の範囲である。
【００１２】
Ｌ１ の構文法は、ＢＮＦ（Backus Naur Form：バッカス・ナウア記法）の文法に従い、テーブル 1 のようになる。
＜テーブル１：Ｌ１の構文規則＞
算術式の構文規則：
a ::= n | x | a1 ＋
a2 | a1 * a2 | a1 − a2
ブール式の構文規則：
【００１３】
【数１】
プログラムの構文規則：
P ::= x = a
| if b then P
else P
| while b do P
| P; P
２.２ 意味論
● 算術式
算術式の意味論は、式に表れる変数を束縛する値に依存する。例えば、x が5に束縛される場合には、式 x +
2は7と評価される。したがって、算術式の意味を定義するための、環境 (または状態) の概念を導入する必要がある。環境は、変数を入力として取り、変数を束縛する値を出力として与える関数として定義される。つまり、Ｘ
→ Ｚである。s が環境である場合は、環境sにおける変数xを束縛する値を、s(x)、x s または s x と表す。その結果、可能な環境全ての集合をгと表示する。最後に、任意の環境 s における算術式の意味論をテーブル２に示す。そこでは、次のようになっている。
【００１４】
【数２】
＜テーブル２：Ｌ１の意味論＞
算術式の意味論：
【００１５】
【数３】
ブール式の意味論：
【００１６】
【数４】
プログラムの意味論：
【００１７】
【数５】
例えば、
【００１８】
【数６】
とすると、式
x + 1 の意味論は以下のようになる。
【００１９】
【数７】
●ブール式：
ブール式の意味論は、関数
【００２０】
【数８】
によって表され、ここで
bool = {true,
false}である。
【００２１】
テーブル２にあるように
【００２２】
【数９】
の定義は、
【００２３】
【数１０】
の定義の上に成り立っている。
● プログラム：
プログラムの意味論はテーブル２に示されたとおりである。そこでは次のようになっている。
【００２４】
【数１１】
【００２５】
【数１２】
は次のように定義する：
【００２６】
【数１３】
‐ μf は、関数 f の最小不動点 (この概念については後ほど詳しく述べる) である。
以下に、各種プログラムの意味論の背後にあるアイデアについて述べる。
‐ 所与の環境 s における 代入 « x = a » の意味論は、新しい環境
【００２７】
【数１４】
であり、そこでは x は、同じ環境 s における式 a の評価に束縛される。
‐ ２つのプログラムの逐次配列 « P1; P2 » の意味論は、その２つのプログラムの意味論の合成である。つまり以下のようになっている。
【００２８】
【数１５】
‐ 命令 « if » の意味論は次のようになる。
【００２９】
【数１６】
関数condを次のように定義する。
【００３０】
【数１７】
ここでは
【００３１】
【数１８】
である。よって次のようになる。
【００３２】
【数１９】
‐ « while » の意味論は次の方程式を満たすものとする。
【００３３】
【数２０】
言い換えれば、次のようになる。
【００３４】
【数２１】
さらに、
【００３５】
【数２２】
が次の方程式の解になる必要がある。
【００３６】
【数２３】
ここでは次のようになる。
【００３７】
【数２４】
λ計算の概念を使用し、関数fを次のように表すことができる。
【００３８】
【数２５】
【００３９】
【数２６】
、ここで⊥は未定義環境を示す。この記号を使うと、部分関数について触れなくて済むため、意味論の説明を単純化することができる。
【００４０】
【数２７】
は、定義されていなければ常に⊥を返す関数である。
【００４１】
while 命令に関連する意味論は f の最小不動点で、μf で示す。つまり次のようになる。
【００４２】
【数２８】
ここで留意すべきなのは、このような関数 f の不動点の存在 (非特許文献４参照) がよく知られているということである。この命令文の証明は、以下に示した不動点定理(非特許文献７及び８参照)に基づく。
定理２.１（不動点定理） f : D → D を、⊥で表す最小要素を持つ完備半順序集合（cpo：complete partial order）
【００４３】
【数２９】
における連続関数とすると、以下のようになる。
【００４４】
【数３０】
ここで、f 0 は恒等関数であり、
【００４５】
【数３１】
の場合は、
【００４６】
【数３２】
である。
［３.宣言型言語］
この節では、宣言型言語Ｌ２ の構文規則および表示的意味論について述べる。この言語では、プログラムは、独立変数 (単語)の 定義の集合により定義される。したがって、プログラムの変数を定義する際には順序は問わない。
３.１ 構文規則
言語Ｌ２ の、メタ変数とカテゴリーは以下のようになっている。
●nの範囲は、値の集合Ｚの範囲である。
●xの範囲は、変数の集合Ｘの範囲である。
●a, a1 , a2 , . . . の範囲は、算術式の集合Ａ２の範囲である。
●b, b1 , b2 , . . . の範囲は、ブール式の集合Ｂ２の範囲である。
●P, P1 , P2 , . . . の範囲は、プログラムの集合Ｌ２の範囲である。
【００４７】
Ｌ２の構文規則は、ＢＮＦの文法に従い、テーブル３のようになる。この言語の算術式とＬ１の算術式との主要な違いは、Ｌ２の算術式は、条件式または再帰的式もあるということである。例えば、以下はＬ２の算術式である。
【００４８】
【数３３】
＜テーブル３：Ｌ２の構文規則＞
算術式の構文規則：
【００４９】
【数３４】
ブール式の構文規則：
【００５０】
【数３５】
プログラムの構文規則：
【００５１】
【数３６】
３.２ 意味論
● 算術式：
算術式を評価するには、その式が扱う各変数の値を与える環境が必要である。算術式の結果は常に、値の集合Ｚの値である。さらに正確に言うと、算術式の意味論は、テーブル４に定義されている関数
【００５２】
【数３７】
により与えられる。
‐ 値nの意味論は、環境から独立であり、n自身である。
‐ 所与の環境s∈гにおける、変数xの意味論は、環境sにおいてxを束縛する値、すなわち、s
x である。
‐ 所与の環境s∈гにおける、２つの算術式の加算 (あるいは、それぞれ、減算、乗算) の意味論は、同じ環境 s における、１番目の式の意味論と、２番目の式の意味論の加算 (あるいは、それぞれ、減算、乗算) である。
‐ 所与の環境s∈гにおける条件式 «
if(b, a1, a2) » の意味論は、関数
【００５３】
【数３８】
の計算結果である。ここでは次のようになる。
【００５４】
【数３９】
‐ 所与の環境 s における、再帰的式
【００５５】
【数４０】
の意味論は、次のように計算される。
【００５６】
まず、環境
【００５７】
【数４１】
に適用した関数fb,Pの最小不動点を計算する。このステップの結果は新しい環境で、この環境をs'とする。最後に、環境s'におけるxを束縛する値を返す。再帰的定義の意味論に関連した完全な例が結果として得られる。
＜テーブル４：Ｌ２の意味論＞
算術式の意味論：
【００５８】
【数４２】
ブール式の意味論：
【００５９】
【数４３】
プログラムの意味論：
【００６０】
【数４４】
● ブール式：
Ｌ２のブール式の意味論は、Ｌ１のブール式に付随した意味論に類似する。
●プログラム：
‐ 所与の環境s における定義
【００６１】
【数４５】
の意味論は、sに類似した新しい環境s'であるが、異なっているのは、変数xが、s'において、sにおける式aの評価に束縛されているということである。
‐ ２つのプログラムの和集合の意味論は、それらプログラムの意味論の和集合である。ここで留意すべきことは、プログラムの適格（well formed）な合成のみを考察するということである。つまり、
【００６２】
【数４６】
であるならば、a1 = a2
である。
３.３ 例
例 1
以下のプログラム Pは言語Ｌ２によるので、変数「max」という、3 つの変数 a、b、c の最大値を定義している。
【００６３】
【数４７】
ここで、環境
【００６４】
【数４８】
におけるPの意味論を知りたいとする。テーブル４にある意味論の定義に従えば、以下のようになる。
【００６５】
【数４９】
例２
言語Ｌ２によるプログラムで、
【００６６】
【数５０】
を計算するものは、以下のように書くことが可能である。
【００６７】
【数５１】
ここで、
【００６８】
【数５２】
である。
【００６９】
P’の意味論の詳細については、後半 (Ａ 節参照) で述べる。
［４．Ｌ１からＬ２へ：形式的変換］
この節では、プログラムを言語Ｌ１から言語Ｌ２へ移行する関数Ｄを定義する。さらに、Ｄの正しさを証明する。すなわち、
【００７０】
【数５３】
であるなら、以下のようになる。
【００７１】
【数５４】
まず、いくつかの有用な定義を提示する。1 番目のものは、言語Ｌ１で記述された所与のプログラムにおける定義済み変数（defined variable）の概念を示している。
定義４.１ (定義済み変数)
P を言語Ｌ１のプログラムとする。Pによる定義済み変数の集合V(P )は次のようになる。
【００７２】
【数５５】
２番目の定義は、式 e∈A2∪B2を、いかにしてプログラム P∈Ｌ２に置換するかを示す。
定義４.２ (式置換)
【００７３】
【数５６】
が言語Ｌ２によるプログラムであるとし、e をA2∪B2に含まれる式とする。Pによるeの置換 P (a) または aP を、次のように定義する。
【００７４】
【数５７】
ここで、c∈Z∪Boolであり、かつ
【００７５】
【数５８】
である。
【００７６】
ここからは、変換関数（translation function）の定義について述べる。
定義４.３ (変換関数)
プログラムを言語Ｌ１から言語Ｌ２ へと変換する関数Ｄの定義を以降に示す。
【００７７】
【数５９】
次に、各変換の背後にあるアイデアについて述べる。
●代入 « x = a » の変換は、
【００７８】
【数６０】
である。
●２つのプログラムP1とP2の配列の変換は、P2の変換とP1の変換の合成関数である。例えば、P1 : x = x + 3 かつ P2 :
y = x + y ならば、以下のようになる。
【００７９】
【数６１】
●プログラム« if b then P1
else P2 »がＬ２に変換されると、変数の集合になり、各変数は条件定義に束縛される。例えば、P1: x = 2 * x;
y = 2 かつ P2 : y = x +
y ならば、以下のようになる。
【００８０】
【数６２】
●プログラム« while b do P » がＬ２に変換されると、変数の集合になり、各変数は再帰的定義に束縛される。例えば、P: x = x + 3; y = x + y
ならば、以下のようになる。
【００８１】
【数６３】
［５． 例］
以下に、プログラム変換の例をいくつか挙げる。
●例 1
【００８２】
【表１】
D(P) の計算は次のようになる。
【００８３】
【数６４】
●例 2
【００８４】
【表２】
D(P) の計算は次のようになる。
【００８５】
【数６５】
［６．Ｄの正しさ］
この節では、変換関数Ｄがプログラムの意味論を変更しないことを示す。言い換えれば、図 1 の図が変換（commute）可能であることを証明する。
【００８６】
図 1は、
【００８７】
【数６６】
に係る。
【００８８】
主要な結果は以下の定理で与えられる
定理 ６.１
【００８９】
【数６７】
であれば、以下のようになる。
【００９０】
【数６８】
証明：
この定理の証明は、後半 (B.3 参照) で述べる。
［７．考察］
この節では、言語Ｌ２および変換関数Ｄの重要な特徴についていくつか述べる。
●言語Ｌ２で記述された所与のプログラムの各定義は、他から完全に独立である。したがって、所与のプログラムの定義は全て並行に実行することができる。
●Ｌ２で記述されたプログラムのメンテナンスは、Ｌ１のような命令型言語で記述された前のプログラムよりも容易である。例えば、以下のようなことが挙げられる。
‐ Ｌ２で記述された所与のプログラムに新しい定義 (新しい機能性) を加えても、古い定義には影響しない。
‐ Ｌ２で記述された所与のプログラムから定義をいくつか削除あるいは更新しても、他の定義には影響しない。
‐ 言語Ｌ２は、保守演算子（operator）を多数含むように、容易に拡張することができる。例えば、以下のプログラムによって、Ｌ２を簡単に拡張できる。
* X を変数の集合であるとすると、拡張 P - Xを使って、Xに含まれる変数の定義を削除したプログラムPを表すことができる。
* X を変数の集合であるとすると、拡張 P/X を使って、X に含まれる変数の定義のみを含むプログラム P のスライスを表すことができる。
* P1 とP2を２つのプログラムであるとすると、拡張
P1†P2を使って、(P1−Var(P2))∪P2 から得られるプログラムを表すことができる。言い換えれば、プログラム P2により、P1における定義を更新することができる。
【００９１】
こういった拡張により、ユーザはプログラムのメンテナンスが容易になる。
●変換過程においては、定数伝播などの最適化が自動的に関数Ｄによって行われる。例えば、プログラム P: x:= 3; y = 2 * x + z は
【００９２】
【数６９】
に変換され、これは容易に
【００９３】
【数７０】
へ変換できる。
●Ｌ１によるプログラムに、入れ子ループがある場合は、Ｌ２における入れ子再帰的関数（nested recursive function）を持った定義へと変換される。しかし、次のことを念頭に入れておくことが重要である。それは、Ｌ１のような命令型言語におけるプログラムは、変換されると、whileの入っていない(while free、つまり、入れ子ループのない)while 命令を、最大で１つ含む同等なプログラムになるということである。以下のように変換される。
− 「while」命令の後に文がない場合
【００９４】
【数７１】
− 入れ子ループがない場合
【００９５】
【数７２】
［８．結論］
本稿では、プログラムを単語定義の集合により要件指定する宣言型言語Ｌ２を定義した。各定義は、それぞれ1つのユニークな変数に関したもので、かつ、他の定義から完全に独立である。さらに、古典的命令型言語Ｌ１を提案し、言語Ｌ１によるどんなプログラムも、言語Ｌ２による同等なプログラムに変換する関数Ｄを定義した。関数Ｄの正しさは、図１が変換可能であることを示すことにより証明された。
【００９６】
今後の課題としては、言語Ｌ１をCOBOL のような実際の言語に拡張し、画面やファイルからの入出力といった、欠けている機能を補うことが挙げられる。そのためには、言語Ｌ２を拡張し、変換関数およびその正しさの証明を更新する必要がある。さらに、プログラムを言語Ｌ１から言語Ｌ２ へ自動変換することが可能なツールを開発し、かつ、Ｌ１からＬ２ へ変換されたプログラムを理解し、メンテナンスすることがいかに容易か、を研究することを計画している。
［Ａ．ケース・スタディ］
Ｌ２によるプログラムで、
【００９７】
【数７３】
を計算するものは以下のように記述することができる。
【００９８】
【数７４】
ここで、
【００９９】
【数７５】
である。
【０１００】
Ｌ２の意味論によれば、式
【０１０１】
【数７６】
が表しているのは、以下のように定義される関数
【０１０２】
【数７７】
の最小不動点の、変数som上への、射影である。
【０１０３】
【数７８】
不動点定理(２.１) から、
【０１０４】
【数７９】
の最小不動点は次のようになる。
【０１０５】
【数８０】
以降に、
【０１０６】
【数８１】
がどう計算されるかを示す。
【０１０７】
【数８２】
【０１０８】
【数８３】
【０１０９】
【数８４】
【０１１０】
【数８５】
【０１１１】
【数８６】
は、次のようになる、と導き出せる。
【０１１２】
【数８７】
最後に、
【０１１３】
【数８８】
の最小不動点は次のようになる。
【０１１４】
【数８９】
ここで、環境
【０１１５】
【数９０】
における、Pの意味論を評価するとする。
【０１１６】
ここで、
【０１１７】
【数９１】
であるから、
【０１１８】
【数９２】
の定義から、以下のように導き出せる。
【０１１９】
【数９３】
さらに、次のようになる。
【０１２０】
【数９４】
［Ｂ．定理の証明］
この節では、変換関数Ｄがプログラムの意味論を変更しないことを示す。以下の補足概念を用いる。集合ε2はA2∪B2を表し、全ての E∈ε2
において
【０１２１】
【数９５】
は以下のようになる。
【０１２２】
【数９６】
ここで、有用な結果についていくつか述べる。
補助定理 Ｂ.１
【０１２３】
【数９７】
なら、次のようになる。
【０１２４】
【数９８】
証明：
この証明は E における構造的帰納法（structural induction）による。
●E = "c" 、ここで、c∈{n, true, false}である。
【０１２５】
【数９９】
●E = "x"
【０１２６】
【数１００】
●E = ”¬b”
【０１２７】
【数１０１】
●E = ”E 1 op E 2”、ここで
【０１２８】
【数１０２】
である。
【０１２９】
【数１０３】
●E = ”if(b, E 1, E2)” ならば、以下のようになる。
【０１３０】
【数１０４】
以下の定理では、言語Ｌ１の算術式およびブール式と、言語Ｌ２の算術式およびブール式の間のつながりを示している。
補足定理
Ｂ.２
次の結果が得られた。
【０１３１】
【数１０５】
証明：
この証明は以下のものの定義から直接得られる。
【０１３２】
【数１０６】
最後に、以下の定理で、変換関数が正しいことを詳述する。
補足定理
Ｂ.３
【０１３３】
【数１０７】
ならば、次のようになる。
【０１３４】
【数１０８】
証明：
この証明はPにおける構造的帰納法による。
●P = “x = e”
【０１３５】
【数１０９】
●P = ”P1; P 2”
【０１３６】
【数１１０】
●P = ”if b then P1 else P2”
【０１３７】
【数１１１】
●P = ”while b do P1”
【０１３８】
【数１１２】
以上詳細に説明したように、本発明では、標準的な命令型言語の単純なバージョンであるＬ１ を使用する。この言語には、代入（affectation）、条件命令、ループ、および、シーケンス、といった、基本的かつ重要な構文が含まれている。宣言型言語Ｌ２
は、Lyee （商標） から触発されたもので、ソフトウェアを変数定義の集合によって指定する。しかしながら、Lyee のアプローチとは異なり、変数の定義は、ループなどの特別な算術式を含む。また、Ｌ２
によるプログラムの定義は、全て互いに独立である。それぞれの言語に付随する意味論は表示的であり、そこでは、ある環境 (メモリー状態) におけるプログラムの意味論もまた
1つの環境となる。さらに、形式的変換関数 Ｄも提案する。この関数は、いかなるＬ１ プログラムも、同等なＬ２ プログラムに移行することが可能であり、この正しさを証明する。これにより、プログラムを命令型言語から宣言型言語に移行することを可能にする形式的方法が実現される。
【０１３９】
本発明によれば、プログラムを単語定義の集合により要件指定する宣言型言語Ｌ２を定義した。各定義は、それぞれ1つのユニークな変数に関したもので、かつ、他の定義から完全に独立である。さらに、古典的命令型言語Ｌ１を提案し、言語Ｌ１によるどんなプログラムも、言語Ｌ２による同等なプログラムに変換する関数Ｄを定義した。関数Ｄの正しさは、図１が変換可能であることを示すことにより証明された。これにより、プログラムを、命令型言語（imperative
language）から宣言型言語（declarative language）へ形式的に変換することに伴う問題が解決され、命令型言語から宣言型言語への機械的な変換が可能となる。
【産業上の利用可能性】
【０１４０】
本発明によれば、プログラムを単語定義の集合により要件指定する宣言型言語Ｌ２を定義した。各定義は、それぞれ1つのユニークな変数に関したもので、かつ、他の定義から完全に独立である。さらに、古典的命令型言語Ｌ１を提案し、言語Ｌ１によるどんなプログラムも、言語Ｌ２による同等なプログラムに変換する関数Ｄを定義した。関数Ｄの正しさは、図１が変換可能であることを示すことにより証明された。これにより、プログラムを、命令型言語（imperative
language）から宣言型言語（declarative language）へ形式的に変換することに伴う問題が解決され、命令型言語から宣言型言語への機械的な変換が可能となる。
【図面の簡単な説明】
【０１４１】
【図１】本発明の数６６に係り、変換関数Ｄがプログラムの意味論を変更しないことを示すための図である。
【符号の説明】
【０１４２】
Ｄ 変換関数
【特許請求の範囲】
【請求項１】
コンピュータ用の命令型言語Ｌ１で表された所定のプログラムＰ中の変数Ｖ（Ｐ） を定義する第１のステップであって、該Ｐは一群の単語定義によって特定され、該単語定義の各々は一意的な単語に関するものである第１のステップと、
所定の構文法及び意味論に基づいて、前記Ｐ中の演算式もしくは論理式であるｅを置換する第２のステップと、
前記プログラムＰの各単位を対応する演算式もしくは論理式である式ｅに変換するための関数Ｄを、前記Ｖ（Ｐ）、ｅ、前記所定の構文法及び意味論に基づいて規定する第３のステップと、
所定の規則に基づき、前記第３のステップで規定された関数Ｄを変換して宣言型言語Ｌ２で表されるプログラムＰ２を生成する第４のステップと
を具備することを特徴とするプログラムの変換方法。
【請求項１】
コンピュータ用の命令型言語Ｌ１で表された所定のプログラムＰ中の変数Ｖ（Ｐ） を定義する第１のステップであって、該Ｐは一群の単語定義によって特定され、該単語定義の各々は一意的な単語に関するものである第１のステップと、
所定の構文法及び意味論に基づいて、前記Ｐ中の演算式もしくは論理式であるｅを置換する第２のステップと、
前記プログラムＰの各単位を対応する演算式もしくは論理式である式ｅに変換するための関数Ｄを、前記Ｖ（Ｐ）、ｅ、前記所定の構文法及び意味論に基づいて規定する第３のステップと、
所定の規則に基づき、前記第３のステップで規定された関数Ｄを変換して宣言型言語Ｌ２で表されるプログラムＰ２を生成する第４のステップと
を具備することを特徴とするプログラムの変換方法。
【図１】
【公開番号】特開２００８−９４６３（Ｐ２００８−９４６３Ａ）
【公開日】平成２０年１月１７日（２００８．１．１７）
【国際特許分類】
【外国語出願】
【出願番号】特願２００４−２８０５５８（Ｐ２００４−２８０５５８）
【出願日】平成１６年９月２７日（２００４．９．２７）
【出願人】（３９６０２３３６２）カテナ株式会社 (11)
【Ｆターム（参考）】
【公開日】平成２０年１月１７日（２００８．１．１７）
【国際特許分類】
【出願番号】特願２００４−２８０５５８（Ｐ２００４−２８０５５８）
【出願日】平成１６年９月２７日（２００４．９．２７）
【出願人】（３９６０２３３６２）カテナ株式会社 (11)
【Ｆターム（参考）】
[ Back to top ]