(57)【要約】プロセス代数を用いて、ソフトウェアの自動生成プロセス及びＬｙｅｅにより生成したソフトウェアの意味論を形式化する。  本発明は、１つのプログラムとして実装するユーザ要件を、論理体ごとに、該論理体上の単語ごとに、単語名、定義式、該定義式の実行条件、入出力属性、単語の値の属性によって宣言（規定）する第１のステップと、単語単位の宣言から、Ｌｙｅｅ計算法による入出力チャネルをそなえたプロセス・セルとしてモジュール化された論理要素（Ｌ２、Ｌ３、Ｌ４）および、作用要素（Ｉ２、Ｏ４、Ｓ４）を作成する第２のステップと、前記論理要素と作用要素を、同一画面からのコマンドで相互作用を起こすことを集合条件とする集合に集合化する第３のステップと、前記集合ごとに、１つの制御関数モジュールΦを配置する第４のステップと、前記プログラムに１つの制御関数モジュールΨを配置する第５のステップとを具備する。【特許請求の範囲】
【請求項１】
１つのプログラムとして実装するユーザ要件を、論理体ごとに、該論理体上の単語ごとに、単語名、定義式、該定義式の実行条件、入出力属性、単語の値の属性によって宣言（規定）する第１のステップと、
単語単位の宣言から、Ｌｙｅｅ計算法による入出力チャネルをそなえたプロセス・セルとしてモジュール化された論理要素（Ｌ２、Ｌ３、Ｌ４）および、作用要素（Ｉ２、Ｏ４、Ｓ４）を作成する第２のステップと、
前記論理要素と作用要素を、同一画面からのコマンドで相互作用を起こすことを集合条件とする集合に集合化する第３のステップと、
前記集合ごとに、１つの制御関数モジュールΦを配置する第４のステップと、
前記プログラムに１つの制御関数モジュールΨを配置する第５のステップと
を具備することを特徴とするソフトウェア生成方法。
【発明の詳細な説明】
【技術分野】
【０００１】  本発明は、ソフトウェア生成方法に係り、特に、Ｌｙｅｅ方法論におけるプロセス代数による形式化を用いたソフトウェア生成方法に関する。
【背景技術】
【０００２】  ここ数年の間に、ソフトウェアの開発ライフサイクルに関連する１つまたは多くの局面を改善するために種々の方法論および技術が考案され提案されてきた。しかし、この研究分野における熱心な努力にもかかわらず、明快に理解でき、修正可能なシステムの製造は、いまだに野心的目標であり達成するにはほど遠い。その理由の１つは、ソフトウェア自身が複雑なものであり、捕らえにくいものであるからであり、もう１つの理由は、現在の方法論に限界があるからである。最近、Ｌｙｅｅ（商標）と呼ばれる新しく、非常に有望な方法論が提案された。異なる分野に関連する広い範囲のソフトウェアの問題を効率的に処理することを目的としたＬｙｅｅにより、その要件を定義するだけでソフトウェアを開発することができるようになった。【０００３】  しかし、Ｌｙｅｅにより生成されたソフトウェアの意味論も、要件からのソフトウェア自動生成プロセスも、形式的でない言語で説明されるので、この方法論を理解し研究しようとすると、難しく、混乱が生じる恐れがある。
【非特許文献１】ジェイ・エイ・ベルグストゥラ、ジェイ・ダブリュ・クロップ（Ｊ．Ａ．Ｂｅｒｇｓｔｒａ  ａｎｄ  Ｊ．Ｗ．Ｋｌｏｐ）著、「抽象化を用いたコミュニケーション・プロセスの代数」、１９８５年，理論コンピュータ科学、３７（１）、ｐ．７７−１２１
【非特許文献２】ジー・ベリー、ジー・バウドル（Ｇ．Ｂｅｒｒｙ  ａｎｄ  Ｇ．Ｂｏｕｄｏｌ）著、「化学抽象機械」、１９９２年，理論コンピュータ科学、９６（１）、ｐ．２１７−２４８
【非特許文献３】シー・エー・アール・ホーア（Ｃ．Ａ．Ｒ．Ｈｏａｒｅ）著、「コミュニケーティング順次プロセス」、プレンティス・ホールコンピュータ科学国際シリーズ、プレンティス・ホール出版、１９８５年
【非特許文献４】エム・メジリ、ビー・クタリ、エム・アーヒオウイ（Ｍ．Ｍｅｊｒｉ，Ｂ．Ｋｔａｒｉ，ａｎｄ  Ｍ．Ｅｒｈｉｏｕｉ）著、「Ｌｙｅｅ指向ソフトウェアについての静的分析」、パリにおけるＬｙｅｅ方法論に関する第１回国際ワークショップ予稿集、ハミド・藤田、ポウル・ジョナネッセン編「ソフトウェア方法論、ツール及び技術における新潮流」ｐ．３７５−３９４、アイオーエス出版、２００２年
【非特許文献５】アール・ミルナー（Ｒ．Ｍｉｌｎｅｒ）著、「コミュニケーション・システムの計算法」、コンピュータ科学９２講義録、ベルリン、１９８０年、スプリンガー・フェアラーク出版
【非特許文献６】根来文生著、「Ｌｙｅｅソフトウェアの原理」、２１世紀の情報科学についての国際会議２０００（ＩＳ２０００）、ｐ．１２１−１８９、２０００年１１月
【非特許文献７】根来文生著、「Ｌｙｅｅ入門」、ソフトウェア生産技術研究所、東京、日本、２００１年
【非特許文献８】根来文生、アイ・ハミド（Ｉ．Ｈａｍｉｄ）著、「意思工学の提案」、データベースと情報システムに関する第５回東ヨーロッパ会議研究（ＡＤＢＩＳ’２００１）、２０００年９月
【非特許文献９】根来文生、アイ・ハミド（Ｉ．Ｈａｍｉｄ）著、「意思工学の提案」、インターネット上の電子商取引、科学及び教育の基盤における進歩に関する国際会議（ＳＳＧＲＲ２００１）、２００１年
【発明の開示】
【発明が解決しようとする課題】
【０００４】  本発明の主な目的は、第１に、プロセス代数を用いて、Ｌｙｅｅにより生成したソフトウェアの意味論とソフトウェアの自動生成プロセスを形式化することである。実際、プロセス代数は、本質的にＬｙｅｅ方法論の多くの概念を裏付けるので、従ってＬｙｅｅ方法論を簡潔かつ巧みに形式化する。そして、第２の目的は、プロセス代数は、フォン・ノイマンのものより、より適した抽象機械をＬｙｅｅ方法論に提供することである。実際、この新しい抽象機械は、プログラムを化学溶液と見なし、そこでは、分子（Ｌｙｅｅ方法論の異なるベクトル）が共通の目的を達成するために相互に作用しあっている。
【課題を解決するための手段】
【０００５】  かかる課題を解決するために本発明は、１つのプログラムとして実装するユーザ要件を、論理体ごとに、該論理体上の単語ごとに、単語名、定義式、該定義式の実行条件、入出力属性、単語の値の属性によって宣言（規定）する第１のステップと、単語単位の宣言から、Ｌｙｅｅ計算法による入出力チャネルをそなえたプロセス・セルとしてモジュール化された論理要素（Ｌ２、Ｌ３、Ｌ４）および、作用要素（Ｉ２、Ｏ４、Ｓ４）を作成する第２のステップと、前記論理要素と作用要素を、同一画面からのコマンドで相互作用を起こすことを集合条件とする集合に集合化する第３のステップと、前記集合ごとに、１つの制御関数モジュールΦを配置する第４のステップと、前記プログラムに１つの制御関数モジュールΨを配置する第５のステップとを具備する。【０００６】  本発明の異なる実施体としての「開発対象のソフトウェア」を生産するためのプログラム（ソフトウェア）、プログラム生成装置、プログラム処理装置、ツール（装置として或いはソフトウェアとしての双方を含む）、ソフトウェア開発装置、ソフトウェア開発支援装置、ソフトウェア開発管理装置は、Ｌｙｅｅ計算法による入出力チャネルをそなえたプロセス・セルとしてモジュール化された論理要素（Ｌ２、Ｌ３、Ｌ４）および、作用要素（Ｉ２、Ｏ４、Ｓ４）のひな型の未定義部分に、１つのプログラムとして実装するユーザ要件を、論理体ごとに、該論理体上の単語ごとの、単語名、定義式、該定義式の実行条件、入出力属性、単語の値の属性からなる宣言として情報化した情報を挿入する、宣言情報挿入手段と、前記論理要素と作用要素を、同一画面からのコマンドで相互作用を起こすことを集合条件とする集合単位に、１つの制御関数モジュールΦを、前記単位を制御するように関連づける、制御関数Φ配置手段と、１つの制御関数モジュールΨを、前記制御関数Φを制御するように前記制御関数Φに関連づける、制御関数Ψ配置手段とを具備するように構成することもできる。【０００７】  本発明はさらに、上述の「開発対象のソフトウェアを生産する方法」によって生産されたソフトウェア、及び当該ソフトウェアが搭載された記録媒体或いは当該ソフトウェアが搭載された装置（ハードウェア）としても実現されるが、この場合の本発明は、１つのプログラムとして実装するユーザ要件を、論理体ごとに、該論理体上の単語ごとの、単語名、定義式、該定義式の実行条件、入出力属性、単語の値の属性からなる宣言として情報化した情報を、Ｌｙｅｅ計算法による入出力チャネルをそなえたプロセス・セルとしてモジュール化された論理要素（Ｌ２、Ｌ３、Ｌ４）および、作用要素（Ｉ２、Ｏ４、Ｓ４）のひな型の未定義部分に挿入したモジュール群と、前記モジュール群を、同一画面からのコマンドで相互作用を起こすことを集合条件とする集合単位に、１つの制御関数モジュールΦで制御するように関連づけている１つまたは複数の制御関数モジュールΦと、前記制御関数Φを、１つの制御関数モジュールΨで制御するように関連づけている制御関数モジュールΨで構成されることもできる。【０００８】  またさらに本発明は、上述の「開発対象のソフトウェアを生産する方法」によってソフトウェアを生産するために用い��れるソフトウェアコードの雛型としてのソフトウェア、及び当該ソフトウェアが搭載された記録媒体或いは当該ソフトウェアが搭載された装置（ハードウェア）としても実現されるが、この場合の本発明は、１つのプログラムとして実装するユーザ要件を、論理体ごとに、該論理体上の単語ごとの、単語名、定義式、該定義式の実行条件、入出力属性、単語の値の属性からなる宣言として情報化した情報を、埋め込むべき未定義部分を有した、Ｌｙｅｅ計算法による入出力チャネルをそなえたプロセス・セルとしてモジュール化された論理要素（Ｌ２、Ｌ３、Ｌ４）および、作用要素（Ｉ２、Ｏ４、Ｓ４）のひな型と、前記宣言の情報を未定義部分に挿入した前記論理要素と作用要素を、同一画面からのコマンドで相互作用を起こすことを集合条件とする集合単位に、１つの制御関数モジュールΦで制御するための機能を有した制御関数モジュールΦのひな型と、前記制御関数Φを１つの制御関数モジュールΨで制御するための機能を有した制御関数モジュールΨのひな型とを備えるソフトウェアとしてコード化可能なひな型として実現してもよい。【０００９】  さらに、本発明は、上述の「開発対象のソフトウェアを生産する方法」による、要件から抽出した情報（ドキュメント（紙、データ））の抽出方法として、またかかる抽出方法によって抽出された情報（ドキュメント（紙、データ））として、さらには当該抽出された情報の使用方法として、或いは、これらの情報が搭載された情報記録媒体として、または情報の抽出方法／使用方法がコード化されたソフトウェア、当該ソフトウェアが搭載された記録媒体／装置（ハードウェア）として、いずれも実現することができるが、この場合の本発明は、Ｌｙｅｅ計算法による入出力チャネルをそなえたプロセス・セルとしてモジュール化された論理要素（Ｌ２、Ｌ３、Ｌ４）および、作用要素（Ｉ２、Ｏ４、Ｓ４）のひな型の未定義部分に挿入すべき、１つのプログラムとして実装するユーザ要件を、論理体ごとに、該論理体上の単語ごとの、単語名、定義式、該定義式の実行条件、入出力属性、単語の値の属性からなる宣言として情報化した情報と、前記宣言の情報を未定義部分に挿入した前記論理要素と作用要素を、同一画面からのコマンドで相互作用を起こすことを集合条件とする集合単位に、１つの制御関数モジュールΦで制御するように関連づけるための情報と、前記制御関数Φを１つの制御関数モジュールΨで制御するように関連づける情報とを備えるソフトウェア開発要件から抽出した情報として実現してもよい。【００１０】  なお、論理体については、同一出願人による特願２００４−２７２４００を参照し、これを引用し、開示の一部とする。
【発明の効果】
【００１１】  異なる分野に関連する広範囲のソフトウェアの問題を効率的に処理し、従来の方法論と比較した場合には、Ｌｙｅｅを使用すると開発時間、保守時間およびドキュメント量はかなり少なくなる（７０〜８０％程度）。
【発明を実施するための最良の形態】
【００１２】Ｌｙｅｅ方法論：プロセス代数による形式化
概要：ここ数年の間に、ソフトウェアの開発ライフサイクルに関連する１つまたは多くの局面を改善するために種々の方法論および技術が考案され提案されてきた。しかし、この研究分野における熱心な努力にもかかわらず、明快に理解でき、修正可能なシステムの製造は、いまだに野心的目標であり達成するにはほど遠い。その理由の１つは、ソフトウェア自身が複雑なものであり、捕らえにくいものであるからであり、もう１つの理由は、現在の方法論に限界があるからである。最近、Ｌｙｅｅと呼ばれる新しく、非常に有望な方法論が提案された。異なる分野に関連する広い範囲のソフトウェアの問題を効率的に処理することを目的としたＬｙｅｅにより、その要件を定義するだけでソフトウェアを開発することができるようになった。【００１３】  しかし、Ｌｙｅｅにより生成されたソフトウェアの意味論も、要件からのソフトウェア自動生成プロセスも、形式的でない言語で説明されるので、この方法論を理解し研究しようとすると、難しく、混乱が生じる恐れがある。【００１４】  本発明の主な目的は、第１に、プロセス代数を用いて、Ｌｙｅｅにより生成したソフトウェアの意味論とソフトウェアの自動生成プロセスを形式化することである。実際、プロセス代数は、本質的にＬｙｅｅ方法論の多くの概念を裏付けるので、従ってＬｙｅｅ方法論を簡潔かつ巧みに形式化する。そして、第２の目的は、プロセス代数は、フォン・ノイマンのものより、より適した抽象機械をＬｙｅｅ方法論に提供することである。実際、この新しい抽象機械は、プログラムを化学溶液と見なし、そこでは、分子（Ｌｙｅｅ方法論の異なるベクトル）が共通の目的を達成するために相互に作用しあっている。
１．始めに
高い品質を持つソフトウェアを容易に迅速に製造することは、ソフトウェア開発研究分野の基本的な関心事である。ここ数年にわたって、ソフトウェアの開発ライフサイクルに関連する１つまたは多くの局面を改善するために、種々の方法論および技術が考案され提案されてきた。しかし、この研究分野における熱心な努力にもかかわらず、明快に理解でき、修正可能なシステムの製造は、いまだに野心的目標であり達成するにはほど遠い。その理由の１つは、ソフトウェア自身が複雑なものであり、捕らえにくいものであるからであり、もう１つの理由は、現在の方法論に限界があるからである。実際、提案されたほとんどすべての方法論は、明快に理解でき、修正可能なシステムの製造に失敗しており、その使用は、いまだに非常に広範囲の能力、技術および知識を持つ専門家だけが可能なことだと見なされている。そのため、人件費や維持費が高いものになり、ソフトウェアに対して広範なチェックが必要になる。これらの理由で、企業は、ソフトウェア開発サイクルにおける実証可能な改善を約束するすべての新しい方法論を歓迎する傾向にある。【００１５】  最近、Ｌｙｅｅ（「リー」と読む。「ｇｏｖｅｒｎｅｍｅｎｔａＬ  ｍｅｔｈｏｄｏｌｏｇＹ  ｆｏｒ  ｓｏｆｔｗａｒＥ  ｐｒｏｖｉｄｅｎｃＥ」の尾文字語）（非特許文献６、７、８、９参照）と呼ばれる新しく、非常に有望な方法論が提案された。異なる分野に関連する広範囲のソフトウェアの問題を効率的に処理することを目的としたＬｙｅｅにより、その要件を定義するだけでソフトウェアを開発することができる。もっと正確に言えば、開発者は、単語、計算式、計算条件（前提条件）および画面と帳票のレイアウトを与えさえすれば、後は、コンピュータが、以降のすべての面倒なプログラミング・プロセス（例えば、制御ロジックに関する局面など）をすべて行ってくれる。その新しさにもかかわらず、Ｌｙｅｅの使用結果は、Ｌｙｅｅには非常に多くの潜在的可能性があることを示している。実際、従来の方法論と比較した場合には、Ｌｙｅｅを使用すると開発時間、保守時間およびドキュメント量はかなり少なくなる（７０〜８０％程度）（非特許文献７参照）。非特許文献４において、この方法論の多くの、特にＬｙｅｅ要件の、局面を改善するために、我々は、いくつかの古典的静的分析技術を提案した。【００１６】  しかし、Ｌｙｅｅにより生成したソフトウェアの意味論も、要件からのソフトウェア自動生成プロセスも、形式的でない言語で説明されているので、この方法論を理解し研究しようとすると、難しく、混乱が生じる恐れがある。さらに、この方法論の背後にあるアイデアは、このようなアイデアをサポートするのに適当でない、逐次処理言語（ｓｅｑｕｅｎｔｉａｌ  ｌａｎｇｕａｇｅ）によって記述されている。実際、Ｌｙｅｅにより生成したソフトウェアは、基本的には、小さなコンポーネント（Ｌｙｅｅ用語でベクトル（ｖｅｃｔｏｒ）と呼ばれる）群からできている。ここでは、各コンポーネントはそれぞれのアトミック・ゴール（ａｔｏｍｉｃ  ｇｏａｌ：要素の目的）を持って相互作用によって互いに協力し合い、要求される結果（グローバル・ゴール（ｇｌｏｂａｌ  ｇｏａｌ：全体の目的））を生成する。一方、平行性（ｃｏｎｃｕｒｒｅｎｃｙ：複数の計算主体が互いに情報のやりとりを行いながら動作すること）および通信（ｃｏｍｍｕｎｉｃａｔｉｏｎ）をサポートするプロセス代数は、共同作用しあう（ｃｏｎｃｕｒｒｅｎｔ）コンポーネントを記述するのに本質的に適した言語であることはよく知られている。それ故、プロセス代数は、Ｌｙｅｅ方法論の概念をサポートするための、形式的で価値ある基礎を提供する。Ｌｙｅｅ方法論にプロセス代数を使用することによる数ある利点のなかには、Ｌｙｅｅの現実のバージョンにおける多くのコンポーネント（ベクトル全体またはベクトルの一部）は、もはや必要でなくなる、ということがある。これらのコンポーネントは、逐次処理言語によって記述されているがために、ある処理のまとまりの実行順序を制御するためにどうしても必要であったが、これらの役割は、プロセスの平行処理と通信をサポートするプロセス代数により、必然的にサポートされるからである。実際、経路作用要素（ｒｏｕｔｉｎｇ  ｖｅｃｔｏｒ）は、もはや必要ではなくなる。より小さく、処理時間がより短く、必要メモリがより少ないプログラムを生成する、シンプルなＬｙｅｅの形式的記述を手にすることができる。その上、この形式的記述は、この方法論のいろいろな局面の多くの興味ある分析に不可欠なスタート点になる。例えば、Ｌｙｅｅで生成したソフトウェア、またはソフトウェア生成プロセスを最適化するために、最適化されたプログラムが元のバージョンと同じものであるという形式的証拠を必要とする。プロセス代数を使用すれば、形式的に同じものであることのチェック、またはもっと一般的にモデル・チェックをうまく行うことができる。【００１７】  本稿においては、最初に、Ｌｙｅｅ方法論の基本的なコンセプトを容易かつ本質的（ｎａｔｕｒａｌｌｙ）にサポートする、Ｌｙｅｅ計算法（Ｌｙｅｅ−Ｃａｌｃｕｌｕｓ）と呼ぶ形式的プロセス代数（ｆｏｒｍａｌ  ｐｒｏｃｅｓｓ  ａｌｇｅｂｒａ）を定義する。実際に、この計算法は、フォン・ノイマン型（逐次処理型）の計算機より、Ｌｙｅｅ方法論の概念をサポートするのにより適した抽象機械（ａｂｓｔｒａｃｔ  ｍａｃｈｉｎｅ：計算機の概念を抽象化したもの）と見なすことができる。この機械は、プログラムを、最終結果を生成するために共に相互作用を行う分子の集合と見なす。第二に、この計算法が、どのようにして、Ｌｙｅｅコンポーネント（Ｌｙｅｅではベクトルと呼ぶ）とＬｙｅｅ方法論の全ソフトウェア生成プロセスの両方を形式化し、簡単にすることができるのかを示す。実際に、Ｌｙｅｅソフトウェア生成の自動生成全プロセスを形式化した。【００１８】  本稿の残りの部分は、下記のような構成になっている。セクション２において、Ｌｙｅｅ計算法の構文論（ｓｙｎｔａｘ）および意味論（ｓｅｍａｎｔｉｃｓ）を定義する。セクション３においては、Ｌｙｅｅ方法論の技術的紹介を行い、Ｌｙｅｅ計算法によるその形式化の全体像を紹介する。セクション４においては、Ｌｙｅｅ計算法によるＬｙｅｅ方法論の詳細かつ完全な形式化を提案する。セクション５においては、生成したプログラムの、実行段階毎の記述と一緒に、どのようにして簡単な要件からプログラムが自動的に生成されるのか、の両方を具体的に示す１つのケーススタディについて説明する。最後に、セクション６においては、この研究の結論を述べ、将来の研究のいくつかについて説明する。
２．Ｌｙｅｅ計算法
プロセス代数は、複雑なコンピュータ・システム、特に、通信し、平行に実行するコンポーネントを含むコンピュータ・システムのための形式的記述技術である（非特許文献１、３、５参照）。プロセス代数は、通常、文献で計算法（ｃａｌｃｕｌｕｓ）と呼ばれる。何故なら、プロセス代数は、プロセス代数の分野を超えて、種々の数学的および論理的概念（平行性理論（ｃｏｎｃｕｒｒｅｎｃｙ  ｔｈｅｏｒｙ）、動作意味論（ｏｐｅｒａｔｉｏｎａｌ  ｓｅｍａｎｔｉｃｓ）、複雑性理論（ｃｏｍｐｌｅｘｉｔｙ  ｔｈｅｏｒｙ）、ロジック等）を含んでいるからである。【００１９】  このセクションにおいては、Ｌｙｅｅ方法論を形式化するために特に定義したＬｙｅｅ計算法と呼ぶ新しい計算法の構文法および意味論について説明する。
２．１  構文法（Ｓｙｎｔａｘ）
Ｌｙｅｅ計算法プログラムは、指定されたチャネル上でハンドシェイク技術（ｈａｎｄ−ｓｈａｋｅ  ｔｅｃｈｎｉｑｕｅ：２つのプロセスの一方を受信可能状態に、他方を送信可能状態におくことによって通信させる技術）により通信（ｃｏｍｍｕｎｉｃａｔｅ）する独立した並行プロセスからなるシステムである。チャネルは、その上では特定のプロセスだけが通信することができるように制限できる。あるプロセスは、作用［？！ｅ］を行うことにより、チャネル？を通して値？を送ることができる（？は、式ｅの計算結果（ｖａｌｕａｔｉｏｎ））。同様に、あるプロセスは、作用［？？ｅ］を行うことにより、チャネル？から式ｅにの値？を受信することができる（？は、式ｅの計算に使用する値）。【００２０】  あるプロセスは、また、不作用作用（ｓｉｌｅｎｔ  ａｃｔｉｏｎ）τを行うこともできる。この特別な作用は、プロセス間の同期（ｓｙｎｃｈｒｏｎｉｚａｔｉｏｎ：プロセス間通信において、あるプロセスが値などを送信したと同時に、他のプロセスがそれを受信すること）のような、システム内部のふるまい（ｉｎｔｅｒｎａｌ  ｂｅｈａｖｉｏｒ）を表わすことを意図している。また、プロセスの進展における予見不能性（ｉｎｄｅｔｅｒｍｉｎｉｓｍ）、すなわち、複数のプロセスの選択肢があってどのプロセスが実行させれるか予測できないような場合（後述のプロセス構文法定義１の「選択」の説明を参照）、を捉えるために有益である。【００２１】  プロセスの構文法（ｓｙｎｔａｘ）を以下に定義する。
＜定義＜構文法１＞【００２２】
【数１】
2005029323.tif 000002
＜定義＜構文法２＞
Ｋ，Ｋ１，Ｋ２：：＝｛κ｝｜Ｋ１  ∪  Ｋ２
＜定義＜構文法３＞【００２３】
【数２】
2005029323.tif 000003
＜定義＜構文法４＞
κ：：＝？？！ｅ｜？？ｅ｜τ｜
上記の定義構文法に使われる記号の意味と、その直感的構文法の意味は下記のとおりである。
＜定義＜構文法１＞【００２４】
【表１】
2005029323.tif 000004
定義構文法１の直感的意味は次のとおりである。すなわち、プロセスＰとＱがあったとき、その関係や内容は、以下のいずれかとして定義される。すなわち、シーケンス（［Ｋ］．Ｐ）、並行構成（Ｐ｜Ｑ）、選択（Ｐ＋Ｑ）、条件付き選択（Ｐ＞Ｑ）、制限（Ｐ／Ｌ）、定義、無プロセス（ｎｉｌ）、のいずれかである。ここで、「定義」とは、【００２５】
【数３】
2005029323.tif 000005
のことで、記号の左辺は、右辺によって定義される。【００２６】  各構文の解釈については後述する。
＜定義＜構文法２＞【００２７】
【表２】
2005029323.tif 000006
定義構文法２の直感的意味は次のとおりである。すなわち、作用の集合Ｋ、Ｋ１、Ｋ２があるとき、その作用の集合は、１つの作用を要素とする集合（｛κ｝）、作用集合が結合した集合（Ｋ１  ∪  Ｋ２）、のいずれかである。
＜定義＜構文法３＞【００２８】
【表３】
2005029323.tif 000007
定義構文法３の直感的意味は、次のとおりである。すなわち、チャネルの集合Ｌ，Ｌ１，Ｌ２があるとき、そのチャネルの集合は、要素を持たない空集合（０）、１つのチャネルだけを要素とする集合（｛？｝）、チャネルの集合が結合した集合（Ｌ１∪Ｌ２）、のいずれかである。
＜定義＜構文法４＞【００２９】
【表４】
2005029323.tif 000008
定義構文法４の直感的意味は、次のとおりである。すなわち、作用κがあるとき、その作用は、チャネル？上で式ｅの計算結果の値を送信する送信作用（？！ｅ）、チャネル？上で式ｅの値を受信する受信作用（？？ｅ）、不作用作用（τ）、のいずれかである。【００３０】  定義構文法１に定義した、構文法の意味を詳しく説明する。
１）［Ｋ］．Ｐ：シーケンス（Ｓｅｑｕｅｎｃｅ）
プロセス［Ｋ］．Ｐは、作用の集合であるＫに属す全ての作用（ａｃｔｉｏｎ）、すなわち｛κ１，．．．，κｎ｝、を実行した後にＰとしてふるまうプロセスである。Ｋに属する作用を実行する順序は重要ではない。ここでは、説明を簡単にするために、［｛κ１，．．．，κｎ｝］と書く代わりに［κ１，．．．，κｎ］と書く。
２）Ｐ｜Ｑ：並行構成（Ｐａｒａｌｌｅｌ  ｃｏｍｐｏｓｉｔｉｏｎ）
プロセスＰ｜Ｑは、並行に実行されるプロセスＰおよびＱとしてふるまう。各プロセスは、両方が知っているチャネル上で互いに相互作用することができるし、または各プロセスが他方から独立して外部世界（システムの環境またはエンドユーザ）と相互作用（ｉｎｔｅｒａｃｔ）することもできる。同じチャネル上で２つのプロセスが同期する（ｓｙｎｃｈｒｏｎｉｚｅ：プロセス間通信において、あるプロセスが値などを送信したと同時に、他のプロセスがそれを受信する）と、プロセス全体は、作用τ（不作用作用）を実行し、その後、残りのプロセスとしてふるまう。具体的に、下記のプロセスの例で考えてみる。【００３１】                  Ｐ＝Ｐ１｜Ｐ２
Ｐ１およびＰ２を下記のように定義する。【００３２】
【数４】
2005029323.tif 000009
上記式の直感的意味は、
Ｐ１は、値４をチャネル？上に送信し、その後は、プロセスＰ１’としてふるまうプロセスである。Ｐ２は、チャネル？上に式ｘの値が与えられるのを待って、値が与えられたら受信し、その後は、プロセスＰ２’としてふるまうプロセスである。
従って、プロセスＰは、プロセスＰ１とＰ２が同期したとき（それは実際にはＰ１からの値４の送信と同時にＰ２による受信が行われることによる）、不作用作用τを実行し、その後は、残りのプロセスＰ１’｜Ｐ２’としてふるまう。意味論上、この遷移を下記のように表わす。【００３３】
【数５】
2005029323.tif 000010
この式の直感的意味は、プロセスＰにおける相互作用の結果、不作用作用τが実行され、プロセス全体が、並行プロセスＰ１’｜Ｐ２’に移行する、ということである。【００３４】  関係【００３５】
【数６】
2005029323.tif 000011
の形式的定義はこのセクションの後の方で示す。
３）Ｐ＋Ｑ：選択（Ｃｈｏｉｃｅ）
プロセスＰ＋Ｑは、プロセスＰまたはＱとしてふるまうプロセスである。ＰおよびＱのどちらもが、始まりが不作用作用であるような場合を除いて、どちらのプロセスが実行されるかの選択は、環境によって決定論的に決まる。一方、両方のプロセスが不作用作用で開始する場合には、選択は決定されない。
４）Ｐ＞
Ｑ：条件付き選択（Ｇｕａｒｄｅｄ  ｃｈｏｉｃｅ）：
プロセスＰ＞
Ｑは、プロセスＱが活性化（ａｃｔｉｖａｔｅｄ）されるまで、Ｐとしてふるまうプロセスである。後者Ｑが活性化されたときはいつでも、Ｐは停止し、メモリからクリアされる。
５）Ｐ／Ｌ：制限（Ｒｅｓｔｒｉｃｔｉｏｎ）
プロセスＰ／Ｌは、チャネルの集合Ｌに与えられたチャネルだけを使って環境と通信することができるプロセスＰ、としてふるまうプロセスである。
６）数３の記号：定義（Ｄｅｆｉｎｉｔｉｏｎ）
たとえば、数３の記号によって、下式のような定義ができる。【００３６】
【数７】
2005029323.tif 000012
数７の式において、Ａはプロセスの識別名、【００３７】
【数８】
2005029323.tif 000013
はプロセスＡの変数（パラメータ）で、左辺のプロセスは、右辺のプロセスＰに等しいと定義されている。プロセスＰは再起的にＡを含むことができる。
７）ｎｉｌ：無プロセス（ｎｉｌ  ｐｒｏｃｅｓｓ）：
どんな作用も実行できないプロセス、いいかえると終了しているプロセス（ｄｅａｄ  ｐｒｏｃｅｓｓ）である。あるプロセスが終了すると、通常ｎｉｌプロセスになる。終了してｎｉｌプロセスになったとき、そのプロセスはもはや起動して（ａｃｔｉｖａｔｅｄ）いないので、作用を実行する条件が整ったとしても、何の作用も実行できない。
２．２  例値を保持するプロセスのモデル化
このセクションにおいては、メモリという、値を保持するセル（ｃｅｌｌ）を、その通信チャネルを通して、その環境と相互作用を行うプロセスとしてモデル化する方法について説明する。図１に示すように、メモリ・セルは通信のための２つのポート（チャネル）ｉｎおよびｏｕｔを持つものと見なす。このメモリ・セルの基本的なタスクは、チャネルｉｎ上で値を無制限に待つことであり、チャネルｏｕｔ上でその値を利用可能にすることである。メモリ・セルは、新しい値がチャネルｉｎに入力されるまで、同じ値を必要な回数だけチャネルｏｕｔに出力することができる。チャネル自体は値を保持しない。【００３８】  メモリ・セルｘが値？を保持しているプロセス・セルＣｘ（？）は、下記のように表わす。【００３９】
【数９】
2005029323.tif 000014
この形式的記述の直感的意味は、値？を保持しているプロセスＣｘ（？）は、チャネルｉｎｘ上で式ｙの値を受信したときは、プロセスＣｘ（ｙ）としてふるまい（すなわち保持する値が？から式ｙの値に変更される）、保持している値？をチャネルｏｕｔｘ上に送信したときには、送信作用の後も値？を保持したままプロセスＣｘ（？）としてふるまうプロセスである。【００４０】  値を保持するメモリ・セルをプロセスとして捉えることにより、メモリ・セルにさらに知能を付加することができる。例えば、初期化される（初期値を受信する）までその内容にアクセスさせないセルを書くことができる。情報処理能力のあるこのスマート・セル（ｓｍａｒｔ  ｃｅｌｌ）は、下記のように定義することができる。【００４１】
【数１０】
2005029323.tif 000015
プロセスＣｅｌｌ（ｘ）は、チャネルｉｎｘ上で式ｙの値を受信した後、式ｙの値を保持するプロセスＣｘ（ｙ）としてふるまうプロセスである（式ｙに値を受信し、式ｙの値を保持するプロセスで、送信は行わない）。【００４２】  ここで、下記のように定義した２つのプロセスについて考えてみる。【００４３】
【数１１】
2005029323.tif 000016
プロセスＰ１は、チャネルｉｎｘ上に値５を送信し、ｎｉｌになる（終了する）プロセスである（値５を送信するプロセス）。プロセスＰ２は、チャネルｏｕｔｘ上で式ｙの値を受信した後にｎｉｌになる（終了する）プロセスである（数式ｙに値を受信するプロセス）
これらの２つのプロセスが、セルｘ（Ｃｘ）を通して通信するようなプログラムを書くことが容易にできる。【００４４】              Ｐ１｜Ｃｅｌｌ（ｘ）｜Ｐ２
このプログラムは、プロセスＰ１、プロセスＣｅｌｌ（ｘ）、プロセスＰ２が並行に実行されるプログラムである。【００４５】  図２は、上記に含まれる全てのプロセス間の相互作用を示したものである。【００４６】  このプログラムの実行における、個々のステップの詳細は以下のようになる。【００４７】
【数１２】
2005029323.tif 000017
上記の式の意味を直感的に表わせば、プロセスＰ１｜Ｃｅｌｌ（ｘ）｜Ｐ２は、以下の第１ステップと第二ステップを経て実行される。（等号記号で記載される右辺が１つのステップである）下線は相互作用（同期）を起こす送受信作用を示している。
＜第１ステップ＞
（１）［ｉｎｘ！５］．ｎｉｌ（チャネルｉｎｘに値５送信）、（２）［ｉｎｘ！５］．Ｃｘ（ｙ）（チャネルｉｎｘで式ｙに与える値を受信し、受信後はセルｘに式ｙの値を保持）、（３）［ｏｕｔｘ？ｙ］．ｎｉｌ（チャネルｏｕｔｘで式ｙの値を受信）、の３つのプロセスが並行に行われた結果、
（１）がチャネルｉｎｘに値５を送信完了し、同時に（２）がチャネルｉｎｘで値５を受信する、というプロセス間の相互作用（同期）が起こって、
不作用作用τが実行され、
（４）Ｃｘ（５）（セルｘに値５を保持）、と（３）［ｏｕｔｘ？ｙ］．ｎｉｌ（チャネルｏｕｔｘで式ｙの値を受信）、の２つのプロセスの並行プロセスに移行する。
＜第２ステップ＞
前述の数１−１９の定義から、（４）Ｃｘ（５）は選択プロセス（４）−１（［ｉｎｘ？ｙ］．Ｃｘ（ｙ）＋［ｏｕｔｘ？？］．Ｃｘ（？））に置き換えることができる。
すなわち、
プロセス（４）−１と、（３）が並行に行われた結果、
（４）−１の［ｏｕｔｘ？？］．Ｃｘ（？）（チャネルｏｕｔｘに値５を送信）と同時に（３）の（チャネルｏｕｔｘで式ｙの値５を受信）が起こる、という相互作用（同期）が起こって、
不作用作用τが実行され、
その結果、残りのプロセスはＣｘ（５）（セルｘに値５を保持）としてふるまわれる。
２．３  意味論
以下に、Ｌｙｅｅ計算法の形式的意味論について説明する。この意味論は、相互作用関係【００４８】
【数１３】
2005029323.tif 000018
により定義される。この時、演算子→は「関係」（ｒｅｌａｔｉｏｎ）を表わし、κは作用を表わす。「関係」は複数の「関係」の集合であり、その集合要素である１つ１つの「関係」は次の３つの要素で構成されている。第１の要素は「変化前のプロセス」、第２の要素は「変化の後のプロセス」、第３の要素は「変化の間に実行された作用」である。【００４９】
【数１４】
2005029323.tif 000019
と書くとき、関係→の３要素は（Ｐ，Ｑ，Ｋ）である。【００５０】  上記のように定義するとき、数１４の意味は、サブプロセスＰの中の相互作用（ｒｅａｃｔｉｏｎ）によって、全体プロセスがアトミック・アクション（ａｔｏｍｉｃ  ａｃｔｉｏｎ；割込みを許さない一連の不可分な作用で、次の別の作用を開始させるために、必ず完了されなければならない）κを実行してサブプロセスＱとなる、ことを意味する。相互作用関係（ｉｎｔｅｒａｃｔｉｏｎ  ｒｅｌａｔｉｏｎ）とういう着想は、ベリー（Ｂｅｒｒｙ）およびバウドル（Ｂｏｕｄｏｌ）（非特許文献２参照）の化学抽象機械（Ｃｈｅｍｉｃａｌ  Ａｂｓｔｒａｃｔ  Ｍａｃｈｉｎｅ）によって触発されたものである。このモデルでは、プロセスは、相互作用を起こすことを待っている分子の化学溶液であると見なしている。【００５１】  数式１３の関係を形式的に表わすために、下記の概念を定義する必要がある。
・【００５２】
【数１５】
2005029323.tif 000020
は、プロセスを簡単にするために用いる記号で、左辺が、簡素化されたプロセスである右辺と等しいことを表わす。下記に示すように、無プロセスを除去することによりプロセスを簡単にすることができる。【００５３】
【数１６】
2005029323.tif 000021
式ｅの計算結果である値の集合を【００５４】
【数１７】
2005029323.tif 000022
で示す。ｅが変数である場合には、その計算結果の値の変域も、その変数の変域（ｄｏｍａｉｎ）（整数、実数等）と同じである。説明を簡単にするために、すべての変数は実数の集合に属するものと見なす。【００５５】
【数１８】
2005029323.tif 000023
は、作用κが使用するチャネルの名前である。たとえば、【００５６】
【数１９】
2005029323.tif 000024
の意味は次の通り：
不作用作用τが使用するチャネルは存在しないので、空集合（０）である。
送信作用（？！ｅ）と受信作用（？？ｅ）が使用するチャネルは、？である。【００５７】  「関係」の集合（→）は、要素として、表５に示す１５個の規則を満足させるような「関係」を最小数持つ「関係」である。【００５８】  かっこ内ないに示した各種のＲ記号は、規則名を示す記号である。規則は、前提条件と結果からなっており、各規則は、横線の上段に示される条件のとき、下段に示した結果になるような規則である。【００５９】
【表５】
2005029323.tif 000025
たとえば、第２番目の規則（Ｒ！）の意味は以下のとおりである：
値？が式ｅの値の集合に属すとき（上段の前提条件が成立するとき）、チャネル？上に式ｅの値を送信後、プロセスＰとなる［？！ｅ］．Ｐは、チャネル？上への値？送信作用が起こった後、プロセスＰに移行する（下段の結果）。
３．Ｌｙｅｅ要件の非形式的形式化
このセクションにおいては、Ｌｙｅｅ方法論が、どのようにして基本的なユーザ要件からソフトウェアを生成するのか、その全体像について説明する。加えて、この全体像から、Ｌｙｅｅ計算法によってこの方法論をどのようにして簡単かつ効率的に形式化することができるのかを順次紹介する。Ｌｙｅｅ方法論のソフトウェア生成プロセスの完全な形式化については、次のセクションで説明する。
３．１  Ｌｙｅｅ要件
Ｌｙｅｅ方法論において、要件は、宣言的な方法で、単語名、その定義式、その計算条件、およびその属性（入出力、タイプ、セキュリティタイプ等）という要素を含む宣言の集合として与えられる。表６は、Ｌｙｅｅ要件の一例である。【００６０】  「Ｗｏｒｄ」は単語名、「Ｄｅｆｉｎｉｔｉｏｎ」は単語の値を生成するための定義式、Ｃｏｎｄｉｔｉｏｎは定義式を実行する計算条件、「ＩＯ」は単語の値の入出力の属性を示す。ＯＦはファイルへの出力、ＯＳは画面への出力、ＩＳは画面からの入力、ＩＦはファイルからの入力（表にはない）、を表わす。「Ｔｙｐｅ」は、値の属性で、ｉｎｔは整数（ｉｎｔｅｇｅｒ）、ｆｌｏａｔは不動小数点数を表わす。「Ｓｅｃｕｒｉｔｙ」は、値のセキュリティに関する属性を表わす。ｓｅｃｒｅｔは非公開、ｐｕｂｌｉｃは公開、を表わす。【００６１】
【表６】
2005029323.tif 000026
表６の要件は、感覚的にとらえれば、従来のプログラミング言語の表７のコードに対応する。Ｓａは、単語ａの宣言を意味する。【００６２】
【表７】
2005029323.tif 000027
たとえば、単語ａの宣言Ｓａのコードは、
「もし、ｂ＊ｅ＞２が真ならば、単語ａにｂ＋ｃの計算結果を代入し、単語ａの値を出力」、を意味している。【００６３】  宣言Ｓｃのコードは、「単語ｃに値を入力」、を意味している。【００６４】  Ｌｙｅｅ方法論においては、ユーザは、これらの定義が実行される順序（制御ロジック）を指定する必要はない。表７に示すように、単語ａの定義は、単語ｂを使用しているにもかかわらず、宣言Ｓｂは、宣言Ｓａの後に位置している。以下に説明するように、これらの要件から、また、宣言の順序とは無関係に、Ｌｙｅｅはすべての定義した単語を計算するコードを生成することができる。このシンプルなアイデアは、非特許文献６、７、８、９に示されるように、ソフトウェア開発上の異なるステップにおいて、数々の有利な結果を生む。実際、このアイデアを使用することにより、要件が不完全であってもソフトウェアの開発をスタートすることができる。さらに、ユーザは、もっと古典的な方法論の場合のように、単語の実行順序の制御ロジックの問題を扱う必要がない。ソフトウェアの制御ロジック部分は、Ｌｙｅｅ方法論においては、自動的に生成され、その結果、プログラミング・エラーが低減し、プログラミング時間が短縮される。柔軟性も、Ｌｙｅｅ方法論の主要な利点である。何故なら、保守業務を、要件の簡単な修正（単語の定義の追加、削除および／または修正）作業にまで軽減できるからである。【００６５】  従って、Ｌｙｅｅシステムは、求められる結果を生成するために共に相互作用を行う独立したコンポーネント（宣言）の集合体と見なすことができる。本論のプロセス代数の概念は、この見方と非常によく一致する。何故なら、Ｌｙｅｅ計算法は、プログラムを、最終目的に到達するために、共に相互作用しあう分子（プロセス）の化学溶液と見なすからである。それ故、一見して、宣言の集合｛ｓ１，．．．，ｓｎ｝からなるＬｙｅｅ要件ＬＲを、Ｌｙｅｅ計算法の並行プロセス（ｃｏｎｃｕｒｒｅｎｔ  ｐｒｏｃｅｓｓ）として見ることができる。すなわち、次に表わすとおりである。【００６６】              ＬＲ＝ｓ１｜．．．｜ｓｎ
直感的説明によれば、要件ＬＲは、プロセスｓ１、．．．、ｓｎが並行に実行されるプロセスである。
３．２  パレット（Ｐａｌｌｅｔ）および基本構造（Ｓｃｅｎａｒｉｏ  Ｆｕｎｃｔｉｏｎ）
表６の要件から、ａおよびｂの値を計算し、それらを出力するプログラムを、自動的に生成することができる。このプログラムは、不動点（ｆｉｘｅｄ  ｐｏｉｎｔ）に達するまで、すなわち、図３に示されるように、繰り返し処理がいかなる単語の値も変えなくなるまで、これらの命令の実行を単純に反復する。【００６７】  プロセス代数の観点からいうと、「不動点に達する」という概念は、当然意味規則に組み込まれる。実際に、プロセス（分子）は、いかなる進展も可能でなくなる状態（不動点）に達するまで、共に相互作用する。【００６８】  要件からＬｙｅｅにより自動的に生成されるプログラムの構造および内容についてさらに正確に説明する。Ｌｙｅｅ方法論においては、表６に示すような宣言の集合の実行は特定の方法により行われる。実際は、Ｌｙｅｅは、図４に示すように、Ｌｙｅｅ用語で、パレット（Ｗ０２，Ｗ０３およびＷ０４）と呼ばれる３つの領域上に宣言に関連するコードを分配する。
パレットＷ０２：
入力単語を処理する。
パレットＷ０３：
単語の計算条件を計算し、結果をブール型（真偽値を値としてもつ）の変数で保存する。例えば、単語ａの定義の中で使用されている計算条件「ｂ＊ｅ＞２」はＷ０３で計算され、真／偽の結果は、別の変数「ａ＿ｃｏｎｄ」に保存される。
パレットＷ０４：
要件に含まれるその定義式によって単語の計算を行う。パレットＷ０４は、また、計算した単語の値を出力する。【００６９】  Ｌｙｅｅプログラムは、パレットＷ０４からスタートして、不動点に達するまで、すべての定義した単語の値を計算しようとする。単語の値の計算に係わるＷ０４内に進展が見られなくなると、経路作用要素Ｒ４によりパレットＷ０２に制御が与えられる。今度は、この第２のパレットが、単語の値の入力を繰り返し、不動点に達した（他に新たな入力対象がなくなった）とき、次に、経路作用要素Ｒ２が制御をパレットＷ０３に渡す。最後に、そしてパレットＷ０４と同じように、パレットＷ０３が、不動点に達するまで、要件に従って単語の計算条件を計算しようとする。図５に示すように、この全プロセス（Ｗ０４→Ｗ０２→Ｗ０３）は、全体が安定状態に達するまで繰り返され、連結されている３つのパレットは基本構造（Ｓｃｅｎａｒｉｏ  Ｆｕｎｃｔｉｏｎ）と呼ばれる。【００７０】  Ｌｙｅｅ要件を組み込むために逐次処理言語を使用することによって、Ｌｙｅｅ方法論の作者は、パレットが実行される順序、同じパレット内のベクトル（モジュール）が実行されるべき順序、およびあるベクトルから他のベクトルに制御を渡す方法を明確に指定せざるをえなかった。言い換えれば、この逐次処理言語がゆえに、Ｌｙｅｅ方法論の基本概念に属さない、また、この方法論をかなり複雑にしてきたいくつかの局面がもたらされることになった。すなわち、各パレット内のベクトルが実行される繰り返しの制御、パレットから他のパレットに実行を移す（異なる基本構造間を含め）方法および時期等を指定するという必要があった。これらのために、パレット関数（パレット内の実行制御）、経路作用要素（次に実行するパレットの決定）、パレット連鎖関数（パレット間の実行制御）が設置されていた。【００７１】  しかし、Ｌｙｅｅ計算法を使用することにより、パレットが実行される順序、各パレットのベクトルが実行される順序、パレットから他のパレットに制御を渡す方法および時期等を指定する必要がもはやなくなる。このような詳細は、当然ながら本論の抽象機械Ｌｙｅｅ計算法により本質的に管理される。それ故、基本構造は、下式のように形式化することができる。【００７２】              ＳＦ＝Ｗ０４｜Ｗ０３｜Ｗ０２
すなわち、基本構造ＳＦのプロセスは、Ｗ０４、Ｗ０３、Ｗ０２の３つのパレットのプロセスの並行プロセスである。【００７３】  Ｗ０４、Ｗ０３およびＷ０２を実行する順序はもはや重要ではなくなり、これらパレットを接続している経路作用要素も除去されていることに留意されたい。【００７４】  Ｌｙｅｅは、固定構造を持つ簡潔なプログラム（Ｌｙｅｅ用語で述語ベクトル（ｐｒｅｄｉｃａｔｅ  ｖｅｃｔｏｒ）と呼ばれる）を確立した。この構造により、生成されたコードの構造は不変かつ要件の内容に依存しないものになっている。ベクトルの実行を制御する統括プログラム（ｇｌｏｂａｌ  ｐｒｏｇｒａｍ）であるパレット関数の役割は、単に述語ベクトルを呼び出すだけである。図６は、述語ベクトルの構造を示す。【００７５】  述語ベクトルの目的は、各パレットにより異なる。
＜パレットＷ０４＞
パレットＷ０４の第１の目的は、定義式により単語に値を与えることである。この役割を行う述語ベクトルをＬ４と呼ぶ。図４の例における単語ａおよび単語ｂのＬ４は、図７に示すようになる。【００７６】  単語の計算に進展がなくなり、かつ、単語の値が全て成立すると、Ｌｙｅｅの生成コードは、次の目的となる単語の出力を実行しようとする。値を出力するという目的を持つ述語ベクトルは、出力作用要素（Ｏｕｔｐｕｔ  Ｖｅｃｔｏｒ：Ｏ４と呼ぶ）と呼ばれる。他に、領域のクリアを行う構造作用要素（Ｓ４と呼ぶ）がある。
＜パレットＷ０２＞
値を入力単語に関連付けるという目的を持つ２つの述語ベクトルがある。メインメモリ上（Ｌｙｅｅプログラム領域の外）への入力を行う入力作用要素（Ｉｎｐｕｔ  Ｖｅｃｔｏｒ：Ｉ２と呼ぶ）と、属性チェックとＬｙｅｅプログラム領域内への入力を行うＬ２である。
＜パレットＷ０３＞
パレットＷ０３の述語ベクトルＬ３の目的は、図８に示すように、要件内に指定されている、単語の定義式（すなわちＬ４）を実行するための条件を判定することである。【００７７】  最後に、表８は、表６の要件を実装したＬｙｅｅプログラムを示す。【００７８】  各パレットに１つおかれたパレット関数が、パレット内の述語ベクトルをコール（起動）する。パレット関数は、プログラムに１つおかれたパレット連鎖関数によってコールされる。パレット連鎖関数は、各パレットのＲ４、Ｒ２、Ｒ３の指定に従って、該当するパレット関数をコールする。その他のプログラムの意味は、表８のコメントのとおりである。述語ベクトルＬ４、Ｌ２、Ｌ３（総称して論理要素と呼ぶ）の処理対象は単語単位であり、入出力作用要素（Ｉ２およびＯ４）、構造作用要素（Ｓ４）の処理対象は単語の集合である。【００７９】
【表８】
2005029323.tif 000028
ここでＬｙｅｅ計算法を使用すると、Ｗ０４、Ｗ０３およびＷ０２のプロセスは、それぞれ下記のように定義することができる。【００８０】
【数２０】
2005029323.tif 000029
Ｗ０４プロセスは、Ｓ４、Ｌ４＿ａ、Ｌ４＿ｂ、Ｏ４の各プロセスの並行プロセスである。
Ｗ０３プロセスは、Ｌ３＿ａ、Ｌ３＿ｂの各プロセスの並行プロセスである。
Ｗ０２プロセスは、Ｌ２＿ｅ、Ｌ２＿ｃ、Ｉ２の各プロセスの並行プロセスである。
異なる述語ベクトル（Ｌ２、Ｌ３、Ｌ４、Ｉ２、Ｏ４、Ｓ４）の形式的定義については、次のセクションで説明する。
３．３  処理経路図（Ｐｒｏｃｅｓｓ  Ｒｏｕｔｅ  Ｄｉａｇｒａｍ）
前のセクションで示した基本構造は、任意の、要件が簡単なケースのプログラム全体だと見なしてもよい。特に、すべての入力単語および出力単語が、同じ画面に属していて、データベースが全く使用されていない場合のプログラムである。入力単語および出力単語が、いくつかのデータベースまたは、相互に接続された異なる画面に属する場合には、状況はもっと複雑になる。説明を簡単にするために、以下の説明においては、画面の数が複数あるだけの場合について説明する。図９に示すように、相互に接続している画面が３つあり、ユーザは画面から別の画面に移動することができる場合について考える。各画面において、ユーザは単語の入力、計算、また出力ができる。従って、仕様書では、ユーザは、これらの画面がどのように相互接続しているのかを指定しなければならない。【００８１】  さらに言えば、１つの基本構造だけを定義して、そこで全画面中の定義された単語全てを計算するのは都合がよくない。なぜなら、実際、プログラムの任意の実行において、ある画面は訪問されないかもしれず、その場合、訪問されなかった画面の単語の値の計算が無駄になるからである。そのため、Ｌｙｅｅは、各画面に、その画面が訪問された場合だけ実行されるような担当基本構造を関連づける。画面に係わる基本構造は、１つの画面から他の画面への移動を示すように、接続されている。Ｌｙｅｅ用語において、複数の基本構造が接続されたものが、図１０に示すような、処理経路図（Ｐｒｏｃｅｓｓ  Ｒｏｕｔｅ  Ｄｉａｇｒａｍ）である。【００８２】  Ｌｙｅｅ計算法を使用して、ある画面ｓｋを、プロセスＳＦ（ｓｋ）の実行を制御するプロセスΦ（ｓｋ）、として下式のように形式化できる。【００８３】
【数２１】
2005029323.tif 000030
すなわち、プロセスΦ（ｓｋ）は、プロセスＳＦ（ｓｋ）（画面ｓｋに係わる処理の基本構造のプロセス）としてふるまい、チャネル？ｓｋ上で真の値を受信したとき、ＳＦ（ｓｋ）を停止してプロセスΦ（ｓｋ）としてふるまう。実際の動きとしては、制御プロセスΦ（ｓｋ）は、プロセスＳＦ（ｓｋ）を活性化し、画面ｓｋに関連するチャネル？ｓｋ上で信号を受信したとき（すなわち画面ｓｋが再活性化されたとき）、Φ（ｓｋ）自身が再活性化される。従って、制御プロセスΦ（ｓｋ）が再活性化されることによって、ＳＦ（ｓｋ）は一度終了して再活性化され、初期状態（ｆｒｅｓｈ  ｉｎｓｔａｎｃｅ）に戻る。【００８４】  関数Φ（ｓｋ）がどのように機能するかを示す具体例は、本明細書の後の方に記す。
３．４  Ｌｙｅｅプログラム
まとめると、Ｌｙｅｅ方法論によるＬｙｅｅプログラムの構造は次のとおりである。Ｌｙｅｅプログラムはいくつかの処理経路図（ＰＲＤ）で構成される。各ＰＲＤは、相互に接続された基本構造（ＳＦ）の集合である。各基本構造は、３つの相互に接続されたパレットＷ０２、Ｗ０３、Ｗ０４で構成される。最後に、パレットは、述語ベクトルによって構成される。述語ベクトルには、Ｌｙｅｅプログラムの最小単位のモジュールであるので、アトミック・ベクトル（ａｔｏｍｉｃ  ｖｅｃｔｏｒ）とも呼ぶ。述語ベクトルには、論理要素（ｓｉｇｎｉｆｉｃａｔｉｏｎ  ｖｅｃｔｏｒ：Ｌ２、Ｌ３、Ｌ４の総称）および作用要素（ａｃｔｉｏｎ  ｖｅｃｔｏｒ：Ｉ２、Ｏ４、Ｓ４、Ｒ２、Ｒ３、Ｒ４の総称）がある。これらの述語ベクトルの実行を制御する制御モジュールとして、パレットごとにパレット関数がおかれ、そのパレット関数の実行を制御するモジュールとして、プログラムに１つのパレット連鎖関数がおかれる。【００８５】  Ｌｙｅｅ計算法を使用することにより、画面ｓ１，．．．，ｓｋを含むＬｙｅｅプログラムＰは、下式のように形式化される。【００８６】
【数２２】
2005029323.tif 000031
ここで、Ｌ（ｓ１，．．．，ｓｋ）は、入力チャネルおよび出力チャネルの集合である。この式は、Ψ（ｓ１，．．．，ｓｋ）が、Ｌ（ｓ１，．．．，ｓｋ）に属すチャネルだけを通して環境とコミュニケートするように制限する。【００８７】  関数Ψは、下式のように定義される。【００８８】
【数２３】
2005029323.tif 000032
この関数Ψは、画面ｓ（ｓは画面ｓ１，．．．，ｓｋのいずれか）に対応するチャネル？ｓ上で真の値を受信するたびに、画面ｓに対応するＳＦ（ｓ）を起動するために、プロセスΦ（ｓ）を起動。上記チャネル？ｓは、対応する画面を起動するためにユーザが使用するボタンやメニューを形式化したものである。また、この関数Ψは、チャネル？ｓ０上で真の値を受信した時ときに、すべての他のプロセスを終了させて、関数Ψ自身も終了（ｎｉｌになる）する。チャネル？ｓ０は終了ボタン（または、対応するメニュー項目）を形式化したものである。【００８９】  従って、Ｌｙｅｅシステムは、求める出力単語を計算するために相互にコミュニケートする、独立した並行プロセス（ｃｏｎｃｕｒｒｅｎｔ  ｐｒｏｃｅｓｓ）の集合体と見なすことができる。Ｌｙｅｅ方法論の従来の逐次処理的（ｓｅｑｕｅｎｔｉａｌ）見方とは対照的に、すべての経路作用要素は必要なく、制御機能の役割は大幅に簡易化され、作業メモリ領域（ｗｏｒｋｉｎｇ  ｍｅｍｏｒｙ）等も必要ない。Ψ（ｓ１，．．．，ｓｋ）については、具体例と一緒に以下にさらに詳細に説明する。【００９０】  次のセクションにおいては、Ｌｙｅｅ方法論のより詳細かつ完全な形式化について説明する。
４．Ｌｙｅｅ方法論の形式化
Ｌｙｅｅ計算法を使用して、簡単なユーザ要件からどのようにしてソフトウェアを自動的に生成するかを見る。
ユーザ要件は、ｋ個の画面｛ｓ１，．．．，ｓｋ｝を含んでいるとする。また、各画面は宣言の集合を含んでいるとする。この場合、各宣言は、次の形式、すなわち、（ｗ，ｅ，ｃ，ＩｎＯｕｔ，ｔｙｐｅ）を持つ。ここで、ｗは単語名、ｅはその定義式、ｃは定義式の実行条件、ＩｎＯｕｔは単語が入力か出力か、あるいは両方か、または入力でも出力でもないのかの指定（値ｉは入力単語に、値ｏは出力単語に、ｉｏは入力および出力両方である場合に、空のフィールドは入力でも出力でもない場合に使用される）、ｔｙｐｅは値の属性（タイプ）を示す（たとえばタイプＢは、ボタンを示す記号として割り当てられる）。
この要件に関するプログラムＰ（ｓ１，．．．，ｓｋ）を定義するために、下記の表に示したように論理要素および作用要素のベクトル（プロセス）を形式化する。【００９１】  まず、形式化に用いられている未定儀定義の記号を説明する。
Ｕｓｅ（ｅ）は、式ｅで使用する単語の集合を示すものとする。例えば、Ｕｓｅ（ａ＊ｂ＋１）＝｛ａ，ｂ｝である。
また、Ｆ（Ｓ）は、変数Ｓとして入力値の集合をとり、その入力を行う受信作用の集合をかえす関数である。【００９２】
【数２４】
2005029323.tif 000033
上記の意味は次のようになる。
入力値がないとき（Ｆ（０））、受信作用はない（０は空集合）。
入力値ｘと入力値Ａの受信作用（Ｆ（｛ｘ｝∪Ａ））は、チャネル【００９３】
【数２５】
2005029323.tif 000034
上でｘの値を受信する受信作用と、入力Ａの受信作用Ｆ（Ａ）の和集合である。【００９４】  論理要素（Ｓｉｇｎｉｆｉｃａｔｉｏｎ  Ｖｅｃｔｏｒｓ）は表９に示す。【００９５】
【表９】
2005029323.tif 000035
作用要素（Ａｃｔｉｏｎ  Ｖｅｃｔｏｒ）は表１０に示す。【００９６】
【表１０】
2005029323.tif 000036
ベクトルのうち、Ｓ４は、２．２で述べた値を保持するメモリ・セルで、かつ、「初期化される（初期値を受信する）までその内容にアクセスさせない」能力をもったスマート・セルである。【００９７】  経路作用要素は、Ｌｙｅｅ計算法においては本質的には不要なプロセスであるが、Ｌｙｅｅ計算法でどのように形式化できるかを示すために記載している。
パレット
任意の画面ｓの３つのパレットＷ０２、Ｗ０３およびＷ０４は、下式のように形式化される。【００９８】
【数２６】
2005029323.tif 000037
ここで、【００９９】
【数２７】
2005029323.tif 000038
は、Ｂ（ボタンを示す）を除く任意のタイプ（Ｂの補集合）を示し、＊は何であってもよいことを示す。
基本構造：
画面ｓの基本構造ＳＦ（ｓ）は、下式のように形式化される。【０１００】
【数２８】
2005029323.tif 000039
制御機能：
画面ｓに付随する制御機能は、下式のように形式化される。【０１０１】
【数２９】
2005029323.tif 000040
画面の集合に付随する制御機能は、下式のように形式化される。【０１０２】
【数３０】
2005029323.tif 000041
ｓ０は、プログラムを終了したときの画面（プログラム自身の画面群には属さない終了画面）であるとする。【０１０３】  ここで制御機能の役割についてまとめると、下記のようになる。【０１０４】
【表１１】
2005029323.tif 000042
本論では、Ｌｙｅｅ計算法の実現方法の１つとして、ＳＦは、画面に対して１つもうけ、１つのＳＦが、対応する画面に係わる入出力および計算の全てのプロセスを含むように形式化した。従ってＳＦの制御関数Φも、画面に１つである。しかし、画面に対して複数のＳＦおよび制御関数Φを設けるように形式化することも選択しとして可能である。実装方法は、プログラムとしての効率性によって決定すればよい。
Ｌｙｅｅプログラム：
最後に、画面ｓ１，．．．，ｓｋを含む要件に関するＬｙｅｅプログラムＰ（ｓ１，．．．，ｓｋ）は下式で表される。【０１０５】
【数３１】
2005029323.tif 000043
ここで、Ｌ（ｓ１，．．．，ｓｋ）の集合は、環境との間のすべての入力チャネルおよび出力チャネルを含み、下式により定義される。【０１０６】
【数３２】
2005029323.tif 000044
ｉ／ｏの意味は、この項目は値ｉ、ｏまたはｉｏを含んでいなければならないことをさす。また、ｓ１は、ユーザがこのプログラムを実行した場合に最初に現れる画面である。
【実施例１】
【０１０７】５．ケーススタディ１
このセクションにおいては、Ｌｙｅｅ計算法で単語を計算するために、Ｌｙｅｅプログラムがどのように進行するかを、具体例を上げて段階的に説明する。【０１０８】  ここに示す例は、画面を１つしか持たない（２つの画面を持つ他の例は付録に記載した）。表１２の要件に示すように、ユーザは、単語ａを入力し、単語ｂの値を待ち、次に、ボタンＢ０を押して画面を終了する。図１１はこのような画面を示す。【０１０９】
【表１２】
2005029323.tif 000045
この画面ｓ１は３つの宣言からなる。【０１１０】
【数３３】
2005029323.tif 000046
前のセクションで説明した一般的なＬｙｅｅプログラムの定義によれば、表１２の要件に関するＬｙｅｅプログラムは、下式により表される。【０１１１】
【数３４】
2005029323.tif 000047
ここで、Ｗ０２（ｓ１）、Ｗ０３（ｓ１）およびＷ０４（ｓ１）は、下記の通りである。前述したように、Ｒ３のプロセスはＬｙｅｅ計算法では必須ではないので、省くことも可能である。【０１１２】
【表１３】
2005029323.tif 000048
ここで、このプログラムＰ（Ｓ１）のエンドユーザ（環境）が、下記の一連の行動を行いたいと考えていると仮定しよう。プログラムを実行し（画面ｓ１を起動し）、単語ａに値「７」を与え、単語ｂの値を得るのを待ち、ボタンＢ０を押してプログラムを終了する。このエンドユーザの行動は、下記のプロセスεにより捉えることができる。【０１１３】
【表１４】
2005029323.tif 000049
上記に示した、Ｌｙｅｅ計算法によるプログラムＰ（Ｓ１）のプロセスとエンドユーザのプロセスを図１２に示した。【０１１４】  次に、求められる目的に到達するために、プログラムＰ（Ｓ１）がこの環境とどのように相互作用を行うかを見る。言い換えると、エンドユーザの行動を取り込むプログラムεと並行に実行されるプログラムＰ（Ｓ１）の進行プロセスを追うのである。これは、すなわち、Ｐ（ｓ１）｜εのふるまいを探すことである。このプロセスのステップは下記の通りである。定義式には、等号記号の左辺が右辺に置き換えられる根拠となる定義をコメントとして付した。また、プロセス間の相互作用によって、同期（ｓｙｎｃｈｒｏｎｉｚａｔｉｏｎ）（同一チャネル上で値の送信と受信が同時に成立した）が起こった部分にもコメントを付した。下線部分が同期した送信および受信作用である。【０１１５】
【表１５】
2005029323.tif 000050
【０１１６】
【表１６】
2005029323.tif 000051
まとめると、プログラムの進行の主要なステップは下記の通りである。
エンドユーザが、プログラム起動のコマンドを送ることによって、制御関数Ψ（ｓ１）が起動されて、制御関数Ψ（ｓ１）が制御関数Φ（ｓ１）を起動し、制御関数（ｓ１）が初期画面ｓ１とＳＦ（ｓ１）を起動することによって、プログラムが起動する。【０１１７】
【数３５】
2005029323.tif 000052
エンドユーザが単語ａに値「７」を与える（送信する）と、ＳＦ（ｓ１）の中のＩ２（ａ）が値７を受信する。【０１１８】
【数３６】
2005029323.tif 000053
Ｉ２（ａ）は、ａの値７をＬ２（ａ）に送信する。【０１１９】
【数３７】
2005029323.tif 000054
Ｌ２（ａ）が送信したａの値７が、メモリ、すなわち、Ｓ４（ａ）に記憶される（Ｓ４（ａ）に初期値が記憶されることによって初期化された）。【０１２０】
【数３８】
2005029323.tif 000055
ｂの計算条件を計算するために、ａの値７が、初期化されたａのメモリＳ４からＬ３（ｂ，ａ＞０）に送られる。【０１２１】
【数３９】
2005029323.tif 000056
ｂの計算条件が判定され（ａ＞０は真（１）と判定）、Ｌ４（ｂ，２＊ａ）に値１が送られる。【０１２２】
【数４０】
2005029323.tif 000057
ａの値７が、値７を保持しているａのメモリＳ４からＬ４（ｂ，２＊ａ）に送られる。【０１２３】
【数４１】
2005029323.tif 000058
ｂの定義式「２＊ａ」が計算され、ｂの値１４が、メモリ、すなわち、Ｓ４（ｂ）に記憶される（Ｓ４（ｂ）が初期化された）。【０１２４】
【数４２】
2005029323.tif 000059
ｂの値１４が、ｂのメモリＳ４から、出力プロセスＯ４（ｂ）に送られる。【０１２５】
【数４３】
2005029323.tif 000060
１０．Ｏ４によってｂの値が環境に送られ、エンドユーザはｂの値を受信する。この時点で起動中のＳＦ（ｓ１）に属するプロセスは、値を保持しているａおよびｂのＳ４と、Ｒ３（Ｂ０，ｃｌｉｃｋ，ｓ０）である。【０１２６】
【数４４】
2005029323.tif 000061
１１．エンドユーザが、プログラム終了のためにボタンＢ０を押し、Ｒ３（Ｂ０，ｃｌｉｃｋ，ｓ０）は値ｃｌｉｃｋを受信、自身の計算条件を判定して真の値１を制御関数Ψ（ｓ１）に送信する。真の値１を受信したΨ（ｓ１）は、自身が終了する前にΦ（ｓ１）を終了させ、Φ（ｓ１）は自身が終了する前にＳＦ（ｓ１）を終了させる。【０１２７】
【数４５】
2005029323.tif 000062
図１３は、これらの各ステップを示す。【０１２８】  かっこ付き番号は、上記のステップの説明に対応する。かっこなしの数字は、送受信される値を示している。【０１２９】  さらに、各プロセスの遷移は証明によって確認することができる。例えば、下記のプロセスの遷移がある（上記ステップ１に対応）。Ｐ（ｓ１）とεの間に同期が起こり（プログラム起動コマンドの送受信）、Ｐ１（ｓ１）とε１の並行プロセスに移行するプロセス遷移を表わしている。【０１３０】
【数４６】
2005029323.tif 000063
このとき、【０１３１】
【数４７】
2005029323.tif 000064
である。
上記は、表５の規則を用いて、次の証明で正しいことが確認できる。【０１３２】
【数４８】
2005029323.tif 000065
６．結論
本稿は、最初に、Ｌｙｅｅ方法論の基本概念を容易かつ本質的にサポートするＬｙｅｅ計算法と呼ぶ形式的プロセス代数を定義した。実際に、この計算法は、フォン・ノイマンのものより、Ｌｙｅｅ方法論の概念をサポートするのにより適した抽象機械と見なすことができる。この機械は、プログラムを最終結果を生成するために共に相互作用し合う分子の集合と見なす。二番目に、この計算法がどのようにして、全ソフトウェア生成プロセスとＬｙｅｅベクトルの両方を形式化し、簡易化することができるのかを示した。実際、経路作用要素（ｒｏｕｔｉｎｇ  ｖｅｃｔｏｒ）、はもはや必要としない。また、パレット関数も不要となり、制御機能の役割は大幅に簡易化される。Ｌｙｅｅソフトウェア生成の自動生成の全プロセスを形式化した。この形式化によって、この方法論の意味論を、この方法論の背後にある概念を明快に理解することができるように形式化することができる。その上、この形式的記述は、いろいろな局面におけるこの方法論の多くの興味ある分析を始めるためには不可避である。例えば、Ｌｙｅｅで生成したソフトウェアまたはソフトウェア生成プロセスを最適化するためには、最適化されたプログラムがその元のバージョンと同じものである、という形式的証明を必要とする。プロセス代数を使用すれば、形式的に同じものであることのチェック、またはもっと一般的にモデル・チェックをうまく行うことができる。【０１３３】  将来の研究として、我々はＬｙｅｅ方法論の意味論をさらに研究し、Ｌｙｅｅ方法論をより簡素化し、要件からより信頼性の高い最適化されたコードの生成が行えるようにしたい。最適化するために、Ｌｙｅｅ計算法のプロセス間の適合（ｃｏｎｇｒｕｅｎｃｅ）関係を定義し、それによってすべてのそこから帰結する最適化が正しいことを証明したいと考えている。
【実施例２】
【０１３４】＜付録＞
ケーススタディ２−画面が２つの場合
複数画面間の相互作用を示すために、２つの画面からなるプログラムのケースについて述べる。図１４がそのプログラムの画面を示した図である。このプログラムを起動すると画面Ｓ１が表示される。画面Ｓ１で、ユーザは、単語ａを入力し、単語ｂの値が出力されるのを待つ。ボタンＢ２を押すと、画面Ｓ２が表示され、単語ｂの値が出力されるのを待つ。画面Ｓ２でボタンＢ０をおすと、プログラムを終了する。【０１３５】  図１４のプログラムの要件の宣言をまとめると、画面Ｓ１の要件は表１７、画面Ｓ２の要件は表１８のようになる。【０１３６】
【表１７】
2005029323.tif 000066
【０１３７】
【表１８】
2005029323.tif 000067
前のセクションで説明した一般的なＬｙｅｅプログラムの定義によれば、表１７および表１８の要件に関するＬｙｅｅプログラムは、下式により表される。【０１３８】
【数４９】
2005029323.tif 000068
画面ｓ２に対するＷ０２が存在しないことに留意されたい。何故なら、Ｗ０２は、ボタン以外に入力単語を含んでいないからである。【０１３９】
【数５０】
2005029323.tif 000069
ここにおいては、Ｗ０２（ｓ１）、Ｗ０３（ｓ１）、Ｗ０４（ｓ１）および、Ｗ０３（ｓ２）、Ｗ０４（ｓ２）は、以下のように定義される。ケーススタディ１と同様に、Ｒ３のプロセスはＬｙｅｅ計算法では必須ではないので、省くことも可能である。【０１４０】
【表１９】
2005029323.tif 000070
【０１４１】
【表２０】
2005029323.tif 000071
【０１４２】
【表２１】
2005029323.tif 000072
ここで、このプログラムのエンドユーザ（環境）が、下記の一連の行動を行いたいと考えているとする。プログラムを実行し（画面ｓ１を起動し）、単語ａに値「７」を与え、単語ｂの値を得るために待機し、画面ｓ２に行くためにボタンＢ２を押し、値ｅを得るために待機し、ボタンＢ０を押すことによりプログラムを終了する。この行動は、下記のプロセスεにより捉えることができる。【０１４３】
【表２２】
2005029323.tif 000073
上記に示した、Ｌｙｅｅ計算法によるプログラムＰ（Ｓ１）のプロセスとエンドユーザのプロセスを図１５に示した。【０１４４】  プログラムの進行の主要なステップは下記の通りである。
エンドユーザが、プログラム起動のコマンドを送ることによって、制御関数Ψ（ｓ１，ｓ２）が起動されて、制御関数Ψ（ｓ１，ｓ２）が制御関数Φ（ｓ１）を起動し、制御関数（ｓ１）が初期画面ｓ１とＳＦ（ｓ１）を起動することによって、プログラムが起動する。
Ｐ（ｓ１，ｓ２）とεの間に同期が起こり（プログラム起動コマンドの送受信）、Ｐ１（ｓ１，ｓ２）とε１の並行プロセスに移行。【０１４５】
【数５１】
2005029323.tif 000074
ここで、【０１４６】
【数５２】
2005029323.tif 000075
エンドユーザが単語ａに値「７」を与える（送信する）と、ＳＦ（ｓ１）の中のＩ２（ａ）が値７を受信する。
Ｐ１（ｓ１，ｓ２）とε１の間に同期が起こり（単語ａの値の送受信）、Ｐ２（ｓ１，ｓ２）とε２の並行プロセスに移行。【０１４７】
【数５３】
2005029323.tif 000076
ここで、【０１４８】
【数５４】
2005029323.tif 000077
ａの値７がメモリＳ４（ａ）に記憶される。この記憶は、２つのステップにより行うことができる。第１のステップにおいて、ａの値７がＬ２（ａ）に送られる。第２のステップにおいて、Ｌ２（ａ）は、この値をメモリＳ４（ａ）に送る。
第１のステップは下記の通りである。Ｐ２（ｓ１，ｓ２）の中で同期が起こり（Ｉ２（ａ）とＬ２（ａ）間の単語ａの値７の送受信）、Ｐ３（ｓ１，ｓ２）とε２の並行プロセスに移行。
：【０１４９】
【数５５】
2005029323.tif 000078
ここで、【０１５０】
【数５６】
2005029323.tif 000079
第２のステップにおいて、ａの値７はＷ０４のメモリＳ４（ａ）に記憶される（Ｓ４（ａ）に初期値が記憶されることによって初期化された）。Ｐ３（ｓ１，ｓ２）の中で同期が起こり（Ｌ２（ａ）とＳ４（ａ）間の単語ａの値７の送受信）、Ｐ４（ｓ１，ｓ２）とε２の並行プロセスに移行。
：【０１５１】
【数５７】
2005029323.tif 000080
ここで、【０１５２】
【数５８】
2005029323.tif 000081
ｂの計算条件を計算するために、ａの値７が、初期化されたａのメモリＳ４からＬ３（ｂ，ａ＞０）に送られる。Ｐ４（ｓ１，ｓ２）の中で同期が起こり（Ｓ４（ａ）とＬ３（ｂ，ａ＞０）の間の送受信）、Ｐ５（ｓ１，ｓ２）とε２の並行プロセスに移行。：【０１５３】
【数５９】
2005029323.tif 000082
ここで、【０１５４】
【数６０】
2005029323.tif 000083
ｂの計算条件が判定され（ａ＞０は真（１）と判定）、Ｌ４（ｂ，２＊ａ）に値１が送られる。Ｐ５（ｓ１，ｓ２）の中で同期が起こり（Ｌ３（ｂ，ａ＞０）とＬ４（ｂ，２＊ａ）の間の真偽値１の送受信）、Ｐ６（ｓ１，ｓ２）とε２の並行プロセスに移行。：【０１５５】
【数６１】
2005029323.tif 000084
ここで、【０１５６】
【数６２】
2005029323.tif 000085
ａの値７がａのメモリＳ４からＬ４（ｂ，２＊ａ）に送られ、ｂの定義式「２＊ａ」が計算され、ｂの値１４が、メモリＳ４（ｂ）に記憶される（Ｓ４（ｂ）が初期化された）。Ｐ６（ｓ１，ｓ２）の中で同期が起こり（ａのメモリＳ４とＬ４（ｂ，２＊ａ）との間、Ｌ４（ｂ，２＊ａ）とｂのメモリＳ４の間の送受信）、Ｐ７（ｓ１，ｓ２）とε２の並行プロセスに移行。：【０１５７】
【数６３】
2005029323.tif 000086
ここで、【０１５８】
【数６４】
2005029323.tif 000087
ｂの値１４が、ｂのメモリＳ４から、出力プロセスＯ４（ｂ）に送られる。Ｏ４（ｂ）によってｂの値が環境に送られ、エンドユーザはｂの値を受信する。Ｐ７（ｓ１，ｓ２）の中の同期（Ｌ４（ｂ，２＊ａ）とＯ４（ｂ）の間の送受信）と、Ｐ７（ｓ１，ｓ２）とε２間の同期（単語ｂの値の送受信）が起こり、Ｐ８（ｓ１，ｓ２）とε３の並行プロセスに移行。
この時点で起動中のＳＦ（ｓ１）に属するプロセスは、値を保持しているａおよびｂのＳ４と、Ｒ３（Ｂ０，ｃｌｉｃｋ，ｓ０）である。：【０１５９】
【数６５】
2005029323.tif 000088
ここで、【０１６０】
【数６６】
2005029323.tif 000089
画面２に行くために、エンドユーザは画面ｓ１上のボタンＢ２を押す。ε３から送信されたボタンＢ２のＣｌｉｃｋ値をＲ３（Ｂ２，ｃｌｉｃｋ，ｓ２）が受信、Ｒ３（Ｂ２，ｃｌｉｃｋ，ｓ２）は自身の計算条件を判定して真の値１を制御関数Ψ（ｓ１，ｓ２）に送信する。値１を受信した制御関数Ψ（ｓ１，ｓ２）は制御関数Φ（ｓ２）を起動。値１を受信した制御関数Φ（ｓ２）は、ＳＦ（ｓ２）を起動し、画面ｓ２を起動する。
Ｐ８（ｓ１，ｓ２）とε３の間の同期（ボタンＢ２のｃｌｉｃｋ値の送受信と）、Ｐ８（ｓ１，ｓ２）の中の同期（Ｒ３（Ｂ２，ｃｌｉｃｋ，ｓ２）と、Ψ（ｓ１，ｓ２）および制御関数Φ（ｓ２）間の送受信）が起こり、Ｐ９（ｓ１，ｓ２）とε４の並行プロセスに移行。：【０１６１】
【数６７】
2005029323.tif 000090
ここで、【０１６２】
【数６８】
2005029323.tif 000091
ｅの条件を計算するために、ｂのメモリＳ４から値１４をＬ３（ｅ，ｂ＞０）に送信する。Ｐ９（ｓ１，ｓ２）の中で同期が起こり（ａのメモリＳ４とＬ３（ｅ，ｂ＞０）との間の送受信）、Ｐ１０（ｓ１，ｓ２）とε４の並行プロセスに移行。：【０１６３】
【数６９】
2005029323.tif 000092
ここで、【０１６４】
【数７０】
2005029323.tif 000093
ｅの計算条件ｂ＞０が真（１）と判定され、Ｌ３（ｅ，ｂ＞０）から真の値１がＬ４（ｅ，１＋ｂ）に送信され、ｅの値が計算される。Ｐ１０（ｓ１，ｓ２）の中で同期が起こり（Ｌ３（ｅ，ｂ＞０）とＬ４（ｅ，１＋ｂ）の間の送受信）、Ｐ１１（ｓ１，ｓ２）とε４の並行プロセスに移行。：【０１６５】
【数７１】
2005029323.tif 000094
ここで、【０１６６】
【数７２】
2005029323.tif 000095
ｅの値を、Ｌ４（ｅ，１＋ｂ）から、ｅのメモリＳ４（ｂ）に記憶する（Ｓ４（ｂ）が初期化された）。Ｐ１１（ｓ１，ｓ２）の中で同期が起こり（Ｌ４（ｅ）とｅのメモリＳ４の間の送受信）、Ｐ１１（ｓ１，ｓ２）とε４の並行プロセスに移行。：。：【０１６７】
【数７３】
2005029323.tif 000096
ここで、【０１６８】
【数７４】
2005029323.tif 000097
ｅのメモリＳ４（ｂ）からｅの値１５を、Ｏ４（ｅ）に送信、Ｏ４（ｅ）からエンドユーザε４にｅの値を出力する。Ｐ１１（ｓ１，ｓ２）とε４の間で同期が起こり（単語ｅの値１４の送受信）、Ｐ１２（ｓ１，ｓ２）とε５の並行プロセスに移行。：【０１６９】
【数７５】
2005029323.tif 000098
ここで、【０１７０】
【数７６】
2005029323.tif 000099
エンドユーザが、プログラムを終了するためにボタンＢ０を押す。Ｒ３（Ｂ０，ｃｌｉｃｋ，ｓ０）は、エンドユーザε５らボタンＢ０の値ｃｌｉｃｋを受信し、制御関数Ψ（ｓ１，ｓ２）に送信する。Ψ（ｓ１，ｓ２）は、自身が終了する前にΦ（ｓ１）およびΦ（ｓ２）を終了させ、Φ（ｓ１）およびΦ（ｓ２）は自身が終了する前に、それぞれＳＦ（ｓ１）およびＳＦ（ｓ２）を終了させる。Ｐ１２（ｓ１，ｓ２）とε５の間で同期が起こり（ＣＣｌｉｃｋ値の送受信）、次にＰ１２（ｓ１，ｓ２）の中で同期（Ｒ３（Ｂ０，ｃｌｉｃｋ，ｓ０）と、Ψ（ｓ１，ｓ２）、制御関数Φ（ｓ１）およびΦ（ｓ２）間の送受信）が起こり、すべてのプロセスがｎｉｌに移行する。：【０１７１】
【数７７】
2005029323.tif 000100
なお、本発明は、上述した実施形態および実施例には限定されず、本発明の技術思想の範囲内で様々な変形が可能である。たとえば、ビジネス・メソッド、ソフトウェア開発装置、ソフトウェア開発支援装置、ソフトウェア開発管理装置、あるいはこれらの機能をコンピュータに実現するためのソフトウェア並びに該ソフトウェアを搭載した記録媒体・専用機、などとしてもそれぞれ実現することが可能である。さらに、上記で説明したように本発明は、方法としても、或いはかかる機能を備えるソフトウェアとしても、該ソフトウェアが搭載される装置・ツール（ソフトウェア自体の場合も含む）としても、さらにはシステムとしても、実現され得るのはもとよりである。【０１７２】  例えば図１６は、本発明の異なる一実施形態として、「開発対象のソフトウェア」を生産するためのプログラム（ソフトウェア）、プログラム生成装置、プログラム処理装置、ツール（装置として或いはソフトウェアとしての双方を含む）、ソフトウェア開発装置、ソフトウェア開発支援装置、或いはソフトウェア開発管理装置のいずれかとして本発明を実施する場合に機能として備える構成を示した機能ブロック図である。同図に示すように、本発明に係るプログラム（ソフトウェア）、プログラム生成装置、プログラム処理装置、ツール（装置として或いはソフトウェアとしての双方を含む）、ソフトウェア開発装置、ソフトウェア開発支援装置、或いはソフトウェア開発管理装置は、全体制御部１６０１、宣言情報挿入部１６０２、制御関数Φ配置部１６０３、制御関数Ψ配置部１６０４及び情報記憶部１６０５を備えて構成される。【０１７３】  全体制御部１６０１は、本プログラム（ソフトウェア）、プログラム生成装置、プログラム処理装置、ツール（装置として或いはソフトウェアとしての双方を含む）、ソフトウェア開発装置、ソフトウェア開発支援装置、或いはソフトウェア開発管理装置の全体の動作制御、タイミング制御、入出力制御等を行う機能を有しており、当該機能を持つ専用チップ、専用回路、または当該機能をコンピュータに果たさせるためのソフトウェア（ツールとしてのソフトウェアも含む）、或いは該ソフトウェアを記録した記録媒体、当該記録媒体を搭載した処理装置・管理装置・ツールとして実現される。【０１７４】  宣言情報挿入部１６０２は、Ｌｙｅｅ計算法による入出力チャネルをそなえたプロセス・セルとしてモジュール化された論理要素（Ｌ２、Ｌ３、Ｌ４）および、作用要素（Ｉ２、Ｏ４、Ｓ４）のひな型の未定義部分に、１つのプログラムとして実装するユーザ要件を、論理体ごとに、該論理体上の単語ごとの、単語名、定義式、該定義式の実行条件、入出力属性、単語の値の属性からなる宣言として情報化した情報を挿入するための機能を有しており、当該機能を持つ専用チップ、専用回路、または当該機能をコンピュータに果たさせるためのソフトウェア（ツールとしてのソフトウェアも含む）、或いは該ソフトウェアを記録した記録媒体、当該記録媒体を搭載した処理装置・管理装置・ツールとして実現される。【０１７５】  制御関数Φ配置部１６０３は、前記論理要素と作用要素を、同一画面からのコマンドで相互作用を起こすことを集合条件とする集合単位に、１つの制御���数モジュールΦが、制御するように関連づけるための機能を有しており、当該機能を持つ専用チップ、専用回路、または当該機能をコンピュータに果たさせるためのソフトウェア（ツールとしてのソフトウェアも含む）、或いは該ソフトウェアを記録した記録媒体、当該記録媒体を搭載した処理装置・管理装置・ツールとして実現される。【０１７６】  制御関数Ψ配置部１６０４は、１つの制御関数モジュールΨを、前記制御関数Φを制御するように前記制御関数Φに関連づけるための機能を有しており、当該機能を持つ専用チップ、専用回路、または当該機能をコンピュータに果たさせるためのソフトウェア（ツールとしてのソフトウェアも含む）、或いは該ソフトウェアを記録した記録媒体、当該記録媒体を搭載した処理装置・管理装置・ツールとして実現される。【０１７７】  情報記憶部１６０５は、プログラム情報のほか、各種制御情報、プロセス・セルとしてモジュール化された論理要素（Ｌ２、Ｌ３、Ｌ４）および、作用要素（Ｉ２、Ｏ４、Ｓ４）の前記ひな型、前記制御関数モジュールΦのひな型、前記制御関数モジュールΨのひな型、目的プログラム等の格納のほか、一時記憶のためのメモリとしても用いられる。【０１７８】  図１７は、上記の構成を備えるプログラム（ソフトウェア）、プログラム生成装置、プログラム処理装置、ツール（装置として或いはソフトウェアとしての双方を含む）、ソフトウェア開発装置、ソフトウェア開発支援装置、或いはソフトウェア開発管理装置のいずれかとして実施される本発明の動作を示したフローチャートである。【０１７９】  同図に示すように、まず、宣言情報挿入部１６０２は、Ｌｙｅｅ計算法による入出力チャネルをそなえたプロセス・セルとしてモジュール化された論理要素（Ｌ２、Ｌ３、Ｌ４）および、作用要素（Ｉ２、Ｏ４、Ｓ４）のひな型の未定義部分に、１つのプログラムとして実装するユーザ要件を、論理体ごとに、該論理体上の単語ごとの、単語名、定義式、該定義式の実行条件、入出力属性、単語の値の属性からなる宣言として情報化した情報を挿入する。（ステップ１７０１）。【０１８０】  すると、制御関数Φ配置部１６０３は、前記論理要素と作用要素を、同一画面からのコマンドで相互作用を起こすことを集合条件とする集合単位に、１つの制御関数モジュールΦが、制御するように関連づける。（ステップ１７０２）。【０１８１】  次に、制御関数Ψ配置部１６０４は、１つの制御関数モジュールΨを、前記制御関数Φを制御するように前記制御関数Φに関連づける。（ステップ１７０３）。【０１８２】  よって、上記のような構成を備える本発明によれば、本発明の独自の体系に基づいて要求定義をとらえ、それを本発明独自の構造を備えるプロセス・セルとしてモジュール化され論理要素（Ｌ２、Ｌ３、Ｌ４）および、作用要素（Ｉ２、Ｏ４、Ｓ４）のひな型の未定義部分に代入するので、所望のソフトウェアが、属人性なく得られる。【０１８３】  本発明の異なる実施体としての「開発対象のソフトウェア」を生産するためのプログラム（ソフトウェア）、プログラム生成装置、プログラム処理装置、ツール（装置として或いはソフトウェアとしての双方を含む）、ソフトウェア開発装置、ソフトウェア開発支援装置、ソフ���ウェア開発管理装置は、Ｌｙｅｅ計算法による入出力チャネルをそなえたプロセス・セルとしてモジュール化された論理要素（Ｌ２、Ｌ３、Ｌ４）および、作用要素（Ｉ２、Ｏ４、Ｓ４）のひな型の未定義部分に、１つのプログラムとして実装するユーザ要件を、論理体ごとに、該論理体上の単語ごとの、単語名、定義式、該定義式の実行条件、入出力属性、単語の値の属性からなる宣言として情報化した情報を挿入する、宣言情報挿入手段と、前記論理要素と作用要素を、同一画面からのコマンドで相互作用を起こすことを集合条件とする集合単位に、１つの制御関数モジュールΦを、前記単位を制御するように関連づける、制御関数Φ配置手段と、１つの制御関数モジュールΨを、前記制御関数Φを制御するように前記制御関数Φに関連づける、制御関数Ψ配置手段とを具備するように構成することもできる。【０１８４】  本発明はさらに、上述の「開発対象のソフトウェアを生産する方法」によって生産されたソフトウェア、及び当該ソフトウェアが搭載された記録媒体或いは当該ソフトウェアが搭載された装置（ハードウェア）としても実現されるが、この場合の本発明は、１つのプログラムとして実装するユーザ要件を、論理体ごとに、該論理体上の単語ごとの、単語名、定義式、該定義式の実行条件、入出力属性、単語の値の属性からなる宣言として情報化した情報を、Ｌｙｅｅ計算法による入出力チャネルをそなえたプロセス・セルとしてモジュール化された論理要素（Ｌ２、Ｌ３、Ｌ４）および、作用要素（Ｉ２、Ｏ４、Ｓ４）のひな型の未定義部分に挿入したモジュール群と、前記モジュール群を、同一画面からのコマンドで相互作用を起こすことを集合条件とする集合単位に、１つの制御関数モジュールΦで制御するように関連づけている１つまたは複数の制御関数モジュールΦと、前記制御関数Φを、１つの制御関数モジュールΨで制御するように関連づけている制御関数モジュールΨで構成されることもできる。【０１８５】  またさらに本発明は、上述の「開発対象のソフトウェアを生産する方法」によってソフトウェアを生産するために用いられるソフトウェアコードの雛型としてのソフトウェア、及び当該ソフトウェアが搭載された記録媒体或いは当該ソフトウェアが搭載された装置（ハードウェア）としても実現されるが、この場合の本発明は、１つのプログラムとして実装するユーザ要件を、論理体ごとに、該論理体上の単語ごとの、単語名、定義式、該定義式の実行条件、入出力属性、単語の値の属性からなる宣言として情報化した情報を、埋め込むべき未定義部分を有した、Ｌｙｅｅ計算法による入出力チャネルをそなえたプロセス・セルとしてモジュール化された論理要素（Ｌ２、Ｌ３、Ｌ４）および、作用要素（Ｉ２、Ｏ４、Ｓ４）のひな型と、前記宣言の情報を未定義部分に挿入した前記論理要素と作用要素を、同一画面からのコマンドで相互作用を起こすことを集合条件とする集合単位に、１つの制御関数モジュールΦで制御するための機能を有した制御関数モジュールΦのひな型と、前記制御関数Φを１つの制御関数モジュールΨで制御するための機能を有した制御関数モジュールΨのひな型とを備えるソフトウェアとしてコード化可能なひな型として実現してもよい。【０１８６】  さら��、本発明は、上述の「開発対象のソフトウェアを生産する方法」による、要件から抽出した情報（ドキュメント（紙、データ））の抽出方法として、またかかる抽出方法によって抽出された情報（ドキュメント（紙、データ））として、さらには当該抽出された情報の使用方法として、或いは、これらの情報が搭載された情報記録媒体として、または情報の抽出方法／使用方法がコード化されたソフトウェア、当該ソフトウェアが搭載された記録媒体／装置（ハードウェア）として、いずれも実現することができるが、この場合の本発明は、Ｌｙｅｅ計算法による入出力チャネルをそなえたプロセス・セルとしてモジュール化された論理要素（Ｌ２、Ｌ３、Ｌ４）および、作用要素（Ｉ２、Ｏ４、Ｓ４）のひな型の未定義部分に挿入すべき、１つのプログラムとして実装するユーザ要件を、論理体ごとに、該論理体上の単語ごとの、単語名、定義式、該定義式の実行条件、入出力属性、単語の値の属性からなる宣言として情報化した情報と、前記宣言の情報を未定義部分に挿入した前記論理要素と作用要素を、同一画面からのコマンドで相互作用を起こすことを集合条件とする集合単位に、１つの制御関数モジュールΦで制御するように関連づけるための情報と、前記制御関数Φを１つの制御関数モジュールΨで制御するように関連づける情報とを備えるソフトウェア開発要件から抽出した情報として実現してもよい。【０１８７】  さらに本願発明は、その技術思想の同一及び等価に及ぶ範囲において様々な変形、追加、置換、拡大、縮小等を許容するものである。また、本願発明を用いて生産される装置、方法、ソフトウェア、システムが、その２次的生産品に登載されて商品化された場合であっても、本願発明の価値は何ら減ずるものではない。
【産業上の利用可能性】
【０１８８】  異なる分野に関連する広範囲のソフトウェアの問題を効率的に処理し、従来の方法論と比較した場合には、Ｌｙｅｅを使用すると開発時間、保守時間およびドキュメント量はかなり少なくなる（７０〜８０％程度）。
【図面の簡単な説明】
【０１８９】
【図１】本発明の一実施形態に係るセルの概念を説明するための概念図である。
【図２】本発明の一実施形態に係る相互に作用するプロセスの例を示す図である。
【図３】本発明の一実施形態に係る要件の実行の概念を説明するための概念図である。
【図４】本発明の一実施形態に係るＬｙｅｅパレットの概念を説明するための概念図である。
【図５】本発明の一実施形態に係る基本構造の概念を説明するための概念図である。
【図６】本発明の一実施形態に係る述語ベクトルの概念を説明するための概念図である。
【図７】本発明の一実施形態に係るＬ４＿ａおよびＬ４＿ｂの述語ベクトルの概念を説明するための概念図である。
【図８】本発明の一実施形態に係るＬ３＿ａおよびＬ３＿ｂの述語ベクトルの概念を説明するための概念図である。
【図９】本発明の一実施形態に係る画面相互作用の概念を説明するための概念図である。
【図１０】本発明の一実施形態に係る処理経路図を説明するための概念図である。
【図１１】本発明の一実施形態に係る画面が一つの場合を示す概念図である（実施例１）。
【図１２】本発明の一実施形態に係るＬｙｅｅ計算法によるプログラムＰ（Ｓ１）のプロセスとエンドユーザのプロセスを示すための説明図である。
【図１３】本発明の一実施形態に係るプロセス間の相互作用を説明するための概念図である。
【図１４】本発明の一実施形態に係る画面が二つの場合を示す概念図である（実施例２）。
【図１５】本発明の一実施形態に係るＬｙｅｅ計算法によるプログラムＰ（Ｓ１）のプロセスとエンドユーザのプロセスを示すための説明図である。
【図１６】本発明の異なる一実施形態として、「開発対象のソフトウェア」を生産するためのプログラム（ソフトウェア）、プログラム生成装置、プログラム処理装置、ツール（装置として或いはソフトウェアとしての双方を含む）、ソフトウェア開発装置、ソフトウェア開発支援装置、或いはソフトウェア開発管理装置のいずれかとして本発明を実施する場合に機能として備える構成を示した機能ブロック図である。
【図１７】本発明の一実施形態に係る上記の構成を備えるプログラム（ソフトウェア）、プログラム生成装置、プログラム処理装置、ツール（装置として或いはソフトウェアとしての双方を含む）、ソフトウェア開発装置、ソフトウェア開発支援装置、或いはソフトウェア開発管理装置のいずれかとして実施される本発明の動作を示したフローチャートである。
【符号の説明】
【０１９０】Ｗ０４    Ｗ０４パレット
Ｗ０２    Ｗ０２パレット
Ｗ０３    Ｗ０３パレット
１６０１  全体制御部
１６０２  宣言情報挿入部
１６０３  制御関数Φ配置部
１６０４  制御関数Ψ配置部
１６０５  情報記憶部
【図１】
2005029323.tif 000101
【図２】
2005029323.tif 000102
【図３】
2005029323.tif 000103
【図４】
2005029323.tif 000104
【図５】
2005029323.tif 000105
【図６】
2005029323.tif 000106
【図７】
2005029323.tif 000107
【図８】
2005029323.tif 000108
【図９】
2005029323.tif 000109
【図１０】
2005029323.tif 000110
【図１１】
2005029323.tif 000111
【図１２】
2005029323.tif 000112
【図１３】
2005029323.tif 000113
【図１４】
2005029323.tif 000114
【図１５】
2005029323.tif 000115
【図１６】
2005029323.tif 000116
【図１７】
2005029323.tif 000117
【国際調査報告】
2005029323.tif 000118
2005029323.tif 000119
2005029323.tif 000120
2005029323.tif 000121