(57)【要約】Ｌｙｅｅ要件の中に、従来法で用いられた静的分析手法を応用する。具体的には、Ｌｙｅｅ要件を対象として、最適化（古典的最適化、述部ベクトルの順序付けによる最適化）、スライシング、要件デバッグ、タイピング（誤り検出、タイプ発見、タイプを用いたセキュリティ）を行う。また、これらをＬｙｅｅＡｌｌツールでの最適化コードの生成に適した前処理を施した形式として要件を出力する。これにより、Ｌｙｅｅ方法論におけるより良い品質（より少ないメモリと実行時間の消費）を有するコード生成のための要件定義の最適化が可能となる。
2004081788.tif 000002
【特許請求の範囲】
【請求項１】
Ｌｙｅｅ方法論に則ってソフトウェアを生産するために単語ごとの定義式を含む要求定義を得るステップと、
前記得られた要求定義を単語をキーにして定数を検出するステップと、
前記検出された定数を使用する定義式に沿って該定数を伝播させるステップと
を具備することを特徴とするＬｙｅｅ指向ソフトウェアに関する静的分析方法。
【請求項２】
Ｌｙｅｅ方法論に則ってソフトウェアを生産するために単語ごとの定義式を含む要求定義を得るステップと、
前記得られた要求定義中の定義式からパターンを検出するステップと、
前記要求定義を該検出されたパターンを置換式とする表現で置きかえるステップと
を具備することを特徴とするＬｙｅｅ指向ソフトウェアに関する静的分析方法。
【請求項３】
Ｌｙｅｅ方法論に則ってソフトウェアを生産するために単語ごとの定義式及び前提条件を含む要求定義を得るステップと、
前記要求定義に基づき、少なくとも前記単語に係る識別子、前記定義式及び前提条件をＢＮＦ文法を遵守して記述した宣言を得るステップと、
前記得られた宣言ごとにＤｅｆ／Ｕｓｅ関数を定義するステップと、
前記定義されたＤｅｆ／Ｕｓｅ関数間の順序関係から前記宣言間の順序関係を得るステップと
を具備することを特徴とするＬｙｅｅ指向ソフトウェアに関する静的分析方法。
【請求項４】
Ｌｙｅｅ方法論に則ってソフトウェアを生産するために単語ごとの定義式及び入出力属性を含む要求定義を得るステップと、
前記要求定義に基づき、少なくとも前記単語に係る識別子、前記定義式及び入出力属性を記述した宣言を得るステップと、
前記得られた宣言（第１の宣言）から、該宣言に係る単語の定義に貢献する別の宣言（第２の宣言）を導き、該第１及び第２の宣言を同一宣言群とするスライス関数を当該総ての宣言に対して実行するステップと、
前記スライス関数から互いに独立なスライスを得るステップと
を具備することを特徴とするＬｙｅｅ指向ソフトウェアに関する静的分析方法。
【請求項５】
Ｌｙｅｅ方法論に則ってソフトウェアを生産するために単語ごとの定義式及び入出力属性を含む要求定義を得るステップと、
前記要求定義に基づき、少なくとも前記単語に係る識別子、前記定義式及び入出力属性を記述した宣言を得るステップと、
前記得られた宣言についての所定の分析に基づき前記要求定義中のバグを検出するステップと
を具備することを特徴とするＬｙｅｅ指向ソフトウェアに関する静的分析方法。
【請求項６】
前記宣言についての所定の分析は、非活性宣言、サイクリック宣言、不完全宣言、もしくは余計宣言の少なくともいずれかを割り出すことによることを特徴とする請求の範囲第５項記載のＬｙｅｅ指向ソフトウェアに関する静的分析方法。
【請求項７】
Ｌｙｅｅ方法論に則ってソフトウェアを生産するために単語ごとの定義式及び入出力属性を含む要求定義を得るステップと、
前記要求定義に基づき、少なくとも前記単語に係る識別子、前記定義式及び入出力属性を記述した宣言を得るステップと、
前記得られた宣言、該宣言中の演算子及びデータに対して各々タイプ代数を定義するステップと、
前記定義されたタイプ代数に対して関連付けられる環境及び所定のタイプ規則を用いて前記要求定義中のタイプ誤りを発見するステップと
を具備することを特徴とするＬｙｅｅ指向ソフトウェアに関する静的分析方法。
【請求項８】
Ｌｙｅｅ方法論に則ってソフトウェアを生産するために単語ごとの定義式及び入出力属性を含む要求定義を得るステップと、
前記要求定義に基づき、少なくとも前記単語に係る識別子、前記定義式及び入出力属性を記述した宣言を得るステップと、
前記得られた宣言、該宣言中の演算子及びデータに対して各々タイプ代数を定義するステップと、
前記定義されたタイプ代数をもとに、所定の環境及びタイプ規則を用いて、前記要求定義中の入力単語から中間介在物及び出力単語のタイプを生成するステップと
を具備することを特徴とするＬｙｅｅ指向ソフトウェアに関する静的分析方法。
【請求項９】
Ｌｙｅｅ方法論に則ってソフトウェアを生産するために単語ごとの定義式及び入出力属性を含む要求定義を得るステップと、
前記要求定義に基づき、少なくとも前記単語に係る識別子、前記定義式、入出力属性及びセキュリティラベルを記述した宣言を得るステップと、
前記得られた宣言中のセキュリティラベル間の関係を示すラチスを用いて、前記単語の値にセキュリティラベルを関連付けるラベル関数を定義するステップと、
前記定義されたラベル関数をもとに、所定のセキュリティ方針を用いて、規定のセキュリティ方針を遵守しないプログラムを割り出すステップと
を具備することを特徴とするＬｙｅｅ指向ソフトウェアに関する静的分析方法。
【発明の詳細な説明】
【技術分野】  本発明は、例えば業務用・個人用などの用途、ビジネスアプリケーション・ゲーム等の種類・内容、ソフトウェア単体・電化製品ＲＯＭ組み込みなどの形態を問わずあらゆる用途、種類・内容、形態におけるソフトウェアに用いることができるソフトウェアの分析方法に係り、特にＬｙｅｅ（登録商標。以下同様）指向ソフトウェアに関する静的分析方法に関する。
【背景技術】  ソフトウェア開発と維持は我々の経済において主要な重要性を持つ活動になった。コンピュータが広範囲に使用されるときには、かかる活動は産業に大きく広範囲にかかわることになる。
毎年、ソフトウェアを開発・維持するために何千億ドルもの巨額の資金が費やされている。今日、ソフトウェア開発分野の参加者同士の競争は以前より激しさを増している。そのレースに残るために、これらの参加者（会社）は生産性を最大限に、費用を最小限に保たなければならない。彼らはまた、高い品質を持つ製品（ソフトウェア）を、時間内に、納入しなければならない。しかしながら、ソフトウェア開発のために現在利用可能なツールと方法論は会社のニーズに正しく適合しているといいきれない部分がある。
基本的に、ソフトウェア研究・開発の目標は、簡単に、すばやく、より品質の高いソフトウェアを構築し得る方法を探すことである。ここ１０年間、さまざまな方法論とテクニックが練られ、提案されてきて、それなりにソフトウェア開発ライフサイクルのステップを改良してきた。
これらは改良についてかなり貢献をしたと認められるにもかかわらず、それらを広範囲に使用するには困難があった。事実上、それらのうち、明確な理解や修正を可能とするシステムが生み出しされたのはほとんどなかったし、それらの使用は依然として、能力、技能、及び知識を幅広く有する専門家のみに勝手がよいと考えられてきたのである。このことは逆に、ソフトウェアの実行には、高給の人材の登用、高価につく維持、及び大規模なチェックを要することを意味する。こういった理由から、企業は現在、新しい有望なソフトウェア開発サイクルの改良方法論に対しては、どんなものであっても十二分に歓迎し、同時に、対価を支払う準備ができている。
Ｌｙｅｅ（「ソフトウェア開発のための統一的方法論」を意味する尾文字語）は新しくて非常に有望な方法論の１つである。異なった分野に関連する広範囲のソフトウェア問題を効率的に扱うことが意図されているＬｙｅｅは、単に所望のソフトウェア開発の要件を定義するだけでソフトウェアを開発することを可能にする。より正確にいえば、ユーザは単に単語、単語についての計算式、その計算の条件（前提条件）、及び画面とプリントアウトのレイアウトを与えるのみで良い（例えば、特許文献１及び２、４乃至６参照。）。
あとは、コンピュータの手にその後のすべての厄介なプログラミング過程（コントロールロジックの側面）を委ねるのである。つまり、ＳＥ（システムエンジニア）などの人間がロジックを設計する必要はない。Ｌｙｅｅは発明後まだ間もないにもかかわらず、その使用の結果は想像を超える可能性を示している。事実上、従来の方法論と比べて、開発時間、維持時間、および文書容量をかなり減少することができる（７０〜８０％）。現在までのところ、要件からコードの自動生成を行う開発者は、ＬｙｅｅＡＬＬと呼ばれる原始的な支援ツールを利用可能である（例えば、特許文献３及び４参照。）。
それにもかかわらず、どんな新しい方法論においてもそうであるように、Ｌｙｅｅについても、その効率を立証し、その良い品質を改良すべく研究が行われなければならない。その上、ＬｙｅｅＡＬＬツールは、更なるユーザフレンドリーを実現するように改良される余地がゼロとはいえない。
一方、ソフトウェアの静的分析手法としては、（１）最適化のテクニック、（２）プログラム・スライシング・テクニック、（３）要件デバッグ、（４）タイピング等がある（非特許文献１及び４参照）。
（１）最適化のテクニック（非特許文献３及び８参照）は、一連の変更を導入することで、コード列の容量、その実行時間、消費メモリ等を短縮する目的で行われるものであるが、Ｌｙｅｅ方法論との組み合わせにおいては、これまでは最適化の対象はＬｙｅｅによってなされたコード列であって、Ｌｙｅｅ要件をその対象とするものは技術的に明確に実現されていなかった（特許文献４参照）。
（２）プログラム・スライシング・テクニックは伝統的なプログラミング言語の中では、プログラム読解とデバッグを「分割して支配する」アプローチとして、長い間、使用されてきた。また、多くのアプリケーションの分析にも首尾よく使用されてきたがこれらのアプリケーションの目標とするのは、結合、アルゴリズムのデバッグ、リバースエンジニアリング、コンポーネント再使用、自動並行化、プログラム統合、および検証補助を測定することなどであり、これまではＬｙｅｅ方法論と組み合わせるという発想がなかった（非特許文献１２参照）。
（３）の要件デバッグはコードが生成される前に要件バグを検出しより有益な結果を得られるものであるが、これまではＬｙｅｅ方法論と組み合わせるという発想はなかった。
（４）のタイプシステム（非特許文献２及び１１参照）はプログラムのいくつかの動的な良い振舞いの特性を静的に保証するのにおいて主に使用され、これによれば、プログラムの実行時に頻繁に起こるエラーを、コンパイル時に検出することができる。また、タイピング技術は、開発されたソフトウェアが何らかのセキュリティ問題に対処するのを確実にするのに首尾よく使用されてきた（非特許文献１１参照）が、これまではＬｙｅｅ方法論と組み合わせるという発想はなかった。
【特許文献１】        国際公開ＷＯ９７／１６７８４  Ａ１パンフレット
【特許文献２】        国際公開ＷＯ９８／１９２３２  Ａ１パンフレット
【特許文献３】        国際公開ＷＯ９９／４９３８７  Ａ１パンフレット
【特許文献４】        国際公開ＷＯ００／７９３８５  Ａ１パンフレット
【特許文献５】        国際公開ＷＯ０２／４２９０４  Ａ１パンフレット
【特許文献６】        日本国特開２００２−２０２８８３号公報
【非特許文献１】      エム・ボツガ、ジェー・ジー・フェルナンデス、エル・ギルブ（Ｍ．Ｂｏｚｇａ，Ｊ．Ｃ．Ｆｅｒｎａｎｄｅｚ，ａｎｄ  Ｌ．Ｇｈｉｒｖｕ）著、「自動テスト生成改良のための静的分析の使用」、２０００年，ｐ．２３５−２５０
【非特許文献２】      エル・カーデリ（Ｌ．Ｃａｒｄｅｌｌｉ）著、「タイプ・システム」、コンピュータサイエンスと工学のハンドブック、第１０３章、ＣＲＣプレス社、１９９７年
【非特許文献３】      ティー・ヘニング（Ｔ．Ｈｅｎｎｉｎｇ）著、「最適化手段」、スプリング・フェアラーク出版、１９７５年
【非特許文献４】      エス・ムヒニック（Ｓ．Ｍｕｃｈｎｉｃｋ）著、「コンパイラデザインの移植」、モーガンコーフマン出版社、カリフォルニア、１９９９年
【非特許文献５】      根来文生著、「Ｌｙｅｅソフトウェアの本質」、２１世紀情報化社会に関する国際会議２０００（ＩＳ２０００）、ｐ．１２１−１８９、２０００年１１月
【非特許文献６】      根来文生著、「Ｌｙｅｅ入門」、ソフトウェア生産技術研究所、東京、日本、２００１年
【非特許文献７】      根来文生、アイ・ハミド（Ｉ．Ｈａｍｉｄ）著、「意思工学の提案」、データベースと情報システムに関する第５回東ヨーロッパ会議研究（ＡＤＢＩＳ’２００１）、２０００年９月
【非特許文献８】      エス・パンデ（Ｓ．Ｐａｎｄｅ）、デー・ピー・アグローワル（Ｄ．Ｐ．Ａｇｒａｗａｌ）著、「スケーラブル平行システムのためのコンパイラ最適化：言語、コンパイルテクニック、および実行時間システム」、スプリンガー・フェアラーク社、２００１年
【非特許文献９】      デー・イー・ラザフォード（Ｄ．Ｅ．Ｒｕｔｈｅｒｆｏｒｄ）著、「格子理論（ラチス理論）への序論」、ハーフネン出版、ニューヨーク、１９６５年
【非特許文献１０】      エフ・チップ（Ｆ．Ｔｉｐ）著、「プログラムスライシング技術に関する調査」、プログラミング言語ジャーナル、３（３）：ｐ．１２１−１８９、１９９５年９月
【非特許文献１１】      デー・ヴォルパノ（Ｄ．Ｖｏｌｐａｎｏ）、ジー・スミス（Ｇ．Ｓｍｉｔｈ）、およびシー・アーバイン（Ｃ．Ｉｒｖｉｎｅ）著、「確実なフロー分析のための静的タイプシステム」、コンピュータセキュリティジャーナル、４（３）：ｐ．１６７−１８７、１９９６年
【非特許文献１２】      ダブリュ・ヴァイザー（Ｗ．Ｗｅｉｓｅｒ）著、「プログラムスライシング」、ＩＥＥＥ  トランス・ソフトウェア・エンジニアリング、ｐ．３５２−３５７、１９８４年７月
このように、簡単に、すばやく、より品質の高いソフトウェアを構築し得る方法として従来よりさまざまな方法論と技術が提案されてき、それなりにソフトウェア開発ライフサイクルのステップを改良してきたが、これらは明確な理解や修正を実現するものではなかったし、それらの使用は、能力、技能、及び知識を幅広く有する専門家のみに勝手がよいものであったので、ソフトウェアの実行には、人件費、ソフトウェア維持費、及びチェック費に大規模な出費を必至ならしめていたという問題があった。
この問題を解決すべくＬｙｅｅと呼ばれる有望な方法論が提案されたが、その効率、品質での研究、更なるユーザフレンドリーの実現のための改良の余地がある。
本発明は上記の従来技術の問題を解決するためになされたものである。具体的には、本発明は、Ｌｙｅｅ方法論におけるより良い品質（より少ないメモリと実行時間の消費）を有するコード生成を助けるＬｙｅｅ指向ソフトウェアに関する静的分析方法を提供することを目的とする。
そのために本発明は、Ｌｙｅｅ要件（それらの定義、それらの計算状態、およびそれらの属性の中の１セットの単語）を分析するために古典的な静的分析のテクニックを用いることでＬｙｅｅ方法論を一層増進させ得る方法を示し、それを実際に利用することが可能なＬｙｅｅ指向ソフトウェアに関する静的分析方法を提供することを更なる目的とする。
さらに本発明は、タイピングと他の静的な分析のテクニックがいかにＬｙｅｅ方法論の何らかの局面を改良することができるかを示し、それを実際に利用することが可能なＬｙｅｅ指向ソフトウェアに関する静的分析方法を提供することをまた別の目的とする。
また本発明は、Ｌｙｅｅ要件分析器、即ち、いくつかの静的分析のテクニックを与えるために開発した原型を提示し、それを実際に利用することが可能なＬｙｅｅ指向ソフトウェアに関する静的分析方法を提供することを更なる目的とする。
さらに本発明は、最終的に、本作業及び今後の研究に関するいくつかの結論的所見を概観し提示し、それを実際に利用することが可能なＬｙｅｅ指向ソフトウェアに関する静的分析方法を提供することをまた別の目的とする。
ここで「Ｌｙｅｅ（登録商標）」とは、本願発明に係る発明者の一人である根来文生により発明されたソフトウェア生産方法等に係る発明、技術のことをいい、その詳細は例えば、上記特許文献１乃至特許文献６等によって規定される諸国際公開公報等に開示されている。
【発明の開示】
本発明は上記目的を達成するために、Ｌｙｅｅ方法論に則ってソフトウェアを生産するために単語ごとの定義式を含む要求定義を得るステップと、該得られた要求定義を単語をキーにして定数を検出するステップと、該検出された定数を使用する定義式に沿って該定数を伝播させるステップとを具備する。
「定数を伝播させる」とは、要求定義（Ｌｙｅｅ要件）中の単語に定数がある場合に、かかる定数をその単語に代入し、この単語を用いた定義式を有する単語に代入し、と連綿と代入してゆくことで単語ごとの定義式を整理することをいう。
かかる本発明では、Ｌｙｅｅによるソフトウェア生産の前段階であるＬｙｅｅ要件に対して最適化を施すので、Ｌｙｅｅ方法論によるソフトウェア生成においてコード列の容量の軽減、消費メモリの軽減、プログラム実行時間の更なる軽減が達成される。
さらに本発明は、Ｌｙｅｅ方法論に則ってソフトウェアを生産するために単語ごとの定義式を含む要求定義を得るステップと、該得られた要求定義中の定義式からパターンを検出するステップと、該要求定義を該検出されたパターンを置換式とする表現で置きかえるステップとを具備する。
「パターンを置換式とする」とは、要件中のパターンが何回も現れる場合に、それを一時的な変数に置きかえることをいう。
かかる本発明では、Ｌｙｅｅ要件の複数回出現パターンをたった一回のみ計算し何回も計算されることをなくすので、コードの実行時間の減少が達成される。
また、本発明は、Ｌｙｅｅ方法論に則ってソフトウェアを生産するために単語ごとの定義式及び前提条件を含む要求定義を得るステップと、該要求定義に基づき、少なくとも前記単語に係る識別子、定義式及び前提条件をＢＮＦ文法を遵守して記述した宣言を得るステップと、該得られた宣言ごとにＤｅｆ／Ｕｓｅ関数を定義するステップと、該定義されたＤｅｆ／Ｕｓｅ関数間の順序関係から前記宣言間の順序関係を得るステップとを具備する。
「宣言」とは、要件中の単語とそれに対する定義式、前提条件、入出力属性等を１つの関数的表現としたものである。また、「Ｄｅｆ／Ｕｓｅ関数」とは、かかる宣言ごとに被定義単語を表現した関数、該被定義単語を定義するために用いる他単語を表現した関数である。
かかる本発明では、Ｌｙｅｅ要件中の単語とその定義式等を宣言の形態に変換・分析する結果Ｌｙｅｅ基底論理中の述部ベクトルの最も良い（即ち、実行時間が減少される）組み合わせを知ることができるので、例えば要件からコードを生成するツール（ＬｙｅｅＡｌｌ）と組み合わせることにより、Ｌｙｅｅによるソフトウェア生成における効率化を更に推進することができる。
さらにまた、本発明は、Ｌｙｅｅ方法論に則ってソフトウェアを生産するために単語ごとの定義式及び入出力属性を含む要求定義を得るステップと、該要求定義に基づき、少なくとも該単語に係る識別子、前記定義式及び入出力属性を記述した宣言を得るステップと、該得られた宣言（第１の宣言）から、該宣言に係る単語の定義に貢献する別の宣言（第２の宣言）を導き、該第１及び第２の宣言を同一宣言群とするスライス関数を当該総ての宣言に対して実行するステップと、該スライス関数から互いに独立なスライスを得るステップとを具備する。
「スライス関数」とは、プログラムを特定の計算に関連する宣言に収斂させ、互いに独立的な宣言群ごとに分ける機能を有する関数をいう。
かかる本発明では、互いに独立なスライス群を並行実行し得るので、実行時間の縮減、特に宣言数の多いときでも要件定義の把握における誤りの縮減を達成できる。
また、本発明は、Ｌｙｅｅ方法論に則ってソフトウェアを生産するために単語ごとの定義式及び入出力属性を含む要求定義を得るステップと、該要求定義に基づき、少なくとも前記単語に係る識別子、該定義式及び入出力属性を記述した宣言を得るステップと、該得られた宣言についての所定の分析に基づき前記要求定義中のバグを検出するステップとを具備する。
「要求定義中のバグを検出する」には、例えば宣言についてのルールを用いることで、非活性宣言、サイクリック宣言、不完全宣言、余計宣言等を発見することをいう。もちろん、バグ検出にはこれらの宣言に限定されるものではなく、他の宣言を対象とすることも可能である。
かかる本発明では、Ｌｙｅｅ方法論におけるシナリオ関数実行において、実際上実行されないサブプログラムに制御が移るのを防止し得るので、処理時間の軽減、消費メモリの効率化等が達成される。
さらに、本発明は、Ｌｙｅｅ方法論に則ってソフトウェアを生産するために単語ごとの定義式及び入出力属性を含む要求定義を得るステップと、該要求定義に基づき、少なくとも前記単語に係る識別子、該定義式及び入出力属性を記述した宣言を得るステップと、該得られた宣言、該宣言中の演算子及びデータに対して各々タイプ代数を定義するステップと、該定義されたタイプ代数に対して関連付けられる環境及び所定のタイプ規則を用いて前記要求定義中のタイプ誤りを発見するステップとを具備する。
「タイプ代数」とは、要件から生成する宣言に係る単語、定義式等にタイプの概念を導入し、タイプの異なるものを同格に扱おうとするものをエラーとして要件段階で排除する操作を数式的に行うために導入する概念である。
かかる本発明では、Ｌｙｅｅ要件を対象としてタイプ的に分析を行い、タイプ規則を用いて要件中の誤りを発見するので、プログラムエラーの軽減を更に促進できる。
また、本発明は、Ｌｙｅｅ方法論に則ってソフトウェアを生産するために単語ごとの定義式及び入出力属性を含む要求定義を得るステップと、該要求定義に基づき、少なくとも前記単語に係る識別子、該定義式及び入出力属性を記述した宣言を得るステップと、前記得られた宣言、該宣言中の演算子及びデータに対して各々タイプ代数を定義するステップと、該定義されたタイプ代数をもとに、所定の環境及びタイプ規則を用いて、該要求定義中の入力単語から中間介在物及び出力単語のタイプを生成するステップとを具備する。
かかる本発明では、入力単語から予め出力単語や中間介在物のタイプを唯一的に導出するので、ユーザ作業の簡素化、誤りの減少を達成できる。
さらに、本発明は、Ｌｙｅｅ方法論に則ってソフトウェアを生産するために単語ごとの定義式及び入出力属性を含む要求定義を得るステップと、該要求定義に基づき、少なくとも該単語に係る識別子、該定義式、入出力属性及びセキュリティラベルを記述した宣言を得るステップと、該得られた宣言中のセキュリティラベル間の関係を示すラチスを用いて、該単語の値にセキュリティラベルを関連付けるラベル関数を定義するステップと、該定義されたラベル関数をもとに、所定のセキュリティ方針を用いて、規定のセキュリティ方針を遵守しないプログラムを割り出すステップとを具備する。
「セキュリティラベル」とは、ある情報についてのセキュリティ要件（例えば、「公開の」、「秘密の」等）を表すラベルである。「ラベル関数」は、要件中の単語に対してかかるセキュリティラベルを与え、これを数式的に処理するための関数である。また、「セキュリティ方針」とは、ユーザサイドで自由に規定し得る、あるセキュリティラベルを持った情報はどう扱うかを定めた指針をいう。
かかる本発明では、上述のタイピング技術を情報セキュリティにも拡大することで、セキュリティ違反を発生させる余地のある設計上の欠陥を明確にするのに役立つ自動的プログラム検証を達成できる。
本発明はまた、Ｌｙｅｅ方法論に則ってソフトウェアを生産するために単語ごとの定義式及び前提条件を含む要求定義を受け取る要求定義受取部と、該受け取られた要求定義からこれに含まれる語彙及び構文を分析し中間的表現を出力する分析部と、該出力された中間的表現から始めて該要求定義に対してデータフロー及び制御フローに関する分析を行いデータフロー図及び制御フロー図を出力するフロー分析部と、該フロー分析を経た要求定義に対して最適化を施し改善された規約を出力する最適化部とを具備するように構成することも可能である。
この場合の「要求定義受取部」とは、本願によるいわば加工を施される前のＬｙｅｅ要件（要求定義）を入力される機能を有する単位をいい、例えば、当該機能をプログラム化して実行可能な形式にしたものを登載した記録媒体やＲＯＭ等として実現することができる。
「分析部」とは、受け取った当該要求定義から語彙及び構文を抽出し分析したのち、当該要求定義を構文状の中間的表現として出力する機能を有する単位をいい、例えば、当該機能をプログラム化して実行可能な形式にしたものを登載した記録媒体やＲＯＭ等として実現することができる。
「フロー分析部」とは、中間的表現から始めて、１要件ポイントから別の１ポイントまで至るデータフロー制御の循環に関係あるすべての情報を、例えば制御フロー図（Ｃｏｎｔｒｏｌ  Ｆｌｏｗ  Ｇｒａｐｈ：ＣＦＧ）及びデータ・フロー図（Ｄａｔａ−Ｆｌｏｗ  Ｇｒａｐｈ：ＤＦＧ）等として出力する機能を有する単位をいい、例えば、当該機能をプログラム化して実行可能な形式にしたものを登載した記録媒体やＲＯＭ等として実現することができる。
「最適化部」とは、例えば定数伝播技術を実行し、ＬｙｅｅＡｌｌツールが、より速く実行でき消費するメモリがより少ないプログラムを生成するのに適する、規則正しくて簡易化された宣言の系列を生産する機能を有する単位をいい、例えば、当該機能をプログラム化して実行可能な形式にしたものを登載した記録媒体やＲＯＭ等として実現することができる。
「スライサ」とは、フローベース分析要素及びスライシング評価基準によって生み出されるフローに関する（各単語に関連づけられるＤｅｆ／Ｕｓｅなどの）情報を受け取り、これらの与えられた評価基準に対応するスライスを出力として与える機能を有する単位をいい、例えば、当該機能をプログラム化して実行可能な形式にしたものを登載した記録媒体やＲＯＭ等として実現することができる。
したがって本発明によれば、上述のそれぞれの機能を実現可能単位の例えば媒体としたので、入力としてＬｙｅｅ要件をうけ取り、ＬｙｅｅＡｌｌツールでの最適化コードの生成に適したスライスと順序を整えられた要件を出力として与えること、さらに、定数伝播などの他の要件最適化を実行することが可能となる。
また、本発明は、ソフトウェア分析方法としてのみならず、ソフトウェア分析装置、あるいは広くソフトウェア開発方法、ソフトウェア開発装置、及び、これらをコンピュータに実施させるためのソフトウェア、当該ソフトウェアを記録した記録媒体、当該ソフトウェアを搭載した装置、当該ソフトウェアを例えばＲＯＭ等に格納した専用マシン、あるいはこれらを業務形態として実行するビジネスモデル等としても実現可能であり、本発明はこれらの実現形態を含むものである。
【図面の簡単な説明】  第１図は、本発明に係るＬｙｅｅ方法論における要件実行をコード列で表した概念図である。
第２図は、本発明に係るＬｙｅｅ方法論におけるパレットの概念を説明するための概念図である。
第３図は、本発明に係るＬｙｅｅ方法論におけるシナリオ関数の概念を説明するための概念図である。
第４図は、本発明に係るＬｙｅｅ方法論における述部ベクトルの動的構造を示すフローチャートである。
第５図は、本発明に係るＬｙｅｅ方法論におけるＬ４，ａ、およびＬ４，ｂの述部ベクトルの動的構造を示すフローチャートである。
第６図は、本発明に係るＬｙｅｅ方法論におけるＬ３，ａ、およびＬ３，ｂの述部ベクトルの動的構造を示すフローチャートである。
第７図は、本発明に係るＬｙｅｅ方法論における画面の相互作用を概念的に説明するための概念図である。
第８図は、本発明に係るＬｙｅｅ方法論における処理経路図の概念を説明するための概念図である。
第９図は、本発明一実施形態に係るＵｓｅＤｉｒｅｃｔＡｎｄＩｎｄｉｒｅｃｔ（ｓ，Ｓ）のアルゴリズムを説明するためのフローチャートである。
第１０図は、本発明一実施形態に係る循環宣言文を検出するアルゴリズムを説明するためのフローチャートである。
第１１図は、本発明一実施形態に係る不完全宣言文を検出するアルゴリズムを説明するためのフローチャートである。
第１２図は、本発明一実施形態に係る不要宣言文を検出するアルゴリズムを説明するためのフローチャートである。
第１３図は、本発明一実施形態に係る不要宣言文を検出するアルゴリズムを説明するためのフローチャートである。
第１４図は、本発明一実施形態に係る、２つのうち先行実行すべき宣言文を検出するアルゴリズムを説明するためのフローチャートである。
第１５図は、本発明一実施形態に係る宣言文の順序を整序するアルゴリズムを説明するためのフローチャートである。
第１６図は、本発明一実施形態に係る宣言文の順序を整序するアルゴリズムを説明するためのフローチャートである。
第１７図は、本発明一実施形態に係る単語ａのスライスを抽出するアルゴリズムを説明するためのフローチャートである。
第１８図は、本発明一実施形態に係る単語ａのスライスを抽出するアルゴリズムを説明するためのフローチャートである。
第１９図は、本発明一実施形態に係る独立したスライスを検出するアルゴリズムを説明するためのフローチャートである。
第２０図は、本発明一実施形態に係るタイピングのアルゴリズムを説明するためのフローチャートである。
第２１図は、本発明一実施形態に係るタイピングのアルゴリズムを説明するためのフローチャートである。
第２２図は、本発明一実施形態に係るタイピングのアルゴリズムを説明するためのフローチャートである。
第２３図は、本発明一実施形態に係るタイピングのアルゴリズムを説明するためのフローチャートである。
第２４図は、本発明一実施形態に係るタイピングのアルゴリズムを説明するためのフローチャートである。
第２５図は、本発明一実施形態に係るタイピングのアルゴリズムを説明するためのフローチャートである。
第２６図は、本発明の一実施形態に係るＬｙｅｅ要件分析器の動的構造を説明するための機能ブロック兼フローチャートである。
発明の概要
本発明の基本となる考え方は、Ｌｙｅｅと呼ばれる開発方法論であり、これについては、上記の特許文献１乃至特許文献６等で開示されているものである。
ソフトウェアシステムの研究と開発の過程で最も問題の多いタスクの１つは要件を十分に理解しそれを正しくそれらをコードに変えることである。この問題を解決するために、Ｌｙｅｅ方法論では、要件からプログラムを発生させる簡単な方法が提案されている。
Ｌｙｅｅ方法論の背景にある哲学的な原則については上記の文献によるものとし、以下では、図面・表を参照し、この方法論を使用することでソフトウェアを書く方法とその方法によって要件から自動的に生成されたコードどう見るかを理解するために役に立ついくつかの実用的なアイデアだけに焦点を合わせて説明する。
（１）Ｌｙｅｅ要件
Ｌｙｅｅ方法論では、要件は、複数の宣言（文）（ｓｔａｔｅｍｅｎｔｓ）の集合として宣言的方法で与えられる。宣言は、単語、それに伴う単語の定義、計算条件と属性（インプット／アウトプット、タイプ、セキュリティ属性など）を含んでいる。
単純化のために、本明細書では、各宣言は次の１）から５）の情報を含むとみなす。
１）単語（Ｗｏｒｄ）
単語の識別子
２）定義（Ｄｅｆｉｎｉｔｉｏｎ）：単語を定義する式。単純化のため、式とは以下のいずれか１つでありえると考える。
2004081788.tif 000003
上記に示した式Ｅｘｐの定義は以下のとおりである。
・Ｅｘｐ：
式「Ｅｘｐ」（式）、値「ｖａｌ」、識別子「ｉｄ」、カッコ付けされた式「（Ｅｘｐ）」、後ろに式が続く単項演算子「ｏｐ  Ｅｘｐ」（例えば−２、−（ａ＋ｂ））、あるいは、他の式を伴う二項演算子が続く式「Ｅｘｐ  ｏｐ  Ｅｘｐ」である。
・ｖａｌ：
値「ｖａｌ」は、数値「ｎｕｍ」、浮動小数点値「ｎｕｍ．ｎｕｍ」（数値．数値）、あるいはブール値（真偽値）「ｂｏｏｌ」である。
・ｎｕｍ：
数値「ｎｕｍ」は、数字（ｄｅｇｉｔ）か、もう１つの数値が後ろに続く数値「ｎｕｍ．ｎｕｍ」である。
・ｂｏｏｌ：
ブール値は、真（ｔｒｕｅ）、あるいは偽（ｆａｌｓｅ）である。
・ｉｄ：
識別子「ｉｄ」は文字、文字の後に数値が続く「ｉｄ  ｎｕｍ」、あるいは識別子の後ろに識別子が続く「ｉｄ  ｉｄ」である。
・ｏｐ：
演算子は＋、−、＊、ｏｒ、ａｎｄ、＜、＜＝、＝、＜＞、＞、＞＝またはｎｏｔである。
２）条件（Ｃｏｎｄｉｔｉｏｎ）
条件とは、単語の計算条件で、ブール演算子と見なされる式Ｅｘｐである。もし条件がない（すなわち条件が常に真）なら、この項目は空欄のままにしておく。
３）ＩＯ
この項目は定義された単語が入力単語、出力単語あるいは中間単語（ｉｎｔｅｒｍｅｄｉａｔｅ  ｗｏｒｄ）であることを明示するために割り当てる。もし単語が入力であって、それがファイルからの入力であるなら、この項目は値ＩＦとなり、もし単語が画面からの入力であるならＩＳとなる。同様に、もし単語が出力であるなら、この欄は値ＯＦ（ファイルへの出力の場合）またはＯＳ（画面への出力の場合）となる。しかしながら、もし単語が中間単語なら、この欄を空欄のままにしておく。中間単語とは、入力ではなく、かつ、定義の式によって生成された値は出力されず、生成された値が他の出力単語の値の生成にのみ寄与する単語である。
４）タイプ（Ｔｙｐｅ）
この項目は単語のタイプを指定するために割り当て、整数「ｉｎｔ」、浮動小数点数「ｆｌｏａｔ」あるいはブール値「ｂｏｏｌ」のいづれか１つの値をとる。
５）セキュリティ（Ｓｅｃｕｒｉｔｙ）
この項目は、定義された単語のセキュリティレベルを決定するために割り当て、公開「ｐｕｂｌｉｃ」あるいは非公開「ｓｅｃｒｅｔ」のいずれか１つの値をとる。もし定義された単語が入力でないなら、項目「タイプ」と「セキュリティ」は空欄でもよい。同じく、他の種類のタイプと他の種類のセキュリティレベルは容易に拡張して、真のＬｙｅｅ要件を正確に満たすことができる。
表１はＬｙｅｅ要件の例を示す。
2004081788.tif 000004
2004081788.tif 000005
本明細書では、以降、宣言（ｓｔａｔｅｍｅｎｔ）とは、要件表の１行のことを意味する。
例えば、表１で単語ａを定義している宣言（これをｓａと記す）は、表２に記述されたとおりである。
2004081788.tif 000006
本明細書では、以降、もしｓが宣言であるなら、次の定義は以下のような意味で用いる。
１）Ｗｏｒｄ（ｓ）とは、宣言の項目「単語」を意味する。
２）Ｄｅｆｉｎｉｔｉｏｎ（ｓ）とは、宣言の項目「定義」を意味する。
３）Ｃｏｎｄｉｔｉｏｎ（ｓ）とは、宣言の項目「条件」を意味する。
４）ＩＯ（ｓ）とは、宣言の項目「ＩＯ」を意味する。
５）Ｔｙｐｅ（ｓ）とは、宣言の項目「タイプ」を意味する。
６）Ｓｅｃｕｒｉｔｙ（ｓ）とは、宣言の項目「セキュリティ」を意味する。
（２）Ｌｙｅｅプログラムのコード生成
Ｓｗを、単語ｗを定義する宣言とする。伝統的なプログラミング言語では、表１で与えられる要件は、表３で与えられているコードに対応する。Ｌｙｅｅ方法論の中では、ユーザはこれらの定義が実行される順序（制御ロジック）を指定する必要はない。表１では、単語ａが単語ｂを使用して定義されているという事実にもかかわらず、宣言Ｓｂが宣言Ｓａの後に与えられている。Ｌｙｅｅ方法論においては、ソフトウェアの論理部分である制御ロジックが自動的に生成される結果、プログラミングエラーとプログラム時間が劇的に短縮される。
2004081788.tif 000007
表１の要件から、我々はａとｂの値を計算するプログラムを自動的に生成し、それらを出力することができる。ここで図１は、要件が実行に反映される姿をコード列として表現した概念図である。同図に示すように、プログラムは、ある一定のポイントに達するまで、これらの指示を単純に繰り返すのである、すなわち、いかなる繰り返しによっても、図１に示されるいかなる単語の値も変化しない。
その上、表３で与えられている宣言に関連づけられるコードに関する順序を変えても、プログラムの意味が決して変化しない、すなわち、いつも正しい値を単語に関連づける。
次に、Ｌｙｅｅによって要件から自動的に生成されるプログラムの構造と内容に関してより詳しく説明する。Ｌｙｅｅ方法論の中では、１セットの宣言の実行（表１で与えられているもの）は独特の方法で実行される。Ｌｙｅｅは宣言に関連づけられるコードを、図２に示される、Ｌｙｅｅ用語でパレット（Ｗ０２、Ｗ０３、及びＷ０４）と呼ばれる３つの領域上に分配する。
同図に示されるように、Ｗ０２パレットは入力単語を扱う、そして、Ｗ０３パレットは単語の計算条件を算出し、その結果はいくつかの変数（値としてブール値をとる）中に格納される。例えば、単語ａの定義の中で使用された「ｂ＊ｅ＞２」という条件はＷ０３パレットで計算され、真／偽というその結果は「ａ＿ｃｏｎｄ」という別の変数に格納される。最終的に、Ｗ０４パレットは、要件中で与えられている定義に従って単語の計算を行う。また、それは計算された単語の値を出力する。
Ｌｙｅｅでは、Ｗ０４パレットからスタートし、一定ポイントに達するまで、すべての定義された単語についてその値を計算しようとする。Ｗ０４では、単語の値についてこれ以上の進展がないということになったら、制御はＷ０２パレットに移る。自身の番が到来すると、この２番目のパレットは、一定ポイント（新たに取り込める入力が得られない状態）に達するまで欠けている単語を入力しようと繰り返し、ついで制御をＷ０３パレットに移す。最終的に、Ｗ０４パレットの場合と同様に、要件に従って、一定ポイントに達するまで、Ｗ０３パレットは単語の計算条件を算出しようとする。
図３で示されるように、全体の安定状態に達するまでこの全体の過程（Ｗ０４→Ｗ０２→Ｗ０３）は繰り返され、この単位は基本構造（Ｓｃｅｎａｒｉｏ  Ｆｕｎｃｔｉｏｎシナリオ関数）と呼ばれる。図１に示されたプログラムの実行の結果が、図２で示されたプログラムの実行結果と同じになることは容易に考察し得る。
さらにＬｙｅｅは、生成されるべきコードの構造を要件内容とは関係なく一定にする固定構造を持つ簡潔な基準プログラム（Ｌｙｅｅ用語で「基底論理（Ｐｒｅｄｉｃａｔｅ  Ｖｅｃｔｏｒ）」と呼ばれる）を確立した。全体を包括するグローバル・プログラム（ｇｌｏｂａｌ  ｐｒｏｇｒａｍ）は述部ベクトル（ｐｒｅｄｉｃａｔｅ  ｖｅｃｔｏｒ）を単に呼び出すものである。図４はこのような述部ベクトルの構造を示す図である。
同図に示されるように、述部ベクトルの目的とすることろは、パレットによって変る。例えば、Ｗ０４パレットで最初の目的はその計算定義に従って、単語に値を与えることである。例えば図２で示される例に関しては、単語ａと単語ｂの計算に関連づけられる述部ベクトルは図５で示される通りである。なお、図４及び５の各ステップについての詳細な説明は上記特許文献１乃至６の該当箇所によるものとし、ここでは省略する。
当該単語の計算に関してこれ以上の進展がないということになったら、Ｌｙｅｅによって生成されたコードは、次の目的である単語の出力を試みる。値の出力を目的とする述部ベクトルは出力ベクトル（ｏｕｔｐｕｔ  ｖｅｃｔｏｒ）と呼ばれる。Ｗ０２パレットでは、入力単語に値を関連づけることを目的とする２つの述部ベクトルがある。説明を簡潔にするために、入力、出力、およびメモリの初期化を扱う述部ベクトルについては他の詳細説明の中では省略する。最終的に、Ｗ０３パレットでは、述部ベクトルの目的は図６で示されるように、要件の中で指定された前提条件を判定することである。ここでは、同図の各ステップについての詳細な説明は上記特許文献１乃至６の該当箇所によるものとし、省略する。
最終的に、表１で与えられている要件に関連づけられるＬｙｅｅプログラムは表３に示されるようになる。
（３）処理経路図
前セクションで提示された基本構造（Ｓｃｅｎａｒｉｏ  Ｆｕｎｃｔｉｏｎシナリオ関数）は、任意の要件の簡単なケース、特に、すべての入力単語及び出力単語が同一の画面に属して、データベースを使わない場合には、それ自体で完全なプログラムであり得る。しかしながら、データベース、または、相互に繋がりを持つ異なる画面に属する単語を入出力する必要があるときは、状況が少し複雑になり得る。説明を簡潔にするために、以下では画面が複数ある場合のみを取り扱う。例えば、図７に示されるような互いに連結された３つの画面があるとして、ユーザは一の画面から他の画面へと遷移し、これらのいずれにおいてもユーザは、複数の単語を入力し、計算し、出力できるものと仮定する。従ってユーザは、仕様書において、これらの画面がどう結合されるのかを与える必要がある。
2004081788.tif 000008
2004081788.tif 000009
その上、すべての画面上で定義されるすべての単語を計算するためには、１つの基本構造（シナリオ関数）のみを定義するだけでは都合よくない。実際、画面の中には、プログラムの任意の実行においては実行されない画面があるかもしれず、その場合には、それらの画面の単語の値の計算を行うことは時間の無駄になってしまう。このような理由から、Ｌｙｅｅは、各画面を、その画面が実行される場合だけ実行される担当基本構造と関連づけている。画面に関連づけられる基本構造は互いに接続され、いつ画面の１つから別の画面にまで移るかを示す。Ｌｙｅｅ用語で言えば、互いに接続された多数の基本構造が集まって図８に示すような処理経路図（ｐｒｏｃｅｓｓ  ｒｏｕｔｅ  ｄｉａｇｒａｍｓ）を作る。
まとめると、Ｌｙｅｅ方法論では、プログラムは通常多くの処理経路図を含んでいる。それらの処理経路図は、それぞれが１セットの内部連結された基本構造群であり、そして、それぞれの基本構造は内部連結された３つのパレット、Ｗ０２パレット、Ｗ０３パレット、およびＷ０４パレットを含んでいる。
（４）Ｌｙｅｅ方法論の改善点
Ｌｙｅｅ方法論の簡潔さと、Ｌｙｅｅ方法論がソフトウェア開発サイクルのすべてのステップに与えるいくつもの肯定的な影響にもかかわらず、Ｌｙｅｅ方法論は、生成されたコードの容量に関して重要な改善点がある。実際、要件の中で与えられた各単語のそれぞれに対してＬｙｅｅは、いくつかのメモリ領域を割り当てる。メモリとして消費された正確な容量の詳細については、上記の非特許文献６及び７を参照されたい。
以降に、静的分析のテクニックによって、いかにＬｙｅｅプログラムを、より速く動き、かつメモリスペース消費がより少ない等のより優れた品質をもつプログラムに改善するか、を示す。
発明の最良の実施形態
以下、図面を参照してＬｙｅｅ要件に関する静的分析に係る本発明の実施形態を説明する。
ソフトウェアの静的分析（非特許文献１及び４参照）は、プログラムのコードについての検証を実際にプログラムを実行させることなく行うことを一般に意味する。経験が示すところによれば、静的分析のテクニックによって仕様書とコード中の多くの質的属性を制御して、改良することができる。とりわけ、静的分析のテクニックによれば、より速く動き、メモリスペースの消費がより少ないプログラムを作ることができ、プログラムのバグを発見することもできる。静的分析を要件に対して適用すれば、コード生成の前に論理的誤りと欠落箇所を見つけることが可能であり、その結果ユーザは開発及びテストのための貴重な時間を節約できることになる。
本明細書ではＬｙｅｅ要件とその生成コード列の品質を改良することができたいくつかの静的分析のテクニックを示す。
一般に、プログラムの最適化とは、一連の変更を加えることで、コード列のサイズ、その実行時間、消費メモリ等を縮小することである。所与のコード列の最適化が最大の目的であることは明らかであるが、どのような場合においても、初期プログラムの意味論を変更するべきではない。
１．古典的な最適化
本セクションでは、いくつかの古典的な最適化のテクニック（非特許文献３及び８参照）と、これらの最適化がメモリ消費量及びＬｙｅｅプログラムの実行時間に対して与える大きな効果を説明する。
（１−１）定数伝播解析（Ｃｏｎｓｔａｎｔ  Ｐｒｏｇａｇａｔｉｏｎ）
この簡単なテクニックはプログラムにおける定数を検出し、それらを使用する式に沿ってそれらの定数の値を伝播させ、最終的にはこれらの定数をなくしていくのである。例えば、表１の例では、定数伝播前の要件においては、単語ａの定義に定数５が与えられている。単語ｂの定義においては、ａ＋３＊５であるので、ａ＝５を代入することで定数伝播を行うと、単語ｂの定義は定数２０となる。単語ｄの定義はｅ＋ｂ＊ａであるので、ａ＝５、ｂ＝２０を代入して定数伝播すれば、その定義式はｅ＋１００となる。このような定数伝播の結果、初期要件は、表５の「定数伝播解析後」のようになる。定義が定数である宣言は、値を生成する必要がないので、要件から除かれている。
2004081788.tif 000010
（１−２）パターン検出
パターンはプログラムの中で何回も繰り返される準式である。このことは、それぞれの準式が何回も計算されることを意味する。従って、パターンが要件に存在しているならば、一般に、このパターンのそれぞれを、準式が１回のみ計算される一時的な変数に置き替えることによって、それらの関連コードの実行時間を減少させることができる。表６は準式「ｂ＊ｃ」がパターンである例を与える。
2004081788.tif 000011
さて、これらの簡単で古典的な最適化のテクニックの使用がＬｙｅｅによって生成されるコードのメモリスペースと実行時間をどう改良することができるかについて説明する。これらの最適化のテクニックがほとんどすべての利用可能なコンパイラで与えられるのは、よく知られている事実である。その上、Ｌｙｅｅが一般にＣＯＢＯＬなどの高レベルプログラミング言語によってコードを生成するので、人によっては、Ｌｙｅｅの高レベルのコードがいったん生成されれば、低レベルのコードを作成するのに使用されるコンパイラがこれらの最適化をするのだろうと結論を下すかもしれない。しかしながら、この問題を深く研究すると、この結論が完全に真であるというわけではないことが示される。実際、Ｌｙｅｅがコード生成に用いる方法は、これらの古典的な最適化を探索する際のコンパイラの作業を複雑にするかもしれない。
それを確認するために、我々はＣ言語を用いて、簡単な要件を実行する２つのプログラムを書いた。我々はこれらの１つへＬｙｅｅＡＬＬ（登録商標）ツールで生成したものと同様の構造を、２番目のものに通常の構造を、それぞれ与えた。２つのプログラムに対して、コンパイラによってこれらの最適化編集を行った後に、我々は、Ｌｙｅｅ構造を持つプログラムにおいてはコンパイラが定数伝播テクニックを適用することができなかった一方、２番目のプログラムの中ではこの最適化が首尾よく行われたことを発見した。すなわち、いったん要件がユーザによって与えられると、Ｌｙｅｅ方法論の中ではコード生成の前にこれらの最適化のテクニックを使用するのがより有益であってより簡単であると、我々は結論を下した。
２．Ｌｙｅｅ要件静的分析における基本解析
このセクションでは、本明細書で明らかにする静的分析テクニックの大半の説明を単純化するのに非常に有益ないくつかの基本的解析の定義を行う。
（２−１）  Ｄｅｆ／Ｕｓｅ解析
（２−１−１）Ｄｅｆ／Ｕｓｅ解析の非形式的定義
任意のＬｙｅｅ要件における各宣言ｓは、新しい単語を定義するために、定義式、あるいは条件式の中でいくつかの単語を使う。定義式あるいは条件式で使われる単語の集合をＵｓｅ（ｓ）と呼び、新しく定義された単語をＤｅｆ（ｓ）と呼ぶ。
表７はＤｅｆ／Ｕｓｅ概念の具体例である。
2004081788.tif 000012
（２−１−２）Ｄｅｆ／Ｕｓｅの形式的定義
ｓが宣言（ｗｒｄ、Ｄｅｆ、Ｃｏｎｄ、ｉｏ、ｔｙｐｅ、ＳｅｃＴｙｐｅ）だとする。Ｄｅｆ（ｓ）によって表される宣言ｓのＤｅｆは、単にｗｒｄである。そして、Ｕｓｅ（ｓ）で表される宣言ｓのＵｓｅは、次のように定義される。
＜宣言のＵｓｅ＞
2004081788.tif 000013
＜式のＵｓｅ＞
2004081788.tif 000014
上記の定義は次のような意味である。
１）宣言のＵｓｅ
Ｕｓｅ（ｓ）＝Ｕｓｅ（Ｄｅｆ）∪Ｕｓｅ（Ｃｏｎｄ）：宣言ｓの定義および条件で使用される単語（Ｕｓｅ（ｓ））は、その定義の定義と条件で使用される単語（Ｕｓｅ（Ｄｅｆ））、および、その条件の定義と条件で使用される単語（Ｕｓｅ（Ｃｏｎｄ））の和集合である。定義と条件は両方が式であるので、つまり任意の宣言のＵｓｅの定義を完了するには、式のＵｓｅを定義するだけでよい。そのために、式の各種類に対して、そのＵｓｅを明確にしなければならない。
２）式のＵｓｅ
2004081788.tif 000015
式が値（ｖａｌ）なら、そのＵｓｅは空欄である。すなわち、定義および条件で使用されている単語はない。
2004081788.tif 000016
式が識別子（Ｉｄ）なら、そのＵｓｅは識別子それ自身である。
2004081788.tif 000017
式が「Ｏｐ  Ｅｘｐ」（式（Ｅｘｐ）を後に伴う単項演算子（Ｏｐ））の形式なら、そのＵｓｅは式（Ｅｘｐ）に等しい。
2004081788.tif 000018
式が「Ｅｘｐ１  Ｏｐ  Ｅｘｐ２」なら、そのＵｓｅは式１（Ｅｘｐ１）のＵｓｅと式２（Ｅｘｐ２）のＵｓｅの和集合である。
（２−２）直接および間接Ｕｓｅ
前項で述べたように、要件の各宣言ｓは、単語の集合Ｕｓｅ（ｓ）によって定義されるような、いくつかの単語を使う場合がある。この単語の集合を宣言ｓの直接Ｕｓｅと呼ぶ。実際、Ｕｓｅ（ｓ）に属する各単語は、その定義式あるいは条件式の宣言ｓで直接使われているからである。
直接Ｕｓｅの単語以外に、宣言ｓは他の単語を間接的に使う場合もある。例えば、もし宣言ｓが単語「ａ」を直接使い、そして単語「ａ」を定義する宣言が単語「ｂ」を使うなら、その時、宣言ｓは単語ｂを間接的に使っている、と言える。さらに、もし単語ｂを定義している宣言が単語ｃを使うなら、同じく宣言ｓは単語ｃを間接的に使うと言うことができる。
間接Ｕｓｅの概念を明確にするための具体例を表８に示す。
2004081788.tif 000019
表８の例において、単語ｅは入力単語であるので、そのＵｓｅ（直接Ｕｓｅ。以下、直接Ｕｓｅは単に「Ｕｓｅ」と記載する）は空欄で、従って間接Ｕｓｅも空欄である。単語Ｉは、そのＵｓｅである単語ｅが入力単語であってその定義および条件が空欄であるので、間接Ｕｓｅは空欄である。単語ｂは、そのＵｓｅである単語ｉのＵｓｅが単語であるので、間接Ｕｓｅは単語ｅである。単語ｃは、そのＵｓｅである単語ｂのＵｓｅが単語ｉおよびその間接Ｕｓｅが単語ｅであるので、単語ｃの間接Ｕｓｅは、単語ｅおよび単語ｉである。単語ａは、そのＵｓｅである単語ｂのＵｓｅが単語ｉそして間接Ｕｓｅが単語ｅ、そしてもう１つのＵｓｅである単語ｃのＵｓｅが単語ｂそして間接Ｕｓｅが単語ｅと単語ｉであるので、従って単語ａの間接Ｕｓｅは、単語ｅおよび単語ｉである（単語ｂは直接Ｕｓｅであるので、間接Ｕｓｅには加えない）。
下記の関数ＵｓｅＤｉｒｅｃｔＡｎｄＩｎｄｉｒｅｃｔ（ｓ，Ｓ）のアルゴリズムによって、任意のＬｙｅｅ要件Ｓ（宣言の集合）の中の任意の１つの宣言ｓのＵｓｅと間接Ｕｓｅの両方を取得することができる。
2004081788.tif 000020
上記の関数ＵｓｅＤｉｒｅｃｔＡｎｄＩｎｄｉｒｅｃｔ（ｓ，Ｓ）のアルゴリズムの意味は以下の通りである。
ｓは宣言、Ｓは要件である宣言の集合である。変数Ｗ＿Ｏｌｄと変数Ｗ＿Ｎｅｗは単語の集合である。
＜開始＞
変数Ｗ＿Ｏｌｄに、Ｕｓｅ（ｓ）［宣言ｓの直接Ｕｓｅである単語（群）］を記録
変数Ｗ＿Ｏｌｄに、変数Ｗ＿Ｏｌｄの値を記録する
変数Ｆｉｘ＿Ｐｏｉｎｔに、値Ｆａｌｓｅを記録する
＜Ｗｈｉｌｅ文開始＞変数Ｆｉｘ＿Ｐｏｉｎｔの値がＦａｌｓｅである間は下記を実行する
＜Ｆｏｒ文開始＞全ての単語ａについて、要件Ｓに属す宣言ｓのＵｓｅである場合以下を実行する。
変数Ｗ＿Ｎｅｗに、変数Ｗ＿Ｎｅｗに記録された単語（群）、および要件Ｓに属する単語ａの宣言のＵｓｅである単語（群）、を記録する。
＜Ｆｏｒ文終了＞
＜Ｉｆ文開始＞もし、変数Ｗ＿Ｎｅｗの値が変数Ｗ＿Ｏｌｄの値と等しいなら、
変数Ｆｉｘ＿Ｐｏｉｎｔに値Ｔｒｕｅを記録する。
そうでなければ、変数Ｗ＿Ｏｌｄに変数Ｗ＿Ｎｅｗの値を記録する。
＜Ｉｆ文終了＞
＜Ｗｈｉｌｅ文終了＞
＜終了＞
上記アルゴリズムで、関数Ｓｔａｔｅｍｅｎｔ（ａ，Ｓ）は、Ｌｙｅｅ要件Ｓの中の単語ａを定義する宣言を返す関数である。すなわち、Ｄｅｆ（ｓａ）＝｛ａ｝（単語ａの宣言ｓａのＤｅｆは単語ａである、を示す）であるような宣言ｓａ∈Ｓ（要件Ｓに含まれる単語ａの宣言ｓａ）を返す。
上記関数ＵｓｅＤｉｒｅｃｔＡｎｄＩｎｄｉｒｅｃｔ（ｓ，Ｓ）のアルゴリズムをフローチャートに示すと図９のようになる。図９の処理ステップを順に説明すれば、次の通りである。変数Ｗ＿Ｏｌｄの領域にＵｓｅ（ｓ）［宣言ｓの直接Ｕｓｅである単語（群）］の結果を記録し（ステップ１０１）、変数Ｗ＿Ｎｅｗの領域にＷ＿Ｏｌｄの値を複写（ステップ１０２）する。次に領域Ｆｉｘ＿Ｐｏｉｎｔに「偽（ｆａｌｓｅ）」を記録する（ステップ１０３）。
ステップ１０４の条件判定により、Ｆｉｘ＿Ｐｏｉｎｔの値が偽であればステップ１０５に進む。
ステップ１０５で、「Ｕｓｅ（ｓ）の結果と  Ｗｏｒｄ（Ｓ）の結果の和［宣言ｓのＵｓｅと要件Ｓの全宣言の単語］である単語の集合の中に、ステップ１０６の処理が未実行の単語ａがあるか否か」の判定において、結果が真であればステップ１０６に進む。ステップ１０６では、変数Ｗ＿Ｎｅｗの領域に、変数Ｗ＿Ｎｅｗの値とＵｓｅ（Ｓｔａｔｅｍｅｎｔ（ａ，Ｓ））［単語ａの宣言のＵｓｅ］の値を記録する。
ステップ１０６終了後、ステップ１０５に戻り再度判定を実行する。ステップ１０５の判定結果が真である限り、ステップ１０５からステップ１０６の第１の再起処理（１１１）を繰り返す。
ステップ１０５の判定において、結果が偽となったとき、すなわち、Ｕｓｅ（ｓ）の結果とＷｏｒｄ（Ｓ）の結果の和［宣言ｓのＵｓｅと要件Ｓの全宣言の単語］である単語の集合の中に、まだ実行されていない単語ａがなくなったとき、ステップ１０７に進む。ステップ１０７で、「変数Ｗ＿Ｎｅｗの値が変数Ｗ＿Ｏｌｄに等しいか否か」の判定において、結果が偽である場合はステップ１０８に進んで変数Ｗ＿Ｏｌｄの領域に変数Ｗ＿Ｎｅｗの値を複写し、結果が真である場合はステップ１０９に進んで領域Ｆｉｘ＿Ｐｏｉｎｔに真を記録する。ステップ１０８またはステップ１０９終了後、ステップ１０４に戻り再度判定を行る。ステップ１０４の判定結果が真である限り、ステップ１０４からステップ１０９の第２の再起処理（１１２）を繰り返す。
Ｆｉｘ＿Ｐｏｉｎｔの値が真となってステップ１０４の判定結果が偽となったとき、ステップ１０４からステップ１１０に進み、関数ＵｓｅＤｉｒｅｃｔＡｎｄＩｎｄｉｒｅｃｔ（ｓ，Ｓ）の結果として、変数Ｗ＿Ｎｅｗの値を返す。
３．要件デバッグ
（３−１）非活性宣言（Ｄｅａｄ  Ｓｔａｔｅｍｅｎｔｓ）
ある宣言が決して実行されないならば、その宣言は死んでいると考えられる。死んでいる宣言は多くの原因によって起こり得る。知られている原因の多くの１つは、宣言の中の相容れない前提条件の存在である。実際、与えられた宣言に関連づけられる前提条件がいつも誤っているならばこの宣言は意味を持ち得ず、結果として、それに関連づけられる述部ベクトル（ｐｒｅｃｉｄａｔｅ  ｖｅｃｔｏｒｓ）は完全に実行されることは決してない。このことは、一般的に仕様の誤りに由来するので、このことはユーザに伝えられなければならない。この種類の死んでいるコードを検出するためには、宣言に関連づけられる前提条件を分析するだけでよい。与えられた宣言に関連付けられた前提条件が常に偽であると静的に証明することが可能ならば（評価をするに当たって前提条件に用いられている総ての単語の値を得る必要は必ずしもないことに注意されたい。つまり、条件「Φ∧¬Φ」が、Φの値に関係なく常に偽であるなら、この宣言は死んでいるのである。さらにいえば、死んだ宣言を用いている他の宣言は総て、結局は死んでいる。より形式的に表すなら、もし宣言ｓが死んで
2004081788.tif 000021
を表す。）
（３−２）循環宣言（Ｃｙｃｌｉｃ  Ｓｔａｔｅｍｅｎｔｓ）
（３−２−１）循環宣言の非形式的定義
任意の宣言の単語の直接あるいは間接的定義が、その単語自身を含んでいる場合、との宣言は循環（ｃｙｃｌｉｃ）であると言う。言い換えると、任意の単語「ａ」の定義に単語「ａ」が必要となっている場合である。以下に、いくつかの具体的な例を示す。
表９は、単語「ａ」がそれ自身を使って定義されており、直接循環の例である。
2004081788.tif 000022
2004081788.tif 000023
次に間接循環の例を示す。表１０では、単語「ａ」の定義は他の単語以外に単語「ｂ」の定義を必要としている。しかし、単語「ｂ」の定義も単語「ａ」の定義を必要としている。従って、単語「ａ」と単語「ｂ」は間接循環に陥いる。
2004081788.tif 000024
（３−２−２）循環宣言の形式的定義
以下に、循環宣言の形式的定義を示す。Ｓを宣言の集合とすると、下記の条件に合致する時、宣言ｓ∈Ｓ（要件Ｓに属する宣言ｓ）は循環する。
2004081788.tif 000025
すなわち、Ｄｅｆ（ｓ）∈ＵｓｅｄｉｒｅｃｔＡｎｄＩｎｄｉｒｅｃｔ（ｓ，Ｓ）は、「宣言ｓのＤｅｆが、要件Ｓに属する宣言ｓの直接および間接Ｕｓｅに含まれる」ことを形式的に表している。
下記の関数ＣｙｃｌｉｃＳｔａｔｅｍｅｎｔｓ（Ｓ）のアルゴリズムによって、任意のＬｙｅｅ要件Ｓの中の循環宣言を検出することができる。
2004081788.tif 000026
上記の関数ＣｙｃｌｉｃＳｔａｔｅｍｅｎｔｓ（Ｓ）のアルゴリズムの意味は以下の通りである。
Ｓは要件である宣言の集合である。変数ＣｙｃｌｉｃＳｅｔは宣言の集合である。
＜開始＞
変数ＣｙｅｌｉｃＳｅｔに「０」を記録する。
＜Ｆｏｒ文開始＞宣言の集合Ｓに属する総ての宣言ｓに対して、以下を実行する。
＜Ｉｆ文開始＞もし、Ｄｅｆ（ｓ）［宣言ｓの単語］が、ＵｓｅＤｉｒｅｃｔＡｎｄＩｎｄｉｒｅｃｔ（ｓ）［宣言ｓの直接および間接Ｕｓｅ］に含まれるなら、
変数ＣｙｃｌｉｃＳｅｔに、変数ＣｙｃｌｉｃＳｅｔの値と｛ｓ｝［宣言ｓ］を記録する。
＜Ｉｆ文終了＞
＜Ｆｏｒ文終了＞
変数ＣｙｃｌｉｃＳｅｔの値を返す。
＜終了＞
図１０は、この関数ＣｙｃｌｉｃＳｔａｔｅｍｅｎｔｓ（Ｓ）のアルゴリズムをフローチャートに示したものである。図１０の処理ステップを順に説明すれば、次の通りである。まず、変数Ｃｙｃｌｉｃｓｅｔの領域に「０」を記録し（ステップ２０１）、「宣言の集合Ｓの中にステップ２０２の処理が未実行の宣言ｓがあるか否か」の判定を行う（ステップ２０２）。判定が真の場合は、「Ｄｅｆ（ｓ）［宣言ｓの単語］がＵｓｅＤｉｒｅｃｔＡｎｄＩｎｄｉｒｅｃｔ（ｓ）［宣言ｓの直接および間接Ｕｓｅ］に属すか否か」を判定し（ステップ２０３）、判定が真の場合は、変数ＣｙｃｌｉｃＳｅｔの領域にＣｙｃｌｉｃＳｅｔの値と宣言ｓを記録し（ステップ２０４）、ステップ２０２の判定に戻る。ステップ２０３の判定が偽の場合は、直接ステップ２０２のは判定に戻って再度実行する。ステップ２０２の判定が真である限り、ステップ２０２から２０４の再起処理（２０６）を繰り返す。
ステップ２０２の判定結果が偽となった時、ステップ２０５に進み、関数ＣｙｃｌｉｃＳｔａｔｅｍｅｎｔの結果として、変数ＣｙｃｌｉｓＳｅｔの値（宣言の集合）を返す。
循環宣言の検証は、宣言の上になされるべき最初の静的分析でなければならない、という点は重要である。従って、本明細書でこれ以降に述べる静的分析は、分析結果に循環がないとことを前提する。
（３−３）不完全宣言（Ｉｎｃｏｍｐｌｅｔｅ  Ｓｔａｔｅｍｅｎｔｓ）
（３−３−１）不完全宣言の非形式的定義
宣言Ｓの集合（Ｌｙｅｅ要件）は、もしそれが、Ｓの中で直接的あるいは間接的に定義されていない単語を１つ以上使った宣言ｓを、少なくとも１つ含むなら、不完全であると言える。前記定義は、「すべての使用される単語は定義されなければならない」、という原則をとらえている。
表１１は不完全宣言の具体例である。ここで、単語「ａ」は単語「ｉ」を使っているが、単語ｉはまだ定義されていない。
2004081788.tif 000027
不完全宣言の概念の説明を容易にするために、最初に次の表記法を導入する。Ｄｅｆｉｎｅｄ（Ｓ）：
任意の宣言の集合Ｓ（要件Ｓ）があったとき、関数Ｄｅｆｉｎｅｄ（Ｓ）はＳの中で定義済みの単語の集合を返す。より形式的には下記のような表記になる。
2004081788.tif 000028
上記は、関数Ｄｅｆｉｎｅｄ（Ｓ）は、「要件Ｓに属する総ての宣言ｓのＤｅｆの結果である単語の全体集合」であることを表す。ただし、定義済みであるとは、当該単語の宣言が存在することであって、宣言の総ての項目の必要情報が満たされているとは限らない。たとえば、出力単語であるにもかかわらず、定義式や条件式が未定義である場合もある。そのような宣言は、Ｕｓｅ（ｓ）＝｛  ｝となる。不完全宣言には、定義済みであっても定義式および条件式が未定義の入力でない単語の宣言も含まれる。
下記の図を用いて不完全宣言の定義を説明する。
2004081788.tif 000029
Ｘは、要件Ｓの総ての宣言ｓの直接および間接Ｕｓｅである単語の集合である。Ｙは、要件Ｓ中で定義済みの単語の集合である。ＺはＸとＹの積集合、つまり、要件Ｓのいずれかの宣言で使用されており、かつ、定義済みである単語の集合である。Ｗは、要件Ｓの宣言で使用されている単語のうち、要件Ｓで未定義の単語の集合である。Ｑは、「要件Ｓのいずれかの宣言で使用されており、かつ、定義済みである単語の集合である」Ｚのうち、宣言の定義式および条件式が未定義である入力でない単語である。
従って、不完全宣言は、「要件Ｓの宣言で使用されている単語のうち、要件Ｓで未定義の単語の集合」Ｗの宣言と、「要件Ｓのいずれかの宣言で使用されており、かつ、定義済みである単語の集合」Ｚのうち定義式および条件式が未定義である入力でない単語の集合Ｑの宣言、の和である。
図１１は、不完全宣言を抽出するための処理をフローチャートで表したものである。まず、変数ＩｎｃｏｍｐｌｅｔｅＳｅｔ、変数Ｘ、変数ｑのそれぞれに値「０」を記録（ステップ３０１）。次に、ステップ３０２で「要件Ｓ中にステップ３０３の処理を未実行の宣言ｓがあるか否か」を判定する。判定結果が真であれば、ステップ３０３に進み、変数Ｘに変数Ｘの値とＵｓｅＤｉｒｅｃｔＡｎｄｅＩｎｄｉｒｅｃｔ（ｓ，Ｓ）の値を記録する。ステップ３０３終了後、ステップ３０２に戻り再度実行する。ステップ３０２の判定が真である限り、ステップ３０２からステップ３０３の第１の再起処理（３１１）を繰り返す。
ステップ３０２の判定結果が偽となったとき、ステップ３０４に進み、変数Ｙに関数Ｄｅｆｉｎｄｅｄ（Ｓ）［要件Ｓの定義済み単語の集合を返す］の結果を記録し、変数ＺにＸ∩Ｙ［要件Ｓの宣言で使用されている単語であり、かつ、要件Ｓで定義済みである単語、の集合］を記録し、変数ＷにＸ−Ｚ［要件Ｓの宣言で使用されている単語の集合からＺの単語の集合を除いたもの。すなわち、要件Ｓの宣言で使用されている単語であるが、要件Ｓで未定義の単語の集合］を記録する。
次に、ステップ３０５で「要件Ｓの中にステップ３０６の処理を未実行の単語ａがあるか否か」を判定する。判定結果が真であれば、ステップ３０６で「ＩＯ（Ｓｔａｔｅｍｅｎｔ（ａ，Ｓ））≠ＩＳ  ｏｒ  ＩＦ［単語ａは入力でない］、かつ、Ｕｓｅ（Ｓｔａｔｅｍｅｎｔ（ａ，Ｓ））＝｛｝［単語ａの宣言の直接Ｕｓｅが空、すなわち、単語ａの定義式および条件式が未定義］か否か」を判定する。判定結果が真であれば、ステップ３０７で変数ｑに変数ｑの値と単語ａを記録し、ステップ３０５に戻り再度実行する。ステップ３０５の判定が真である限り、ステップ３０５からステップ３０７の第２の再起処理（３１０）を繰り返す。
ステップ３０５の判定が偽となったとき、ステップ３０８に進み、変数ＱにＺ∩ｑ［要件Ｓの宣言で使用されおりかつ定義済みの単語であり（＝Ｚ）、かつ、定義式および条件式が未定義の入力でない単語（＝ｑ）］の値を記録し、変数ＩｍｃｏｍｐｌｅｔｅＳｅｔにＷ∪Ｑ［要件Ｓの宣言で使用されているが未定義の単語（＝Ｗ）と、前記Ｑの単語］の単語全ての宣言を記録する。最後に、要件Ｓの中の不完全宣言として、変数ＩｎｃｏｍｐｌｅｔｅＳｅｔの値を返し（ステップ３０９）、処理を終了する。
（３−４）不要宣言（Ｓｕｐｅｒｆｌｕｏｕｓ  Ｓｔａｔｅｍｅｎｔｓ）
（３−４−１）不要宣言の非形式的定義
任意のＬｙｅｅ要件Ｓの中の宣言ｓが、もしＳのどんな出力単語の定義にも直接または間接に貢献しないならば、その宣言ｓは不要であると考えられる。この定義は、「各定義済みの単語は使用されなければならない」、という原則をとらえている。「使用」とは「出力単語の定義に直接的または間接的に貢献した」ことを意味する。不要の定義と不完全の定義を合わせると次の原則をとらえている：定義したものは全て使用されねばならず、使用するものは全て定義されねばならない。
表１２は不要宣言の具体例である。ここで、単語ｊはどんな出力単語の定義にも直接的あるいは間接的に貢献しない。従って、単語ｊはプログラムの実行に否定的効果をもたらすことなく要件から取り除くことができる。
2004081788.tif 000030
2004081788.tif 000031
不要宣言の概念を形式的に定義するために、次の概念導入する。
ＯｕｔｐｕｔＳｔａｔｅｍｅｎｔｓ（Ｓ）：
任意の宣の集合Ｓがあるとき、関数ＯｕｔｐｕｔＳｔａｔｅｍｅｎｔｓ（Ｓ）は、Ｓの中から、ＯＳあるいはＯＦを入力／出力属性として持つ宣言を返す。形式的表記では以下のよう定義される。
2004081788.tif 000032
上記の形式的表現は、関数ＯｕｔｐｕｔＳｔａｔｅｍｅｎｔｓ（Ｓ）の結果は、「宣言の集合Ｓに属する宣言ｓであって、その宣言ｓは、そのＩＯ（入出力属性）項目の値がＯＳ（画面への出力）またはＯＦ（ファイルへの出力）であるような宣言」であることを意味している。
下記の関数ＯｕｔｐｕｔＳｔａｔｅｍｅｎｔｓ（Ｓ）のアルゴリズムによって、任意のＬｙｅｅ要件Ｓの中から、入力／出力属性が出力（ＯＳまたはＯＦ）である宣言ＯｕｔｐｕｔＳｔａｔｅｍｅｎｔｓを導き出すことができる。
2004081788.tif 000033
上記の関数ＯｕｔｐｕｔＳｔａｔｅｍｅｎｔｓ（Ｓ）のアルゴリズムの意味は以下の通りである。
Ｓは要件である宣言の集合である。変数ＯｕｔｐｕｔＳｅｔは宣言の集合である。
＜開始＞
変数ＯｕｔｐｕＳｅｔの領域に「０」を記録する。
＜Ｆｏｒ文開始＞宣言の集合Ｓに属する全ての宣言ｓについて、以下の処理を行う。
＜Ｉｆ文開始＞もし、宣言ｓのＩＯ［入出力属性］が、ＯＳ［画面への出力］またはＯＦ［ファイルへの出力］である場合は、
変数ＯｕｔｐｕｔＳｅｔの領域に、変数ＯｕｔｐｕＳｅｔの値と宣言ｓを記録する。
＜Ｉｆ文終了＞
＜Ｆｏｒ文終了＞
関数ＯｕｔｐｕｔＳｔａｔｅｍｅｎｔｓ（Ｓ）の結果として、ＯｕｔｐｕｔＳｅｔの値（宣言の集合）を返す。
以上の定義によって、次のセクションに示すような不要宣言の形式的定義が容易になる。
図１２は、この関数ＯｕｔｐｕｔＳｔａｔｅｍｅｎｔｓ（Ｓ）のアルゴリズムをフローチャートに示したものである。図１２の処理を説明すると以下のようになる。まず、変数ＯｕｔｐｕｔＳｅｔの領域に「０」を記録する（ステップ４０１）。次に、ステップ４０２で「宣言の集合Ｓの中に、ステップ４０３の処理が未実行の宣言ｓがあるか否か」を判定する。ステップ４０２の判定結果が真の場合、ステップ４０３に進み、「宣言ｓのＩＯ［入出力属性］がＯＳ［画面への出力］、または、ＯＦ［ファイルへの出力］であるか否か」を判定する。ステップ４０３の判定結果が真の場合は、変数ＯｕｔｐｕｔＳｅｔの領域に変数ＯｕｔｐｕｔＳｅｔの値と宣言ｓを記録して、ステップ４０２に戻る。ステップ４０３の判定結果が偽の場合は、直接ステップ４０２に戻って再度実行する。ステップ４０２の判定結果が真である限り、ステップ４０２から４０４の再起処理（４０６）を繰り返す。
ステップ４０２の結果が偽となったら、関数ＯｕｔｐｕｔＳｔａｔｅｍｅｎｔの結果として、ＯｕｔｐｕｔＳｅｔの値（宣言の集合）を返す。
（３−４−２）不要宣言の形式的定義
不要宣言の形式的定義について述べる。Ｓを宣言の集合であるとすると、Ｓの中の不要宣言は、ＳｕｐｅｒｆｌｕｏｕｓＳｔａｔｅｍｅｎｔｓ（Ｓ）によって示されて、形式的には次のように定義される。
2004081788.tif 000034
上記の形式的表記は、関数ＳｕｐｅｒｆｌｕｏｕｓＳｔａｔｅｍｅｎｔｓ（Ｓ）の結果は、「宣言の集合Ｓから、Ｓに属す総ての宣言ｓの直接および間接Ｕｓｅに属す総ての単語の宣言の集合であって、Ｓの出力単語の宣言であるような宣言の集合を、除いた結果である宣言の集合」であることを意味する。
下記の関数ＳｕｐｅｒｆｌｕｏｕｓＳｔａｔｅｍｅｎｔｓ（Ｓ）のアルゴリズムによって、任意のＬｙｅｅ要件Ｓの中の不要宣言を検出することができる。
2004081788.tif 000035
上記の関数ＳｕｐｅｒｆｌｕｏｕｓＳｔａｔｅｍｅｎｔｓ（Ｓ）のアルゴリズムの意味は以下の通りである。
Ｓ要件である宣言の集合である。変数ＳｕｐｅｒｆｌｕｏｕｓＳｔａｔＳｅｔ、変数ＩｍｐｏｒｔａｎｔＳｔａｔＳｅｔ、変数ＯｕｔｐｕｔＳｔａｔＳｅｔは宣言の集合である。
＜開始＞
変数ＯｕｔｐｕｔＳｔａｔＳｅｔの領域に関数ＯｕｔｐｕｔＳｔａｔｅｍｅｎｔｓ（Ｓ）［要件Ｓに属す全ての出力の宣言］の結果を記録する。
変数ＩｍｐｏｒｔａｎｔＳｔａｔｓｅｔに「０」を記録する。
＜Ｆｏｒ文開始＞ＯｕｔｐｕｔＳｔａｔＳｅｔに属する全ての宣言ｓについて以下の処理を実行する。
＜Ｆｏｒ文開始＞ＵｓｅＤｉｒｅｃｔＡｎｄＩｎｄｉｒｅｃｔ（ｓ，Ｓ）［要件Ｓ中の宣言ｓの直接および間接Ｕｓｅ］に属する全ての単語ａについて以下の処理を実行する。
変数ＩｍｐｏｒｔａｎｔＳｔａｔＳｅｔの領域に、変数ＩｍｐｏｒｔａｎｔＳｔａｔＳｅｔの値と単語ａの宣言を記録する。
＜Ｆｏｒ文終了＞
＜Ｆｏｒ文終了＞
変数ＳｕｐｅｒｆｌｕｏｕｓＳｅｔの領域に、要件Ｓから変数ＩｍｐｏｒｔａｎｔＳｔａｔＳｅｔの値を除い宣言の集合を記録する。
結果として、変数ＳｕｐｅｒｆｌｕｏｕＳｅｔの値を返す。
＜終了＞
図１３は、この関数ＳｕｐｅｒｆｌｕｏｕｓＳｔａｔｅｍｅｎｔｓ（Ｓ）のアルゴリズムをフローチャートに示したものである。図１３の処理を説明すると以下のようになる。まず、変数ＯｕｔｐｕｔＳｔａｔＳｅｔの領域に関数ＯｕｔｐｕｔＳｔａｔｅｍｅｎｔｓ（Ｓ）［要件Ｓに属す全ての出力の宣言］の結果を記録し、変数ＩｍｐｏｒｔａｎｔＳｔａｔｓｅｔに「０」を記録する（ステップ５０１）。次に、「変数ＯｕｔｐｕｔＳｔａｔＳｅｔの中にステップ５０３を未実行の宣言ｓがあるか否か」を判定する（ステップ５０２）。ステップ５０２の結果が真である場合は、ステップ５０３の判定「ＵｓｅＤｉｒｅｃｔＡｎｄＩｎｄｉｒｅｃｔ（ｓ，Ｓ）［宣言ｓの直接および間接Ｕｓｅ］にの中でステップ５０４が未実行の単語ａがあるか否か」を行う。ステップ５０３の結果が真の場合は、ステップ５０４に進み、変数ＩｍｐｏｒｔａｎｔＳｔａｔＳｅｔの領域に、変数ＩｍｐｏｒｔａｎｔＳｔａｔＳｅｔの値とＳｔａｔｅｍｅｎｔ（ａ，Ｓ）［単語ａの宣言］の結果を着ろする。ステップ５０４が終了した後、ステップ５０３に戻り再度実行する。ステップ５０３の判定結果が真である限り、ステップ５０３から５０４の第１の再起処理を繰り返す。
ステップ５０３の結果が偽となったとき、ステップ５０２に戻り再度実行する。ステップ５０３の結果が偽である限り、ステップ５０２からステップ５０４の第２の再起処理を繰り返す。
ステップ５０３の結果が偽となったとき、ステップ５０５に進み、変数ＳｕｐｅｒｆｌｕｏｕｓＳｅｔの領域に、要件Ｓから変数ＩｍｐｏｒｔａｎｔＳｔａｔＳｅｔの値を除いた宣言の集合を記録し、ステップ５０６において関数Ｓｕｐｅｒｆｏｕｏｕｓｓｔａｔｅｍｅｎｔｓ（Ｓ）の結果として変数ＳｕｐｅｒｆｌｕｏｕｓＳｅｔの値を返す。
４．宣言列の最適順付け
（４−１）述部ベクトルの順序付けによる最適化
前述したように、Ｌｙｅｅ方法論の中ではユーザが自身の要件の宣言を入力する順序は、それらに関連づけられるプログラムの意味論（実行の結果）にどんな影響も与えない。そして、この事実はこの方法論の大きな貢献の１つである。それにもかかわらず、我々がこれらの宣言に関連づけられる述部ベクトルを作成する順序は生成されるコードの効率（実行時間）にかなりの影響力を持っている可能性がある。具体的な例でこの問題についてさらに説明する。表１３のような初期要件が与えられた場合を仮定する。
2004081788.tif 000036
また、これらの各宣言に関連づけられて生成されたＷ０４パレットの述部ベクトルが表１４の（ａ）に示されるような順番であると仮定する。（たとえば、Ｌ４ａは、単語ａの述部ベクトルである。）
2004081788.tif 000037
表１４の（ａ）のプログラムが必要とする実行時間について簡潔に説明すると以下のようになる。初期化ベクトル（Ｓ４）がいったん実行された後、最初の繰り返しでは、プログラムはＬ４ａを実行して単語ａに値を与えるべく試みるが、値を得ることに失敗する。なぜなら、単語ａの計算は、まだ値が計算されていない単語ｂを必要とするからである。従って、この１番目の繰り返しでは、単語ｄを除き、任意の単語に値を与える試みは失敗する。２番目の繰り返しでは、プログラムは単語ｃに値を割り当てることに成功する。３番目の繰り返しにおいては、単語ｂの値が計算され、最終的に４番目の繰り返しにおいて単語ａの値が算出される。要するに、このプログラムは、すべての単語の値を算出するために４回の繰り返しを必要とする。
しかしながら、表７の（ａ）のプログラムを、表７の（ｂ）のプログラムによって置き換えると、すべての単語に値を与えるのに必要である繰り返しの数は抜本的に減少することになる。事実上、たった１回の繰り返しのみで、プログラムは、すべての指定された単語について値を計算し得る。これらのことから、述部ベクトルの実行順序がプログラムの実行時間に深い効果を与えると結論付けられる。結果的に、Ｌｙｅｅ要件からコードを生成するツール（たとえばＬｙｅｅＡＬＬ）に対し、実行時間を減少させるように述部ベクトルを並べるよう指示することは有益となろう。幸い、述部ベクトルの最適順列は自動的かつ静的に生成することができる。すなわち、Ｌｙｅｅ要件の宣言列に対して、最適順列への並びかえを行うのである。
（４−２）最適順序付けの非形式的定義
以下に、最適順序付けされた宣言列の意味を、非形式的に定義する。宣言列Ｓは、もし各単語の定義が宣言列Ｓの中で自身の使用の前に現われるなら、最適順序だと言える。宣言の条件は、任意の単語を定義している宣言は、宣言列Ｓの中で、その宣言を使用しているすべての宣言より前に現われなければならない、ということである。
表１５は順序付けされていない宣言列の具体例である。
2004081788.tif 000038
一方、表１６は順序付けされた後の宣言列である。
2004081788.tif 000039
2004081788.tif 000040
順序付けの概念を形式的に定義するために、次の関数の概念を導入する。
１）Ｆｉｒｓｔ
任意の宣言の順列＜ｓ１．．．，ｓｎ＞があるとき、関数Ｆｉｒｓｔはこの順列の最初の要素であるｓ１を返す。
２）ＡｄｄＦｉｒｓｔ
任意の宣言の順列＜ｓ１．．．，ｓｎ＞と宣言ｓ０があった時、関数ＡｄｄＦｉｒｓｔは＜ｓ０，１．．．，ｓｎ＞を返し、すなわち、それは最初の順列の頭にｓ０を加えることである。
３）Ｒｅｍｏｖｅ
任意の宣言の順列Ｓと宣言ｓがあったとき、関数ＲｅｍｏｖｅはＳから、ｓと等しい宣言を取り除く。（Ｓは何度も同じ宣言文を含んでいないと仮定する）。
４）Ｌｏｗｅｒ
任意の２つの宣言ｓとｓ’があった時、もしＤｅｆ（ｓ）∈Ｕｓｅ（ｓ’）なら、Ｌｏｗｅｒ（ｓ，ｓ’）は真である。下記の関数Ｌｏｗｅｒ（ｓ，ｓ’）のアルゴリズムがこのＬｏｗｅｒの定義を捉えている。
2004081788.tif 000041
上記の関数Ｌｏｗｅｒ（ｓ，ｓ’）のアルゴリズムの意味は以下の通りである。
＜開始＞
＜Ｉｆ文開始＞もし、Ｄｅｆ（ｓ）［宣言ｓの単語］がＵｓｅ（ｓ’）［宣言のｓ’のＵｓｅ］に属するなら、真（ｔｒｕｅ）を返す
そうでないなら、偽（ｆａｌｓｅ）を返す
＜Ｉｆ文終了＞
＜終了＞
図１４は、この関数Ｌｏｗｅｒ（ｓ，ｓ’）のアルゴリズムをフローチャートに示したものである。図１４の処理を説明すると以下のとおりである。まず、ステップ６０１の判定「Ｄｅｆ（ｓ）［宣言ｓの単語］がＵｓｅ（ｓ’）［宣言のｓ’のＵｓｅ］に属すか否か」を行う。判定結果が真の場合は、関数の結果として「真ｔｒｕｅ」を返す（ステップ６０２）。判定結果が偽の場合は、関数の結果として「偽ｆａｌｓｅ」を返す（ステップ６０３）。
５）Ｍｉｎ
任意の宣言の順列Ｓがあるとき、関数Ｍｉｎは、Ｓの中の宣言ｓであって、Ｌｏｗｅｒ（ｓ’，ｓ）が真となるような別の宣言ｓ’をＳの中に持たない宣言ｓを返す。下記の関数Ｍｉｎ（Ｓ）のアルゴリズムがこの定義をとらえている。
2004081788.tif 000042
上記の関数Ｍｉｎ（Ｓ）のアルゴリズムの意味は以下の通りである。
Ｓは空集合でない宣言列である。変数ｓは１つの宣言である。
＜開始＞
関数Ｆｉｒｓｔ（Ｓ）［宣言列の先頭の宣言返す］の結果を変数ｓに記録する。
＜Ｆｏｒ文開始＞宣言列Ｓから変数ｓの値（宣言）を除いた宣言列に属す全ての宣言ｓ’について以下を実行する。
＜Ｉｆ文開始＞もし、関数Ｌｏｗｅｒ（ｓ’，ｓ）が真である［宣言ｓ’の単語は変数ｓの宣言の定義に使用される］なら、変数ｓに宣言ｓ’を記録する。
＜Ｉｆ文終了＞
＜Ｆｏｒ文終了＞
変数ｓの値を返す
＜終了＞
図１５は、この関数Ｍｉｎ（Ｓ）のアルゴリズムをフローチャートに示したものである。図１５を説明すると以下のようになる。まず、関数Ｆｉｒｓｔ（Ｓ）［宣言列の先頭の宣言返す］の結果を変数ｓに記録する（ステップ７０１）。次に、ステップ７０２で「宣言列Ｓから変数ｓの値（宣言）を除いた宣言列の中で、ステップ７０３が未実行の宣言ｓ’があるか否か」を判定する。判定結果が真の場合は、ステップ７０３に進み、「関数Ｌｏｗｅｒ（ｓ’，ｓ）が真である［宣言ｓ’の単語は変数ｓの宣言の定義に使用される］か否か」を判定し、結果が真なら変数ｓに宣言ｓ’を記録し（ステップ７０４）、ステップ７０２に戻る。ステップ７０３の結果が偽なら直接ステップ７０２に戻る。ステップ７０２の結果が真である限り、ステップ７０２から７０４の再起処理（７０６）を繰り返す。
ステップ７０２の結果が偽となったら、ステップ７０５に進み、関数Ｍｉｎ（Ｓ）の結果として変数ｓの値を返す。
以上の定義によって、宣言列の最適順序付けを形式的に定義することが容易となる。
（４−３）最適順序付けの形式的定義
宣言列の最適順序付けを形式的に定義する。Ｓが宣言列であるとすると、ＳｔａｔｅｍｅｎｔＯｒｄｅｒｉｎｇ（Ｓ）によって示されたＳに属する宣言列の順序付けされた順列は、形式的には下記のように定義される。
2004081788.tif 000043
上記の形式的定義は、関数ＳｔａｔｅｍｅｔｎｓＯｒｄｅｒｉｎｇ（Ｓ）の結果は、「宣言の順列Ｓが空であれば、空。そうでなければ、ＡｄｄＦｉｒｓｔ（Ｍｉｎ（Ｓ），ＳｔａｔｅｍｅｎｔＯｒｄｅｒｉｎｇ（Ｒｅｍｏｖｅ（Ｓ，Ｍｉｎ（Ｓ））））の結果」であることを意味している。ＡｄｄＦｉｒｓｔ（Ｍｉｎ（Ｓ），ＳｔａｔｅｍｅｎｔＯｒｄｅｒｉｎｇ（Ｒｅｍｏｖｅ（Ｓ，Ｍｉｎ（Ｓ））））の意味については、後述する関数ＳｔａｔｅｍｅｎｔｓＯｒｄｅｒｉｎｇ（Ｓ）のフローチャートの説明によって詳しく述べる。
下記の関数ＳｔａｔｅｍｅｎｔｓＯｒｄｅｒｉｎｇ（Ｓ）のアルゴリズムによって、宣言列Ｓの最適順序付けが可能である。
2004081788.tif 000044
上記の関数ＳｔａｔｅｍｅｎｔｓＯｒｄｅｒｉｎｇ（Ｓ）のアルゴリズムの意味は以下の通りである。
Ｓは宣言列である。変数ｍｉｎは１つの宣言である。
＜開始＞
＜Ｉｆ文開始＞宣言列Ｓが空集合なら、空を返し、
そうでないなら、Ｍｉｎ（Ｓ）［宣言列Ｓの中で、その定義に他のいずれの宣言も使用していない宣言を返す］の結果の宣言を変数ｍｉｎに記録し、
関数ＡｄｄＦｉｒｓｔ（ｍｉｎ，ＳｔａｔｅｍｅｎｔＯｒｄｅｒｉｎｇ（Ｒｅｍｏｖｅ（Ｓ，ｍｉｎ）））の値を返す
＜Ｉｆ文終了＞
＜終了＞
関数ＡｄｄＦｉｒｓｔ（ｍｉｎ，ＳｔａｔｅｍｅｎｔＯｒｄｅｒｉｎｇ（Ｒｅｍｏｖｅ（Ｓ，ｍｉｎ）））については、以下のフローチャートの説明で詳しく述べる。
図１６は、この関数ＳｔａｔｅｍｅｎｔｓＯｒｄｅｒｉｎｇ（Ｓ）のアルゴリズムをフローチャートに示したものである。図１６の説明は次のようになる。まず、ステップ８０１の「要件の宣言列Ｓは空集合か否か」の判定を行い、判定結果が真であれば関数ＳｔａｔｅｍｅｎｔｓＯｒｄｅｒｉｎｇ（Ｓ）の結果として空を返して処理を終わる。
ステップ８０１の判定結果が偽であれば、ステップ８０２に進み、変数ｍｉｎの領域に関数Ｍｉｎ（Ｓ）［宣言列Ｓの中で、その定義に他のいずれの宣言も使用していない宣言を返す］の結果を記録し、ステップ８０３に進む。ステップ８０３で関数Ｒｅｍｏｖｅ（Ｓ，ｍｉｎ）［宣言列Ｓから変数ｍｉｎの値の宣言を除く］を実行し、ステップ８０４の進む。ステップ８０４で「関数Ｒｅｍｏｖｅ（Ｓ，ｍｉｎ）の結果であるＳ’が固定値か否か」を判定し、判定結果が偽であればステップ８０３に戻って再度実行する。ステップ８０４の結果が偽である限り、ステップ８０３から８０４の第１の再起処理（８１１）を繰り返す。
ステップ８０４の判定結果が真になったとき、ステップ８０５に進む。ステップ８０５で関数ＳｔａｔｅｍｅｎｔＯｒｄｅｒｉｎｇ（Ｓ’）を実行し、ステップ８０６に進む。ステップ８０６で［関数ＳｔａｔｅｍｅｎｔＯｒｄｅｒｉｎｇ（Ｓ’）の結果Ｓ’’が固定値か否か」を判定し、判定結果が偽であれば、ステップ８０１に戻ってステップ８０１を再度実行する。ステップ８０６の結果が偽である限り、ステップ８０１からステップ８０６の第２の再起処理（８１２）を繰り返す。
ステップ８０６の結果が真となったとき、ステップ８０７に進み、関数ＡｄｄＦｉｒｓｔ（ｍｉｎ，Ｓ’’）を実行し、次にステップ８０８に進む。ステップ８０８では、「関数ＡｄｄＦｉｒｓｔ（ｍｉｎ，Ｓ’’）の結果Ｓ’’’が固定値に達したか否か」を判定し、判定結果が偽であればステップ８０７に戻って再度実行する。ステップ８０８の結果が偽である限り、ステップ８０７から８０８の第３の再起処理（８１３）を繰り返す。
ステップ８０８の判定結果が真になったとき、ステップ８０９に進み、関数ＳｔａｔｅｍｅｎｔＯｒｄｅｒｉｎｇ（Ｓ）の結果として宣言列Ｓ’’’の値を返えし、関数処理を終了する。
５．スライシング（Ｓｌｉｃｉｎｇ）
プログラムのスライシング・テクニックは非特許文献１２にさかのぼる。スライシングは、プログラムを特定の計算に関連している宣言に縮小させるというプログラムの抽出として考えられる。伝統的なプログラミング言語の中で、スライシングは、プログラム読解とデバッグを「分割して支配する」アプローチ（より小さいプログラム群、すなわち、スライス群は、大きなプログラムより理解しやすい）として、長い間、使用されてきた。また、多くのアプリケーションの分析にも首尾よく使用されてきており、その目的は様々である。たとえば、結合度の判定、アルゴリズムのデバッグ、リバースエンジニアリング、コンポーネント再使用、自動並行化、プログラム統合、および補助検証が含まれる。
Ｌｙｅｅ要件においては、スライシングは、異なった観点から要件を分析するために役立てることができる。とりわけスライシングによれば、以下の観点から分析できるようになる。
１．任意の単語の定義に直接的または間接的に貢献する宣言はどれか？
２．並行して実行させることができるサブプログラム群を生成し得る要件の中で、独立している部分はどれか？
自動ツールを使って、上記の第１の観点から分析をおこなうことは、Ｌｙｅｅソフトウェア（要件）を理解して、維持するために非常に役に立つ。実際、要件で与えられている宣言の数が重大であるときに（数百本）、全体を見とおしてソフトウェアを理解し、維持するためには、いかなる定義がどれにに依存するのかを調べて行くことは、慎重になされない限り、骨の折れる作業であって誤りをおこし易い。
（５−１）単一スライス
（５−１−１）単一スライスの非形式的定義
任意の単語ａと宣言の集合Ｓがあった時、Ｓｌｉｃｅ（ａ，Ｓ）は、直接的または間接的に単語ａの定義に貢献するＳの中にあるすべての宣言である。スライスの概念を明確にするために具体例を上げる。
表１７は宣言の集合であるＬｙｅｅ要件である。
2004081788.tif 000045
Ｓが表１７で与えられた宣言の集合であるなら、単語ａのスライスＳｌｉｃｅ（ａ，Ｓ）は表１８に示されるものとなる。
2004081788.tif 000046
スライスそれ自体が要件の完全な集合である、ということは重要な点である。このスライスの概念は、いわゆる「分割して征服する」テクニックだと考えることができ、Ｌｙｅｅ要件を理解、あるいは維持するために、特にそれらが宣言を大量に含む場合に非常に有用である。
（５−１−２）単一スライスの形式的定義
任意の単語ａと宣言の集合Ｓがあったとき、Ｓの中の単語ａに関するスライスは、Ｓｌｉｃｅ（ａ，Ｓ）によって示されて、次のように定義される。
2004081788.tif 000047
上記の形式的定義は、関数Ｓｌｉｃｅ（ａ，Ｓ）の結果は、「宣言の集合Ｓに属する単語ａの宣言と、その単語ａの宣言の直接および間接Ｕｓｅに属する全ての単語ｂの宣言の集合の、和集合」であることを意味する。
下記の関数Ｓｌｉｃｅ（ａ，Ｓ）のアルゴリズムによって、Ｌｙｅｅ要件（宣言の集合）の中の任意の単語に関するスライスを生成することができる。
2004081788.tif 000048
上記の関数Ｓｌｉｃｅ（ａ，Ｓ）のアルゴリズムの意味は以下の通りである。ａは単語、Ｓは要件である宣言の集合である。変数ｓｌｉｃｅ＿ｓは宣言の集合、変数ｓは１つの宣言である。
＜開始＞
変数ｓに関数Ｓｔａｔｅｍｅｎｔ（ａ，Ｓ）［要件Ｓに属する単語ａの宣言を返す］の結果を記録する。
変数ｓｌｉｃｅ＿ｓに、変数ｓの値を記録する。
＜Ｆｏｒ文開始＞関数ＵｓｅＤｉｒｅｃｔＡｎｄＩｎｄｉｒｅｃｔ（ｓ，Ｓ））［要件Ｓに属す宣言ｓの直接および間接Ｕｓｅを返す］の結果に属する全ての単語ｂについて以下を実行する。
変数ｓｌｉｃｅ＿ｓに、変数ｓｌｉｃｅ＿ｓの値と関数Ｓｔａｔｅｍｅｎｔ（ｂ，Ｓ）［宣言Ｓに属する単語ｂの宣言を返す］の結果を記録する。
＜Ｆｏｒ文終了＞
変数ｓｌｉｃｅ＿ｓの値を返す
＜終了＞
図１７は、この関数Ｓｌｉｃｅ（ａ，Ｓ）のアルゴリズムをフローチャートに示したものである。図１７を説明すると以下のようになる。まず、ステップ９０１で、変数ｓに関数Ｓｔａｔｅｍｅｎｔ（ａ，Ｓ）［要件Ｓに属する単語ａの宣言を返す］の結果を記録し、関数Ｓｔａｔｅｍｅｎｔ（ａ，Ｓ）［要件Ｓに属する単語ａの宣言を返す］の結果を記録する。次に、ステップ９０２進み、「関数ＵｓｅＤｉｒｅｃｔＡｎｄＩｎｄｉｒｅｃｔ（ｓ，Ｓ）［要件Ｓに属す宣言ｓの直接および間接Ｕｓｅを返す］の結果の中に未実行単語ｂがあるか否か」の判定を行う。判定結果が真であれば、ステップ９０３に進み、変数ｓｌｉｃｅ＿ｓに変数ｓｌｉｃｅ＿ｓの値と関数Ｓｔａｔｅｍｅｎｔ（ｂ，Ｓ）［要件Ｓに属す単語ｂの宣言を返す］の結果の宣言を記録、ステップ９０２に戻り再度実行する。ステップ９０２が真である限り、ステップ９０２からステップ９０３の再起処理（９０５）を繰り返す。
ステップ９０２の判定結果が偽となったとき、ステップ９０４に進み、関数ｓｌｉｃｅ（ａ，Ｓ）の結果として、変数ｓｌｉｃｅ＿ｓの値を返す。
最も重要なスライスは一般に出力単語に関するスライスである。下記の関数ＡｌｌＯｕｔｐｕｔＳｌｉｃｅ（Ｓ）のアルゴリズムによって、任意のＬｙｅｅ要件の中の各出力単語に関するスライスを生成することができる。
2004081788.tif 000049
上記の関数ＡｌｌＯｕｔｐｕｔＳｌｉｃｅ（Ｓ）のアルゴリズムの意味は以下の通りである。
Ｓは要件である宣言の集合である。変数ｓｌｉｃｅＳｅｔはスライスの集合である。
＜開始＞
変数ｓｌｉｃｅＳｅｔの領域に「０」を記録する。
＜Ｆｏｒ文開始＞関数ＯｕｔｐｕｔＳｔａｔｅｍｅｎｔｓ（ｓ）［要件Ｓにの全ての出力単語の宣言を返す］に属す全ての宣言ｓについて以下を実行する。
変数ｓｌｉｃｅＳｅｔに、変数ｓｌｉｃｅＳｅｔの値と関数Ｓｌｉｃｅ（Ｗｏｒｄ（ｓ），Ｓ）［要件Ｓに属す宣言ｓの単語のスライスを返す］の結果を記録する。
＜Ｆｏｒ文終了＞
変数ｓｌｉｃｅＳｅｔの値を返す。
＜終了＞
図１８は、この関数ＡｌｌＯｕｔｐｕｔＳｌｉｃｅ（Ｓ）のアルゴリズムをフローチャートに示したものである。図１８を説明すると以下のとおりである。まず、変数ｓｌｉｃｅＳｅｔの領域に値「０」を記録する（ステップ１００１）。次に、ステップ１００２で、「関数ＯｕｔｐｕｔＳｔａｔｅｍｅｎｔｓ（Ｓ）［要件Ｓにの総ての出力単語の宣言を返す］の中で未実行の宣言ｓがあるか否か」を判定する。判定結果が真であればステップ１００３に進み、変数ｓｌｉｃｅＳｅｔの領域に変数ｓｌｉｃｅＳｅｔの値と関数Ｓｌｉｃｅ（Ｗｏｒｄ（ｓ），Ｓ）［要件Ｓに属す宣言ｓの単語のスライスを返す］の結果を記録する。ステップ１００３終了後、ステップ１００２に戻り再度実行する。ステップ１００２の結果が真である限り、ステップ１００２から１００３の再起処理（１００５）を繰り返す。
ステップ１００２の結果が偽となったとき、ステップ１００４に進んで変数ｓｌｉｃｅＳｅｔの値を返す。
（５−２）独立スライス（Ｉｎｄｅｐｅｎｄｅｎｔ  Ｓｌｉｃｅｓ）
スライシングのテクニックは、要件の中で独立部分を知るためにも容易に用いることができる。任意の要件の独立部分を探すことは、もう１つの「分割して征服する」テクニックとして、プログラムの理解と自動的並行化（ｐａｒａｌｌｅｌｉｚａｔｉｏｎ）に有用な方法である。
（５−２−１）独立スライスの非形式的定義
２つのスライス集合Ｓ１とＳ２は、もしＳ１とＳ２の両方に関係している宣言がないなら、独立していると言える。独立したスライスの具体例を示す。Ｓが表１７に示された宣言の集合であるとき、Ｓｌｉｃｅ（ｄ，Ｓ）は表１９のように示される。
2004081788.tif 000050
2004081788.tif 000051
このとき、表１８のＳｌｉｃｅ（ａ，Ｓ）、および表１９のＳｌｉｃｅ（ｄ，Ｓ）の両方に関係している宣言はない。従って、２つのスライスＳｌｉｃｅ（ａ，Ｓ）とＳｌｉｃｅ（ｄ，Ｓ）は独立しており、そして並列に実行できると結論づけできる。
（５−２−２）独立スライスの形式的定義
もし、以下の条件が成立すれば、２つのスライス集合Ｓ１とＳ２は独立している。
2004081788.tif 000052
上記は、Ｓ１の要素でありかつＳ２の要素であるスライス（宣言の集合）がないことを示している。
１つのスライス集合があって、どのスライスが他から独立したスライスの部分集合かを把握しようとした場合を考えてみる。例えば、我々がそれぞれの出力単語に関するスライスを生成し、これらのスライスの独立部分を検出しようとする場合である。まず、スライスの独立した部分集合の概念を理解する手助けとなるいくつかの定義を紹介する。
２つの独立したスライス集合：
Ｓ１とＳ２を２つのスライス集合とする。スライスＳ１∈Ｓ１（スライス集合Ｓ１に属するスライスＳ１）とスライスＳ２∈Ｓ２（スライス集合Ｓ２に属するスライスＳ２）が独立しているなら、スライス集合Ｓ１とＳ２は独立している。
最適スライス集合：
Ｓをスライス集合とする。Ｓ１≠０かつＳ２≠０であるような、Ｓ１⊂Ｓ（スライスＳ１がスライス集合Ｓに属す）である総てのＳ１、かつ、Ｓ２⊂Ｓ（スライスＳ２がスライス集合Ｓに属す）である総てのＳ２、において、Ｓ１とＳ２が独立していないなら、Ｓは最適スライス集合である。
最適かつ独立したスライス集合：
Ｓ１・・・Ｓｎをｎ個のスライス集合とする。もし、ｉが１＜ｉ＜ｎであるような総てのＳｉが最適スライス集合で、ｊが１＜ｊ＜ｎかつｉ≠ｊであるようなＳｊがあったとき、総てのＳｉとＳｊが独立スライス集合であるなら、Ｓ１・・・Ｓｎは最適かつ独立したスライス集合である。
下記の関数ＩｎｄｅｐｅｎｄｅｎｔＳｅｔＯｆＳｌｉｃｅ（Ｓ）のアルゴリズムによって、出力単語のスライスを抽出し、それらを最適かつ独立したスライス集合に分離することができる。
2004081788.tif 000053
上記の関数ＩｎｄｅｐｅｎｄｅｎｔＳｅｔＯｆＳｌｉｃｅ（Ｓ）のアルゴリズムの意味は以下の通りである。
Ｓは要件である宣言の集合である。変数ｓｌｉｃｅＭｕｌｔｉＳｅｔはスライス集合の集合である。変数ｓｌｉｃｅＳｅｔはスライスの集合である。変数ＯｕｔｐｕｔＷｏｒｄｓ、変数ＮｏｔＴｒｅａｔｅｄＷｏｒｄｓは単語の集合である。
＜開始＞
変数ｓｌｉｃｅＳｅｔの領域に値「０」を記録する。
変数ＯｕｔｐｕｔＷｏｒｄｓの領域に関数Ｗｏｒｄ（ＯｕｔｐｕｔＳｔａｔｅｍｅｎｔｓ（Ｓ））［要件Ｓの全出力単語の宣言の単語を返す］の結果を記録する。
＜Ｆｏｒ文開始＞変数ＯｕｔｐｕｔＷｏｒｄｓの値に属す全ての単語ａについて以下を実行する。
変数ｓｌｉｃｅＳｅｔに関数Ｓｌｉｃｅ（ａ，Ｓ）［要件Ｓに属す単語ａのスライスを返す］の結果を記録する。
変数ＯｕｔｐｕＷｏｒｄｓの領域に、変数ＯｕｔｐｕｔＷｏｒｄｓの値から単語ａを除いた単語の集合を記録する。
変数ＮｏｔＴｒｅａｔｅｄＷｏｒｄｓの領域に変数ＯｕｔｐｕｔＷｏｒｄｓの値を記録する。
＜Ｆｏｒ文開始＞変数ＮｏｔＴｒｅａｔｅｄＷｏｒｄｓに属する全ての単語ｂについて以下を実行する。
＜Ｉｆ文開始＞もし、関数ＵｓｅＤｉｒｅｃｔＡｎｄＩｎｄｉｒｅｃｔ（Ｓｌｉｃｅ（ｂ，Ｓ））［単語ｂのスライス［単語ｂの定義に使用されている単語の宣言の集合］の直接および間接Ｕｓｅ］と単語ｂの和集合と、
関数ＵｓｅＤｉｒｅｃｔＡｎｄＩｎｄｉｒｅｃｔ（Ｓｌｉｃｅ（ａ，Ｓ））［単語ｂのスライス［単語ａの定義に使用されている単語の宣言の集合］の直接および間接Ｕｓｅ］と単語ａの和集合の、２つの集合の積集合が空でなければ、すなわち２つの集合に共に属す単語があれば、
変数ｓｌｉｃｅＳｅｔの領域に、変数ｓｌｉｃｅＳｅｔの値と関数Ｓｌｉｃｅ（ｂ，Ｓ）を記録し、
変数ＮｏｔＴｒｅａｔｅｄＷｏｒｄｓの領域に、変数ＮｏｔＴｒｅａｔｅｄＷｏｒｄｓの値から単語ｂを除いた単語の集合を記録する。
＜Ｉｆ文終了＞
＜Ｆｏｒ文終了＞
変数ｓｌｉｃｅＭｕｌｔｉＳｅｔの領域に、変数ｓｌｉｃｅＳｅｔの値を記録する。
＜Ｆｏｒ文終了＞
変数ｓｌｉｃｅＭｕｌｔｉＳｅｔの値を返す
＜終了＞
図１９は、この関数ＩｎｄｅｐｅｎｄｅｎｔＳｅｔＯｆＳｌｉｃｅ（Ｓ）のアルゴリズムをフローチャートに示したものである。図１９を説明する次のようになる。まず、変数ｓｌｉｃｅＳｅｔの領域に値「０」を、変数ＯｕｔｐｕｔＷｏｒｄｓの領域に関数Ｗｏｒｄ（ＯｕｔｐｕｔＳｔａｔｅｍｅｎｔｓ（Ｓ））［要件Ｓの全出力単語の宣言の単語を返す］の結果を記録する（ステップ１１０１）。次に、ステップ１１０２で「変数ＯｕｔｐｕｔＷｏｒｄｓの値の中で未実行の単語ａがあるか否か」判定し、判定結果が真であればステップ１１０３に進む。ステップ１１０３では、変数ｓｌｉｃｅＳｅｔに関数Ｓｌｉｃｅ（ａ，Ｓ）［要件Ｓに属す単語ａのスライスを返す］の結果を記録、変数ＯｕｔｐｕＷｏｒｄｓの領域に変数ＯｕｔｐｕｔＷｏｒｄｓの値から単語ａを除いた単語の集合を記録、変数ＮｏｔＴｒｅａｔｅｄＷｏｒｄｓの領域に変数ＯｕｔｐｕｔＷｏｒｄｓの値を記録する。
次に、ステップ１１０４で「変数ＮｏｔＴｒｅａｔｅｄＷｏｒｄｓの値の中に未実行の単語ｂがあるか否か」判定し、結果が真であれば、ステップ１１０５に進む。
ステップ１１０５では、「関数ＵｓｅＤｉｒｅｃｔＡｎｄＩｎｄｉｒｅｃｔ（Ｓｌｉｃｅ（ｂ，Ｓ））［単語ｂのスライス［単語ｂの定義に使用されている単語の宣言の集合］の直接および間接Ｕｓｅ］と単語ｂの和集合と、関数ＵｓｅＤｉｒｅｃｔＡｎｄＩｎｄｉｒｅｃｔ（Ｓｌｉｃｅ（ａ，Ｓ））［単語ｂのスライス［単語ａの定義に使用されている単語の宣言の集合］の直接および間接Ｕｓｅ］と単語ａの和集合の、２つの集合の積集合が存在するか否か（すなわち２つの集合に共に属す単語があるか否か）」を判定する。判定結果が真であれば、ステップ１１０６に進み、変数ｓｌｉｃｅＳｅｔの領域に変数ｓｌｉｃｅＳｅｔの値と関数Ｓｌｉｃｅ（ｂ，Ｓ）を記録し、変数ＮｏｔＴｒｅａｔｅｄＷｏｒｄｓの領域に変数ＮｏｔＴｒｅａｔｅｄＷｏｒｄｓの値から単語ｂを除いた単語の集合を記録する。ステップ１１０６終了後はステップ１１０４に戻り再度実行する。ステップ１１０４の判定が真である限り、ステップ１１０４から１１０６の第１の再起処理（１１０９）を繰り返す。
ステップ１１０４の判定が偽となったときは、ステップ１１０７に進み、変数ｓｌｉｃｅＭｕｌｔｉＳｅｔの領域に、変数ｓｌｉｃｅＳｅｔの値を記録する。ステップ１１０７が終了後は、ステップ１１０２に戻り再度実行する。ステップ１１０２の判定結果が真である限り、ステップ１１０２から１１０７の第２の再起処理（１１１０）を繰り返す。
ステップ１１０２の判定結果が偽となったときは、ステップ１１０８に進み、関数ＩｎｄｅｐｅｎｄｅｎｔＳｅｔＯｆＳｌｉｃｅ（Ｓ）の結果として変数ｓｌｉｃｅＭｕｌｔｉＳｅｔの値を返す
（５−２−３）最適独立スライス集合の例
最適かつ独立したスライス集合の具体例を示す。表２０は、Ｓで示される宣言の集合である。
2004081788.tif 000054
（１）出力単語のスライス
Ｓによって示される、Ｓの出力単語に対応しているスライスの集合は、以下のとおりである。
2004081788.tif 000055
そして、これらのスライスは以下の表のようになる。
2004081788.tif 000056
2004081788.tif 000057
2004081788.tif 000058
2004081788.tif 000059
2004081788.tif 000060
2004081788.tif 000061
（２）最適かつ独立したスライス集合
Ｓから抽出できる最適かつ独立したスライス集合は下記のとおりである。
2004081788.tif 000062
６．タイピング（Ｔｙｐｉｎｇ）
タイピング（非特許文献２及び１１参照）はプログラムのいくつかの動的な良い振舞いの特性を静的に保証するために主に使用されている。タイピングを行えば、プログラムの実行時に頻繁に起こるエラーを、コンパイル時に検出することができる。また、タイピング技術は、開発されたソフトウェアが何らかのセキュリティ問題に対処するのを確実にするのに首尾よく使用されてきた（非特許文献１１参照）。
このセクションでは、Ｌｙｅｅ要件の単語のタイプに関連する誤りを検出するための分析と、Ｌｙｅｅ要件簡素化（出力単語のタイプを指定しなくとも、入力されたもののタイプから、中間単語と出力単語のタイプを自動的に生成する）のために、どのようにタイピング技術を使用することができるかを示す。さらに、ソフトウェア開発に関連するセキュリティ問題（例えば何らかの機密情報がソフトウェアの原因によって漏らされてはならない）を扱うために、いかに容易にＬｙｅｅ方法論を拡張することができるかを示す。
タイピングの目的は、タイプの正しくない取り扱いによるエラーを検出することである。タイピングにより、可能な場合は、タイプの修正や、欠けているタイプの生成することができる。例えば、ユーザが入力単語のタイプの指定のみが可能であるとき、それだけですべての単語のタイプが自動的に生成することがでる。タイプのエラー検出や、誤っているタイプを訂正すること、あるいは欠けているタイプを生成するためには、最初に、含まれている演算対象（ｏｐｅｒａｎｄ）のタイプを明確に定義することが必要である。任意のＬｙｅｅ要件のタイピングが、本セクション以前に説明した各種の最適化や分析の後に行われると非常に有益である、ということは重要な点である。言い換えれば、任意のＬｙｅｅ要件に循環宣言、不要宣言、非活性宣言が含まれていないことを、タイピングを始める前に、確認しなければならない。
（６−１）タイピング規則
タイピングのテクニックは、一般に次の要素の使用を含む。
（６−１−１）基本のタイプ
この項では、任意のＬｙｅｅ要件に含まれる単語、定数、演算子に属するタイプの、異なる種類を定義する。
＜値のタイプ＞
単純化のために、単語と定数のタイプは、ブール型（ｂｏｏｌｅａｎ）か整数型、あるいはフロート（浮動少数点数）型であるとする。便宜のために、これらのタイプを次のように再編する。
2004081788.tif 000063
上記の定義は次のように読むことができる：Ｔｖａｌ（値のタイプ）とは、Ｔｎｕｍ（数値のタイプ）またはＴｂｏｏｌ（ブール値のタイプ）である。Ｔｎｕｍは整数型あるいはフロート型である。最後に、Ｔｂｏｏｌはブール型に対応する。
＜演算子のタイプ＞
同様に、任意のＬｙｅｅ要件に含まれる、ブールおよび算術演算子のタイプを明確にしなければならない。各演算子に関し、そのオペランド（演算対象）のタイプとその結果のタイプについて正確でなければならない。任意の演算子のタイプは一般に、Ｔ１→Ｔ２の形式をとる。直感的わかるように、これは、演算子は、入力としてタイプＴ１の要素とり、そしてタイプＴ２の要素を返すような関数である、と考えられることを意味する。
いうまでもなく、いくつかの演算子は１つ以上のオペランドを持つ。従って、もし、１つのタイプはそれ自身が２つのタイプの組の場合もあると考えれば、この事実を考慮するのは容易である。まとめると、あるタイプは、Ｔｖａｌ（値のタイプ）、２つのタイプの組Ｔ１×Ｔ２あるいはＴ１→Ｔ２である。より形式的に表せば、次のように書くことができる。
2004081788.tif 000064
上記の形式的表記は、「任意のタイプＴは、Ｔｖａｌ（値のタイプ）、２つのタイプの組Ｔ１×Ｔ２、あるいはＴ１→Ｔ２である」、ことを意味している。
（６−１−２）定数タイピング（Ｃｏｎｓｔａｎｔ  Ｔｙｐｉｎｇ）
Ｌｙｅｅ要件のタイピングにおいて、宣言の中に含まれる定数に許されるタイプは次に通りである。
2004081788.tif 000065
上記の表記は、ｔｒｕｅまたはｆａｌｓｅ（真偽値）のタイプはｂｏｏｌ（ブール型）であり、
ｎｕｍ（数値）のタイプはｉｎｔ（整数型）であり、ｎｕｍ．ｎｕｍ（浮動小数点数値）のタイプはｆｌｏａｔ（フロート型）である、ことを意味している。
より正確には、後述するように、任意の定数に１つのタイプを関連づけるために、下記の関数が使われる。
2004081788.tif 000066
上記の関数ＴｙｐｅＯｆＣｓｔ（ｃｓｔ）の意味は以下の通りである。
関数の引数ｃｓｔは、定数をである。
＜開始＞
関数Ｓｗｉｔｃｈ（ｃｓｔ）の実行
引数の定数ｃｓｔが、ｔｒｕｅまたはｆａｌｓｅ（真偽値）のとき、値ｂｏｏｌ（ブール型）を返す。
引数の定数ｃｓｔが、ｎｕｍ（数値）のとき、値ｉｎｔ（整数型）を返す。
引数の定数ｃｓｔが、ｎｕｍ．ｎｕｍ（浮動小数点数値）のとき、値ｆｌｏａｔ（フロート型）を返す。
関数Ｓｗｉｔｃｈの終了
＜終了＞
定数タイピングは次の規則によって形式化できる。
2004081788.tif 000067
上記形式的記述による定数のタイピング規則は、「任意のＬｙｅｅ要件εに属する定数ｃのタイプは、前提条件なしで、単に関数ＴｙｐｅＯｆＣｓｔ（ｃ）によって返される値である」ことを示している。（これ以前の説明ではＬｙｅｅ要件を示す記号としてＳを用いたが、タイピングテクニックでは、慣習的にεが使われるのでεを用いる。）
（６−１−３）単語のタイピング（Ｗｏｒｄ  Ｔｙｐｉｎｇ）
どんな入力単語についても、ユーザはそのタイプについて絶対に正確でなければならない。入力単語以外の単語については、それらのタイプは自動的に算出され、そしてこれらの単語を定義している宣言の「タイプ」領域に保存される。すでに分かっている単語がある場合に、そのタイプを返す関数ＴｙｐｅＯｆＷｒｄを下記のように定義する：
2004081788.tif 000068
上記の関数ＴｙｐｅＯｆＷｒｄ（ｗ，ε）の意味は以下の通りである。
関数の引数ｗは、宣言のリストεに属する単語である。
＜開始＞
単語ｗの宣言を算出し（Ｓｔａｔｅｍｅｎｔ（ｗ，ε））、算出した宣言（Ｓｔａｔｅｍｅｎｔ（ｗ，ε）の結果をｓとおく）のタイプを返す（Ｔｙｐｅ（ｓ））。
＜終了＞
単語のタイピングは次の規則によって形式化できる。
2004081788.tif 000069
上記形式的記述が示す単語のタイピング規則は、「任意のＬｙｅｅ要件εをタイピングの環境とする単語ｗのタイプは、前提条件なしで、単に関数ＷｙｐｅＯｆＷｒｄ（ｗ，ε）によって返される値である」、ことを示している。
（６−１−４）演算子のタイピング（Ｏｐｅｒａｔｏｒ  Ｔｙｐｉｎｇ）
プログラムで使用できる各演算子のタイプついては、より厳密さが必要である。実際、演算子のあるものはブール型の引数を必要としてブール型の結果を返すが、別の演算子は他のタイプの引数を必要とし、別のタイプの結果を返す、という場合があるからである。Ｌｙｅｅ要件に関与する各演算子のより厳密なタイプは、以下のように形式化できる：
2004081788.tif 000070
上記の形式的定義は、次のような意味である。１）と２）の演算子は、入力として１つの値をとり、１つの値を返すが、３）から６）の演算子は、結果として１つの値を返すために入力として２つの値を必要とする。
１）−ｕ
単項演算子−ｕのタイプは、Ｔｎｕｍ（数値のタイプ）を与えるとＴｎｕｍ（数値のタイプ）を返す関数である。
２）ｎｏｔ
ブール型演算子の１つｎｏｔ（論理否定の演算子）のタイプは、ブール型（ｂｏｏｌ）を与えるとブール型（ｂｏｏｌ）を返す関数である。たとえば、演算子ｎｏｔにｔｒｕｅ（ブール型）を与えれば、「ｎｏｔ  ｔｒｕｅ」の結果はｆａｌｓｅ（ブール型）であり、ｆａｌｓｅ（ブール型）をあたえれば、「ｎｏｔ  ｆａｌｓｅ」の結果はｔｒｕｅ（ブール型）である。
３）＋、−ｂ、＊
演算子＋（加法）、−ｂ（減法）、＊（乗法）のタイプは、Ｔｎｕｍ（数値のタイプ）とＴｎｕｍ（数値のタイプ）の組を与えると、１つのＴｎｕｍ（数値のタイプ）を返す関数である。
４）＜、＜＝、＞＝、＞
演算子＜（左辺が右辺より小さい）、＜＝（左辺が右辺より小さいか、または等しい）、＞＝（左辺が右辺より大きい、または等しい）、＞（左辺が右辺より大きい）のタイプは、Ｔｎｕｍ（数値のタイプ）とＴｎｕｍ（数値のタイプ）の組を与えると、１つのＴｎｕｍ（数値のタイプ）を返す関数である。
５）ｏｒ、ａｎｄ
ブール型演算子であるｏｒ（論理和の演算子）とａｎｄ（論理積の演算子）のタイプは、ｂｏｏｌ（ブール型）とｂｏｏｌ（ブール型）の組を与えると、１つのｂｏｏｌ（ブール型）を返す関数である。たとえば、論理和のブール演算子ｏｒにｔｒｕｅ（ブール型）とｔｒｕｅ（ブール型）を与えれば、「ｔｒｕｅ  ｏｒ  ｔｒｕｅ」の結果はｔｒｕｅ（ブール型）である。
６）＝、＜＞
演算子＝（左辺は右辺に等しい）、＜＞（左辺は右辺と異なる）は、Ｔｖａｌ（値のタイプ）とＴｖａｌ（値のタイプ）の組を与えると、１つのｂｏｏｌ（ブール型）を返す関数である。
より具体的には、任意の演算子のタイプを返す関数ＴｙｐｅＯｆＯｐは、下記のように定義することができる。
2004081788.tif 000071
上記の関数ＴｙｐｅＯｆＯｐ（Ｏｐ）の意味は以下の通りである。
引数ｏｐは、演算子である。
＜開始＞
関数Ｓｗｉｔｃｈ（ｏｐ）の実行
引数の演算子ｏｐが−ｕ（単項演算子）のとき、Ｔｎｕｍ→Ｔｎｕｍ（数値のタイプをとり、数値のタイプを返す関数型）を返す。
引数の演算子ｏｐがｎｏｔ（論理演算子）のとき、ｂｏｏｌ→ｂｏｏｌ（ブール型をとり、ブール型を返す関数型）を返す。
引数の演算子ｏｐが＋または−ｂのとき、Ｔｎｕｍ×Ｔｎｕｍ→Ｔｎｕｍ（２つの数値のタイプの組をとり、数値のタイプを返す関数型）を返す。
引数の演算子ｏｐが＜、＜＝、＞＝、＞のとき、Ｔｎｕｍ×Ｔｎｕｍ→ｂｏｏｌ（２つの数値のタイプの組をとり、ブール型を返す関数型）を返す。
引数の演算子ｏｐがｂｏｏｌ×ｂｏｏｌ→ｂｏｏｌ（２つのブール型の組をとり、ブール型を返す関型）
引数の演算子ｏｐがＴｖａｌ×Ｔｖａｌ→Ｔｖａｌ（２つの値のタイプの組をとり、値のタイプを返す関数型）を返す。
関数Ｓｗｉｔｃｈの終了
＜終了＞
演算子タイピングは次の規則によって形式化することができる：
2004081788.tif 000072
上記形式的記述が示す規則は、任意のＬｙｅｅ要件εをタイピングの環境とする演算子Ｏｐのタイプは、前提条件なしで、常に単に関数ＴｙｐｅＯｆＯｐ（Ｏｐ）によって返される値であることを示している。
（６−１−５）式のタイピング（Ｅｘｐｒｅｓｓｉｏｎ  Ｔｙｐｉｎｇ）
各種類の式のタイプを判定する方法を示す。式のタイピングの説明を
2004081788.tif 000073
係を導入する必要がある。
2004081788.tif 000074
2004081788.tif 000075
きは、ｔｒｕｅ＝ｆａｌｓｅを意味することに留意されたい。
上記の順序関係を使って、２つのタイプの上位のもの（ｓｕｐ）を以下のように定義することができる。
2004081788.tif 000076
上記の記述は、「Ｔ１とＴ２のうち上位のタイプは（Ｓｕｐ（Ｔ１，Ｔ２））、Ｔ１
2004081788.tif 000077
式Ｅｘｐは、以下の定義で示すような、「ｖａｌ（値）」、「ｉｄ（識別子）」、「（Ｅｘｐ）（カッコ付き式）」、「ｏｐ  Ｅｘｐ（演算子  式）」、「Ｅｘｐ  ｏｐ  Ｅｘｐ（式  演算子  式）」のいずれかであるので、
2004081788.tif 000078
次の関数によって、式の種類ごとに１つのタイプを関連づけることができる。
2004081788.tif 000079
上記の関数ＴｙｐｅＯｆＥｘｐ（ｅ，ε）の意味は以下の通りである。関数の引数ｅは、宣言のリストεに属する式である。
＜開始＞
関数Ｓｗｉｔｃｈ（ｅ）の実行
引数ｅがｃ（定数）のとき、ＴｙｐｅＯｆＣｓｔ（ｃ）の値を返す
引数ｅがｗ（単語）のとき、ＴｙｐｅＯｆＷｒｄ（ｗ）の値を返す
引数ｅが「ｅ１」型（式）の式のとき、ＴｙｐｅＯｆＥｘｐ（ｅ１，ε）の値を返す
引数ｅが「ｏｐ  ｅ１」型（単項演算子  式）の式のとき、
ＴｙｐｅＯｆＯｐ（ｏｐ）の値を（Ｔ１、Ｔ２）に、ＴｙｐｅＯｆＥｘｐ（ｅ１，ε）の値をＴ’に記録する。
2004081788.tif 000080
い）の関係なら、Ｔ１を返す。
そうでなければ、エラーメッセージ（ＥｒｒＭｓｇ）を印刷し、ＴｙｐＥｒｒを返す。
＜Ｉｆ処理終了＞
引数ｅが「ｅ１  ｏｐ  ｅ２」型（式  二項演算子  式）の時、
ＴｙｐｅＯｆＯｐ（ｏｐ）の値を（Ｔ１、Ｔ２、Ｔ３）に、ＴｙｐｅＯｆＥｘｐ（ｅ１，ε）の値をＴ’１、に記録、ＴｙｐｅＯｆＥｘｐ（ｅ２，ε）の値をＴ’２に記録する。
2004081788.tif 000081
係なら、
＜Ｉｆ処理開始＞そして、もしＴ３がブール型でないなら、Ｓｕｐ（Ｔ’１，Ｔ’２）を返す。
そうでなければ、ｂｏｏｌを返す
＜Ｉｆ処理終了＞
そうでなければ、エラーメッセージ（ＥｒｒＭｓｇ）を印刷し、「ＴｙｐＥｒｒ」を返す
＜Ｉｆ処理終了＞
関数Ｓｗｉｔｃｈ終了。
＜終了＞
図２０は、この関数ＴｙｐｅＯｆＥｘｐ（ｅ，ε）をフローチャートに示したものである。図２０を説明すると次のようになる。まず、「式ｅが定数か否か」を判定し（ステップ１２０１）、結果が真であれば、関数ＴｙｐｅＯｆＣｓｔ（ｃ）［定数ｃのタイプを返す］の結果を返し（ステップ１２０２）、処理を終了する。
ステップ１２０１の結果が偽であれば、ステップ１２０３に進み、「式ｅが単語か否か」を判定し、判定結果が真であれば、関数ＴｙｐｅＯｆＷｏｒｄ（ｗ）［単語ｗのタイプを返す］の結果を返し（ステップ１２０４）、処理を終了する。
ステップ１２０３の結果が偽であれば、ステップ１２０５に進み、「式ｅが「ｅ１」型（式）の式か否か」を判定し、結果が真であれば、関数ＴｙｐｅＯｆＥｘｐ（ｅ１，ε）［宣言のリストεに属す式ｅ１のタイプを返す］の結果を返し（ステップ１２０６）、処理を終了する。
ステップ１２０５の結果が偽であれば、ステップ１２０７に進み、「式ｅが「ｏｐ  ｅ１」型（単項演算子  式）の式か否か」を判定し、判定結果が真であれば、関数ＴｙｐｅＯｆＯｐ（ｏｐ）［演算子ｏｐのタイプを返す］の値を（Ｔ１、Ｔ２）に、関数ＴｙｐｅＯｆＥｘｐ（ｅ１，ε）［宣言のリストεに属す式ｅ１のタイプを返す］の値をＴ’に記録する（ステップ１２０８）。ステップ１２０８終
2004081788.tif 000082
が真か否か」を判定し、真であればステップ１２１０でＴ１の値を返し、処理を終了する。ステップ１２０９の判定結果が偽であればステップ１２１１でエラーメッセージ（ＥｒｒＭｓｇ）出力して「ＴｙｐＥｒｒ」を返し、処理を終了する。
ステップ１２０７の判定結果が偽であれば、ステップ１２１２に進む。ステップ１２１２では、「式ｅが「ｅ１  ｏｐ  ｅ２」型（式  二項演算子  式）の式か否か」を判定し、判定結果が真であれば、ステップ１２１３で、関数ＴｙｐｅＯｆＯｐ（ｏｐ）［演演算子ｏｐのタイプを返す］の値を（Ｔ１、Ｔ２、Ｔ３）に、関数ＴｙｐｅＯｆＥｘｐ（ｅ１，ε）［宣言のリストεに属す式ｅ１のタイプを返す］の値をＴ’１に記録、関数ＴｙｐｅＯｆＥｘｐ（ｅ２，ε））［宣言のリストεに属す式ｅ２のタイプを返す］の値をＴ’２に記録する。ステップ１２１３終了後、
2004081788.tif 000083
否か」を判定する。判定結果が真であるなら、ステップ１２１５に進み「Ｔ’３のタイプはブール型でないが真か否か」を判定し、判定結果が真ならステップ１２１６でＳｕｐ（Ｔ’１，Ｔ’２）［Ｔ’１とＴ’２の２つのタイプのうち最も上位なタイプを返す］返し（ステップ１２１６）、処理を終了する。ステップ１２１５の結果が偽であったときは、ステップ１２１７でブール型を返して処理を終了する。ステップ１２１４の結果が偽であったときは、ステップ１２１８でエラーメッセージ（ＥｒｒＭｓｇ）出力して「ＴｙｐＥｒｒ」を返し、処理を終了する。
ステップ１２１２の結果が偽であったら、処理を終了する。
この関数がどのように機能するか、具体例をあげて説明する。
式が「ａ＋ｂ」で、「ａ」と「ｂ」はタイプが整数型（ｉｎｔ）である入力単語であるとすると、この式は「ｅ１  ｏｐ  ｅ２（式１  演算子  式２）」という型を持ち、この式の場合「ｅ１＝ａ」、「ｏｐ＝＋」、「ｅ２＝ｂ」となる。
従って、
ＴｙｐｅＯｆｏｐ（＋）＝Ｔｎｕｍ×Ｔｎｕｍ→Ｔｎｕｍ（演算子＋のタイプは、２つの数値のタイプの組をとり、数値のタイプを返す関数型）であるから、
（Ｔ１、Ｔ２、Ｔ３）＝（Ｔｎｕｍ、Ｔｎｕｍ、Ｔｎｕｍ）となり、
ＴｙｐｅＯｆＥｘｐ（ａ）＝ＴｙｐｅＯｆＥｘｐ（ｂ）＝ｉｎｔ（式ａ、式ｂもタイプが整数型ｉｎｔである単語であるから、ＴｙｐｅＯｆＥｘｐ（ａ）＝ＴｙｐｅＯｆＷｒｄ（ａ）＝ｉｎｔ、ＴｙｐｅＯｆＥｘｐ（ｂ）＝ＴｙｐｅＯｆＷｒｄ（ｂ）＝ｉｎｔとなるので）であるから、Ｔ’１＝ｉｎｔ、Ｔ’２＝ｉｎｔとなり、
前述のタイプの半順序定義により、
2004081788.tif 000084
条件が成立し、
Ｔ３＝ＴｎｕｍであるからＴ３≠ｂｏｏｌも成立する。
よって、関数ＴｙｐｅＯｆＥｘｐ（ａ＋ｂ）の最終結果として返すＳｕｐ（Ｔ’１，Ｔ’２）はＳｕｐ（ｉｎｔ，ｉｎｔ）＝ｉｎｔ（整数型と整数型のうち最も大きいタイプは整数型）となるので、次のような最終結果が導かれる。
ＴｙｐｅＯｆＥｘｐ（ａ＋ｂ）＝ｉｎｔ（式ａ＋ｂのタイプは、整数型ｉｎｔ）
もう１つの例として、もし「ａ」のタイプがフロート（浮動小数点数）型である場合は、その時は式「ａ＋ｂ」のタイプはフロート型である。なぜなら、
ＴｙｐｅＯｆＥｘｐ（ａ＋ｂ）において、ａ＝ｆｌｏａｔ、ｂ＝ｉｎｔの場合、
（Ｔ１、Ｔ２、Ｔ３）＝（Ｔｎｕｍ、Ｔｎｕｍ、Ｔｎｕｍ）となり、
ＴｙｐｅＯｆＥｘｐ（ａ）＝ｆｌｏａｔ、ＴｙｐｅＯｆＥｘｐ（ｂ）＝ｉｎｔ（式ａはタイプがフロート型ｆｌｏａｔの単語、式ｂはタイプが整数型ｉｎｔの単語であるから、ＴｙｐｅＯｆＥｘｐ（ａ）＝ＴｙｐｅＯｆＷｒｄ（ａ）＝ｆｌｏａｔ、ＴｙｐｅＯｆＥｘｐ（ｂ）＝ＴｙｐｅＯｆＷｒｄ（ｂ）＝ｉｎｔとなるので）であるから、Ｔ’１＝ｆｌｏａｔ、Ｔ’２＝ｉｎｔとなり、
前述のタイプの半順序定義により、
2004081788.tif 000085
ｎｕｍ）の条件が成立し、Ｔ３＝ＴｎｕｍであるからＴ３≠ｂｏｏｌも成立する。
よって、関数ＴｙｐｅＯｆＥｘｐ（ａ＋ｂ）の最終結果として返すＳｕｐ（Ｔ’１，Ｔ’２）は、Ｓｕｐ（ｆｌｏａｔ，ｉｎｔ）＝ｆｌｏａｔ（フロート型と整数型のうち上位のタイプはフロート型）となる。
より形式的に示すと、式のタイプは以下のタイピング規則によってとらえることができる：
2004081788.tif 000086
上記形式的記述が示す規則は、以下のとおりである。
（Ｃｓｔ）式が定数の場合の規則：
任意のＬｙｅｅ要件εをタイピングの環境とする定数ｃのタイプは、前提条件なしで、関数ＴｙｐｅＯｆＣｓｔ（ｃ）が返す値である。
（Ｗｒｄ）式が単語の場合の規則：
任意のＬｙｅｅ要件εをタイピングの環境とする単語ｗのタイプは、前提条件なしで、関数ＴｙｐｅＯｆＷｒｄ（ｗ，ε）が返す値である。
（Ｏｐ）式が演算子の場合の規則：
任意のＬｙｅｅ要件εをタイピングの環境とする演算子Ｏｐのタイプは、前提条件なしで、関数ＴｙｐｅＯｆＯｐ（Ｏｐ）が返す値である。
（Ｅｘｐｐ）式が括弧付き式の場合の規則：
任意のＬｙｅｅ要件εをタイピングの環境とする式（Ｅｘｐ）のタイプは、前提条件『任意のＬｙｅｅ要件εをタイピングの環境とする式ＥｘｐのタイプがＴ』が成立するとき、Ｔである。
（ＥｘｐＵ）式が「ｏｐ  Ｅｘｐ」の場合の規則：
前提条件『任意のＬｙｅｅ要件εをタイピングの環境とする、演算子ｏｐのタイプがＴ１→Ｔ２であって、式ＥｘｐのタイプがＴ’１であって、
2004081788.tif 000087
要件εをタイピングの環境とする式ｏｐ  Ｅｘｐのタイプは、Ｔ’１である。
（ＥｘｐＢＡ）式が「Ｅｘｐ  ｏｐ  Ｅｘｐ」で、演算結果がブール型でない場合の規則：
前提条件『任意のＬｙｅｅ要件εをタイピングの環境とする、演算子ｏｐのタイプがＴ１×Ｔ２→Ｔ３であって、式Ｅｘｐ１のタイプがＴ’１で
2004081788.tif 000088
つＴ３≠ｂｏｏｌである』が成立するとき、任意のＬｙｅｅ要件εをタイピングの環境とする式Ｅｘｐ１  ｏｐ  Ｅｘｐ２のタイプは、Ｓｕｐ（Ｔ’１，Ｔ’２）である。
（ＥｘｐＢＢ）式が「Ｅｘｐ  ｏｐ  Ｅｘｐ」で、演算結果がブール型の場合の規則：
前提条件『任意のＬｙｅｅ要件εをタイピングの環境とする、演算子ｏｐのタイプがＴ１×Ｔ２→ｂｏｏｌであって、式Ｅｘｐ１のタイプがＴ’１で
2004081788.tif 000089
ある』が成立するとき、任意のＬｙｅｅ要件εをタイピングの環境とする式Ｅｘｐ１  ｏｐ  Ｅｘｐ２のタイプは、ｂｏｏｌである。
（６−１−６）宣言のタイピング
式のタイプ判定方法が分かれば、Ｌｙｅｅ要件の任意の宣言のタイピングを行うことは非常に容易である。次の関数はＬｙｅｅ要件εにおける任意の宣言ｓのタイプを判定する。
2004081788.tif 000090
上記関数ＴｙｐＯｆＳｔａｔ（（Ｉｄ，Ｅｘｐ，Ｃｏｎｄ，ｉｏ，Ｔ，Ｔｓｅｃ），ε）の意味は以下のとおりである。関数の引数（Ｉｄ，Ｅｘｐ，Ｃｏｎｄ，ｉｏ，Ｔ，Ｔｓｅｃ）は、任意のＬｙｅｅ要件である宣言のリストεをタイピングの環境とする任意の宣言を構成する項目の値（ｉｄ＝単語の識別子、Ｅｘｐ＝定義式、Ｃｏｎｄ＝定義式実行条件式、ｉｏ＝入出力属性、Ｔ＝単語の値のタイプ、Ｔｓｅｃ＝単語の値セキュリティレベルを示すタイプ）である。
＜開始＞
＜Ｉｆ処理開始＞
もし、ｏｉ＝Ｉｆまたはｉｏ＝ＩＳかつＴが空なら［すなわち、宣言が入力単語のものでタイプ情報がないなら］、エラーメッセージを印刷し、「０」を返す［すなわち、タイプ判定は不可能］。
そうでなければ［すなわち、宣言が出力単語のものであるなら］、
＜Ｉｆ処理開始＞もし、関数ＴｙｐｅＯｆＥｘｐ（Ｅｘｐ）［定義式Ｅｘｐのタイプを返す］の結果がＴｙｐＥｒｒ［定義式のタイプがＴｙｐＥｒｒ、すなわちタイプが判定不可］であり、かつ、関数ＴｙｐｅＯｆＥｘｐ（Ｃｏｎｄ）［条件式Ｃｏｎｄのタイプ返す］の値がブール型なら、
結果として（Ｉｄ，Ｅｘｐ，Ｃｏｎｄ，ｉｏ，ＴｙｐｅＯｆＥｘｐ（Ｅｘｐ），Ｔｓｅｃ）を返す。
＜Ｉｆ処理終了＞
＜Ｉｆ処理終了＞
＜終了＞
図２１は、この関数ＴｙｐｅＯｆＳｔａｔ（（Ｉｄ，Ｅｘｐ，Ｃｏｎｄ，ｉｏ，Ｔ，Ｔｓｅｃ），ε）をフローチャートに示したものである。図２１を説明すると以下のとおりである。まず、「宣言のｉｏ項目がＩＦ［ファイルへの入力］またはＩＳ［画面への入力］、かつ項目Ｔが空［タイプ情報がない］か否か」を判定する（ステップ１３０１）。判定の結果が真なら、ステップ１３０２に進み、エラーメッセージ（ＥｒｒＭｓｇ）を印刷して「０」を返し、処理を終了する。
判定結果が偽なら、ステップ１３０３に進み、「関数ＴｙｐｅＯｆＥｘｐ（Ｅｘｐ）［定義式Ｅｘｐのタイプを返す］の結果がＴｙｐＥｒｒ［すなわちタイプが判定不可］であり、かつ、関数ＴｙｐｅＯｆＥｘｐ（Ｃｏｎｄ）［条件式Ｃｏｎｄのタイプ返す］の値がブール型、か否か」を判定する。判定結果が真なら、ステップ１３０４で（Ｉｄ，Ｅｘｐ，Ｃｏｎｄ，ｉｏ，ＴｙｐｅＯｆＥｘｐ（Ｅｘｐ），Ｔｓｅｃ）の値を返し、処理を終了する。判定結果が偽なら、処理を終了する。
形式的に表記すれば、この関数のタイピング規則は以下のとおりである。
2004081788.tif 000091
上記形式的記述が示す規則は、「前提条件『任意のＬｙｅｅ要件である宣言のリストεをタイピングの環境とする、定義式ＥｘｐのタイプがＴ１、同じく定義式実行条件式のタイプがブール型で、入出力属性がＩＳおよびＩＦでない』が成立する時、宣言のリストεをタイピングの環境とする宣言（Ｉｄ，Ｅｘｐ，Ｃｏｎｄ，ｉｏ，Ｔ，Ｔｓｅｃ）のタイプは、（Ｉｄ，Ｅｘｐ，Ｃｏｎｄ，ｉｏ，Ｔ１，Ｔｓｅｃ）である。」
（６−１−７）Ｌｙｅｅ要件のタイピング
任意の宣言の順序付けされたリストεがあるとき、そのリストのタイプ判定は以下のようになる。
2004081788.tif 000092
上記の関数ＴｙｐｅＯｆＬｙｅｅ（＜ｓ１，．．．，ｓｎ＞）の意味は以下の通りである。引数＜ｓ１，．．．，ｓｎ＞はＬｙｅｅ要件である宣言のリスト、変数ε０は宣言のリストである。
＜開始＞
変数ε０の領域に、宣言のリスト＜ｓ１，．．．，ｓｎ＞を記録する
＜Ｆｏｒ処理開始＞ｉに１からｎまでを代入し、下記を実行する
ｓ’ｉに、ＴｙｐｅＯｆＳｔａｔ（ｓｉ，εｉ−１）の結果を記録する
εｉには、εｉ−１の結果を記録する
εｉのｉ番目の要素を、ｓ’ｉに置き換える
＜Ｆｏｒ処理終了＞
εｎの値を返す
＜終了＞
たとえば、ｎ＝３であるような関数ＴｙｐｅｏｆＬｙｅｅ（＜ｓ１，ｓ２，ｓ３＞）は以下のようになる。
変数ε０の領域に、宣言のリスト＜ｓ１，ｓ２，ｓ３＞を記録する
＜Ｆｏｒ処理開始＞ｉ＝１のとき、
ｓ’１に、ＴｙｐｅＯｆＳｔａｔ（ｓ１，ε０）の結果を記録する
ε１には、ε０の結果を記録する
ε１の１番目の要素ｓ１を、ｓ’１の値で置き換える
ｉ＝２のとき、
ｓ’２に、ＴｙｐｅＯｆＳｔａｔ（ｓ２，ε１）の結果を記録する
ε２には、ε１の結果を記録する
ε２の２番目の要素ｓ２を、ｓ’２の値で置き換える
ｉ＝３のとき、
ｓ’３に、ＴｙｐｅＯｆＳｔａｔ（ｓ３，ε２）の結果を記録する
ε３には、ε２の結果を記録する
ε３の３番目の要素ｓ３を、ｓ’３の値で置き換える
＜Ｆｏｒ処理終了＞
結果としてε３の値＜ｓ’１，ｓ’２，ｓ’３＞を返す
＜終了＞
図２２は、この関数ＴｙｐｅＯｆＬｙｅｅ（＜ｓ１，．．．，ｓｎ＞）をフローチャートに示したものである。図２２を説明すると次のとおりである。まず、変数ε０の領域に、宣言のリスト＜ｓ１，．．．，ｓｎ＞を記録する（ステップ１４０１）。次に、ｉに１を加算す（ステップ１４０２）、ステップ１４０３に進む。ステップ１４０３で「ｉの値がｎか否か」を判定し、結果が偽であれば、ｓ’ｉにＴｙｐｅＯｆＳｔａｔ（ｓｉ，εｉ−１）の結果を記録、εｉにεｉ−１の結果を記録し、εｉのｉ番目の要素をｓ’ｉに置き換える（ステップ１４０４）。ステップ１４０４終了後、ステップ１４０２に戻り再度実行する。ステップ１４０３の結果が偽である限り、ステップ１４０２からステップ１４０４の再起処理（１４０６）を繰り返す。
ステップ１４０３の結果が真になったとき、ステップ１４０５でεｎの値を返して処理を終了する。このとき、εｎの値は＜ｓ’１，・・・ｓ’ｎ＞になっている。
形式的に表せば、この関数に関連づけられたタイピング規則は次のとおりである。
2004081788.tif 000093
上記形式的記述が示す規則は、「前提条件『Ｌｙｅｅ要件である宣言のリストεをタイピング環境とする宣言ｓ１のタイプがｓ’１、ｓ１にｓ’１が代入されたのちの宣言のリストεをタイピング環境とする＜ｓ２，．．．，ｓ’ｎ＞のタイプが＜ｓ’２，．．．，ｓ’ｎ＞である』が成立するとき、Ｌｙｅｅ要件である宣言のリストεをタイピング環境とする宣言のリスト＜ｓ１，．．．，ｓｎ＞のタイプは、＜ｓ’１，．．．，ｓ’ｎ＞である」、ことを意味している。
最終的に、順序付けされたＬｙｅｅ要件に関連づけられたタイプ判定の完全なシステムは次の通りである。
2004081788.tif 000094
上記形式的記述が示す規則は、以下のとおりである。
（Ｃｓｔ）式が定数の場合の規則：
Ｌｙｅｅ要件である宣言のリストεをタイピング環境とする定数ｃのタイプは、前提条件なしで、関数ＴｙｐｅＯｆＣｓｔ（ｃ）が返す値である。
（Ｗｒｄ）式が単語の場合の規則：
Ｌｙｅｅ要件である宣言のリストεをタイピング環境とする単語ｗのタイプは、前提条件なしで、関数ＴｙｐｅＯｆＷｒｄ（ｗ，ε）が返す値である。
（Ｏｐ）式が演算子の場合の規則：
Ｌｙｅｅ要件である宣言のリストεをタイピング環境とする演算子Ｏｐのタイプは、前提条件なしで、関数ＴｙｐｅＯｆＯｐ（Ｏｐ）が返す値である。
（Ｅｘｐｐ）式が括弧付き式の場合の規則：
Ｌｙｅｅ要件である宣言のリストεをタイピング環境とする式（Ｅｘｐ）のタイプは、前提条件『Ｌｙｅｅ要件である宣言のリストεをタイピング環境とする式ＥｘｐのタイプがＴ』が成立するとき、Ｔである。
（ＥｘｐＵ）式が「ｏｐ  Ｅｘｐ」の場合の規則：
前提条件『Ｌｙｅｅ要件である宣言のリストεをタイピング環境とする、演算子ｏｐのタイプがＴ１→Ｔ２であって、式ＥｘｐのタイプがＴ
2004081788.tif 000095
る宣言のリストεをタイピング環境とする式ｏｐ  Ｅｘｐのタイプは、Ｔ’１である。
（ＥｘｐＢＡ）式が「Ｅｘｐ  ｏｐ  Ｅｘｐ」で、演算結果がブール型でない場合の規則：
前提条件『Ｌｙｅｅ要件である宣言のリストεをタイピング環境とする、演算子ｏｐのタイプがＴ１×Ｔ２→Ｔ３であって、式Ｅｘｐ１のタイ
2004081788.tif 000096
る宣言のリストεをタイピング環境とする式Ｅｘｐ１  ｏｐ  Ｅｘｐ２のタイプは、Ｓｕｐ（Ｔ’１，Ｔ’２）である。
（ＥｘｐＢＢ）式が「Ｅｘｐ  ｏｐ  Ｅｘｐ」で、演算結果がブール型の場合の規則：
前提条件『Ｌｙｅｅ要件である宣言のリストεをタイピング環境とする、演算子ｏｐのタイプがＴ１×Ｔ２→ｂｏｏｌであって、式Ｅｘｐ１のタイ
2004081788.tif 000097
εをタイピング環境とする式Ｅｘｐ１  ｏｐ  Ｅｘｐ２のタイプは、ｂｏｏｌである。
（６−２）ケーススタディ
以下に、Ｌｙｅｅ要件にタイプチェックを適用することの重要性を示す２つの例を提示する。１番目の例は、タイピングシステムが、どのように正しくタイプ違反に関するエラーを検出するかを示す。２番目の例は、タイピングシステムによるタイプの自動的な生成を示す。
＜例１＞
表２６のような初期要件が与えられている。上記の述べたように、タイプの検証の前に、まず宣言の最適順序付けが必要である。従って、タイプの検証は表２７に示された要件の順序づけられたバージョンに対して行われる。
2004081788.tif 000098
2004081788.tif 000099
2004081788.tif 000100
表２７の順序づけられた要件に対してタイピング分析を行うと、返される結果は、要件に以下のようなタイプエラーがあることを示す。
・宣言ｄのエラー：式（ｔｒｕｅ）は数値（ｉｎｔあるいはｆｌｏａｔ）ではない。
・宣言ｃに対する警告：タイプ（ｉｎｔ）は（ｂｏｏｌ）に修正されている。
・宣言ｇに対する警告：タイプ（ｉｎｔ）は（ｂｏｏｌ）に修正されている。
・宣言ｆに対する警告：タイプ（ｆｌｏａｔ）は（ｂｏｏｌ）に修正されている。
・宣言ｈに対する警告：タイプ（ｉｎｔ）は（ｂｏｏｌ）に修正されている。
タイピングによって正しいタイプが新生成された要件は、表２８に示された通りである。
2004081788.tif 000101
2004081788.tif 000102
＜例ＩＩ＞
上述のとおり、タイプシステムは、入力単語以外の、すべての単語のタイプを自動的に生成することも可能である。このことを以下に具体例で示す。
表２９の要件に示されるように、与えられたタイプは入力単語のタイプのみである。この要件の順序付けをした後の要件（表３０）にタイプチェックのシステムを適用すると、表３１のような結果となる。
2004081788.tif 000103
2004081788.tif 000104
2004081788.tif 000105
７．セキュリティ・タイピング
次に、我々はＬｙｅｅ方法論がセキュリティなど、ソフトウェア開発の他の多くの局面を扱うのにいかに適当であるかを示す。実際、プログラムが敵対的環境で実行されるとき、生成されたコードがデータ機密性や保全性などの何らかのセキュリティ方針を満たすことを証明するために、上に提示したタイピング技術を容易に拡大適用させることができる。その主眼は、ユーザがセキュリティ要件を表すセキュリティラベル（「公開」、および、「非公開」など）を、セキュリティ方針（例えば、非公開の単語の値を公開の単語に格納することができない、など）と共に、それぞれの定義された単語に明確に付与するのを可能にすることである。これらの与えられた情報から、セキュリティ違反を発生させる余地のある微妙な設計上の欠陥を明らかにするために、自動的プログラム検証用タイプチェック技術を使用することができる。
例えば、表３２で与えられている宣言の中に示されるセキュリティラベルによって要件を拡張するとする。
2004081788.tif 000106
セキュリティ方針が、非公開の単語の値を公開のものに影響させるのを禁じるものであるとする。また、非公開の値を別の値（非公開の、または、公開の）に添加した結果も非公開であると考えられなければならないとしよう。したがって、中に公開の単語ａが非公開の値を受けているので、表３２で示された要件はセキュリティ方針を遵守しないということが明らかである。
（７−１）セキュリティ・タイピング規則
タイピングの検証と同様に、セキュリティの検証も下記の要素を用いる。このセクションでは、任意のＬｙｅｅ要件に現れる単語、定数、演算子に属す、異なったタイプを定義する。
（７−１−１）基本的なセキュリティ・タイプ
＜値のセキュリティ・タイプ＞
単純化のために、単語と定数のセキュリティ・タイプは、ｐｕｂｌｉｃ（公開）、またはｓｅｃｒｅｔ（非公開）であるとする。
2004081788.tif 000107
上記定義は、「値のセキュリティ・タイプ（Ｔｓｖａｌ）は、ｐｕｂｌｉｃ（公開）またはｓｅｃｒｅｔ（非公開）である」ことを意味している。
＜演算子のセキュリティ・タイプ＞
同じくＬｙｅｅ要件に関与し得るブール演算子および算術演算子のセキュリティ・タイプを明確にしなければならない。各演算子について、その演算数のセキュリティ・タイプとその結果のタイプについて明確にする必要がある。任意の演算子のセキュリティ・タイプは、通常Ｔｓ１→Ｔｓ２の形式を取る。
直感的にわかるように、この形式的記述は、１つの演算子とは、入力としてセキュリティ・タイプＴｓ１をとったときにセキュリティ・タイプＴｓ２を返す関数である、と見なせることを意味している。言うまでもなく、いくつかの演算子は１つ以上のオペランドを取る。従って、セキュリティ・タイプはそれ自身が１対のセキュリティ・タイプの場合もあると見なせば、このようなケースを説明することは容易である。
まとめると、セキュリティ・タイプはＴｓｖａｌ（１つの値のセキュリティ・タイプ）、１対のセキュリティ・タイプＴｓ１×Ｔｓ２、あるいはＴｓ１→Ｔｓ２である。
より形式的に示せば次のように書くことができる。
2004081788.tif 000108
上記形式的記述は、「セキュリティ・タイプ（ＴＳ）は、Ｔｓｖａｌ、またはＴｓ１×Ｔｓ２、またはＴｓ１→Ｔｓ２」であることを意味している。
（７−１−２）定数のセキュリティ・タイピング
Ｌｙｅｅ要件のセキュリティチェックする場合、宣言中に見つかる定数のセキュリティ・タイプは、下記に示すように単純にｐｕｂｌｉｃである。
2004081788.tif 000109
すなわち、定数が、ｔｒｕｅ（真）またはｆａｌｓｅ（偽）の場合も、ｎｕｍ（数値）の場合も、ｎｕｍ．ｎｕｍ（浮動小数点数値）の場合も、セキュリティ・タイプはｐｕｂｌｉｃ（公開）である。タイピングの検証と同様に、次の関数によって、任意の定数のセキュリティ・タイプを判定できる。
2004081788.tif 000110
上記関数ＳｅｃＴｙｐｅＯｆＣｓｔ（ｃｓｔ）の意味は下記のとおりである。
関数の引数ｃｓｔは定数を意味する。
＜開始＞
値ｐｕｂｌｉｃを返す
＜終了＞
定数のセキュリティ・タイピングは、次の規則によって形式化できる：
2004081788.tif 000111
上記形式的記述は、「Ｌｙｅｅ要件である宣言のリストεをセキュリティ・タイピング環境とする定数ｃのセキュリティ・タイプは、前提条件なしで、ＳｅｃＴｙｐｅＯｆＣｓｔ（ｃ）の結果の値」であることを意味している。
（７−１−３）単語のセキュリティ・タイピング
どんな入力単語でも、ユーザはそのセキュリティ・タイプについて絶対に正確でなくてはならない。その他の単語については、セキュリティ・タイプは自動的に算出され、これらの単語を定義している宣言の領域「セキュリティ」に記録される。既に分かっている単語があるとき、単語のセキュリティ・タイプを返す関数ＳｅｃＴｙｐｅＯｆＷｒｄを以下のように定義する。
2004081788.tif 000112
上記関数ＳｅｃＴｙｐｅＯｆＷｏｒｄ（ｗ，ε）の意味は下記のとおりである。
関数の引数ｗは、要件εに属する任意の単語を意味する。
＜開始＞
要件εに属す単語ｗの宣言（Ｓｔａｔｅｍｅｎｔ（ｗ，ε））の、セキュリティ・タイプの値（Ｓｅｃｕｒｉｔｙ（＊）、＊はＳｔａｔｅｍｅｎｔ（ｗ，ε）で求めた宣言）を返す
＜終了＞
単語のセキュリティ・タイピングは、次の規則によって形式化できる。
2004081788.tif 000113
上記形式的記述は、「Ｌｙｅｅ要件である宣言のリストεをセキュリティ・タイピング環境とする単語ｗのセキュリティ・タイプは、前提条件なしで、ＳｅｃＴｙｐｅＯｆＷｒｄ（ｗ，ε）の結果の値である」ことを意味している。
（７−１−４）式のセキュリティ・タイピング
以下に、各種類の式のセキュリティ・タイプを判定する方法を示す。
式のセキュリティ・タイピングの説明を単純化するために、セキュリテ
2004081788.tif 000114
2004081788.tif 000115
前記の半順序関係を使って、２つのセキュリティ・タイプのうちの上位のものを以下のように定義できる。
2004081788.tif 000116
上記の記述は、「Ｔｓ１とＴｓ２のうち上位のタイプは（Ｓｕｐ（Ｔｓ１，Ｔｓ２））、
2004081788.tif 000117
を意味する。
式は以下うちの１つ、すなわち、ｖａｌ（値）、またはｉｄ（単語の識別子）、または（Ｅｘｐ）（括弧付き式）、またはｏｐ  Ｅｘｐ（演算子  式）、またはＥｘｐ  ｏｐ  Ｅｘｐ（式  演算子  式）であるから、
2004081788.tif 000118
次の関数によって、式の各種類ごとにセキュリティ・タイプを関連づけることができる。
2004081788.tif 000119
上記関数ＳｅｅＴｙｐＯｆＥｘｐ（ｅ，ε）の意味は以下のとおりである。
関数の引数ｅは、要件εに属す任意の式である。
＜開始＞
関数Ｓｗｉｔｃｈ（ｅ）の実行
引数ｅがｃ（定数）の場合、ＳｅｅＴｙｐｅＯｆＣｓｔ（ｃ）の結果の値を返す
引数ｅがｗ（単語）の場合、ＳｅｃＴｙｐｅＯｆＷｒｄ（ｗ）の結果の値を返す
引数ｅがｅ１（式）の場合、ＳｅｅＴｙｐｅＯｆＥｘｐ（ｅ１，ε）の結果の値を返す
引数ｅがｏｐ  ｅ１（演算子  式）の場合、ＳｅｅＴｙｐｅＯｆＥｘｐ（ｅ１）の結果の値を返す
引数ｅがｅ１  ｏｐ  ｅ２（式  演算子  式）場合、
Ｔｓ１にＳｅｃＴｙｐｅＯｆＥｘｐ（ｅ１，ε）を記録
Ｔｓ２にＳｅｃＴｙｐｅＯｆＥｘｐ（ｅ２，ε）を記録
ＳｅｃＳｕｐ（Ｔｓ１，Ｔｓ２）を返す
関数Ｓｗｉｔｃｈ終了
＜終了＞
図２３は、この関数ＳｅｃＴｙｐｅＯｆＥｘｐ（ｅ，ε）をフローチャートに示したものである。図２３を説明すると次のようになる。まず、「式ｅが定数か否か」を判定し（ステップ１５０１）、結果が真であれば、関数ＳｅｃＴｙｐｅＯｆＣｓｔ（ｃ）［定数ｃのセキュリティ・タイプを返す］の結果を返し（ステップ１５０２）、処理を終了する。
ステップ１５０１の結果が偽であれば、ステップ１５０３に進み、「式ｅが単語か否か」を判定し、判定結果が真であれば、関数ＳｅｃＴｙｐｅＯｆＷｏｒｄ（ｗ）［単語ｗのセキュリティ・タイプを返す］の結果を返し（ステップ１５０４）、処理を終了する。
ステップ１５０３の結果が偽であれば、ステップ１５０５に進み、「式ｅが「ｅ１」型（式）の式か否か」を判定し、結果が真であれば、関数ＳｅｃＴｙｐｅＯｆＥｘｐ（ｅ１，ε）［宣言のリストεに属す式ｅ１のセキュリティ・タイプを返す］の結果を返し（ステップ１５０６）、処理を終了する。
ステップ１５０５の結果が偽であれば、ステップ１５０７に進み、「式ｅが「ｏｐ  ｅ１」型（単項演算子  式）の式か否か」を判定し、判定結果が真であれば、関数ＳｅｃＴｙｐｅＯｆＥｘｐ（ｅ１）［式ｅ１のセキュリティ・タイプを返す］の結果を返す（ステップ１５０８）。
ステップ１５０７の判定結果が偽であれば、ステップ１５０９に進む。ステップ１５０９では、「式ｅが「ｅ１  ｏｐ  ｅ２」型（式  二項演算子  式）の式か否か」を判定し、判定結果が真であれば、ステップ１５１０で、Ｔｓ１にＳｅｃＴｙｐｅＯｆＥｘｐ（ｅ１，ε）を記録、Ｔｓ２にＳｅｃＴｙｐｅＯｆＥｘｐ（ｅ２，ε）を記録、そしてＳｅｃＳｕｐ（Ｔｓ１，Ｔｓ２）を返し、処理を終了する。
ステップ１５０９の結果が偽であったら、処理を終了する。
より形式的に示せば、式のセキュリティ・タイピングは次の規則によって捉えることができる。
2004081788.tif 000120
上記形式的記述が示す規則は、以下のとおりである。
（Ｃｓｔ）式が定数の場合の規則：
Ｌｙｅｅ要件である宣言のリストεをセキュリティ・タイピング環境とする定数ｃのタイプは、前提条件なしで、関数ＳｅｃＴｙｐｅＯｆＣｓｔ（ｃ）が返す値である。
（Ｗｒｄ）式が単語の場合の規則：
Ｌｙｅｅ要件である宣言のリストεをセキュリティ・タイピング環境とする単語ｗのタイプは、前提条件なしで、関数ＳｅｃＴｙｐｅＯｆＷｒｄ（ｗ，ε）が返す値である。
（ＥｘｐＰ）式が括弧付き式の場合の規則：
Ｌｙｅｅ要件である宣言のリストεをセキュリティ・タイピング環境とする式（Ｅｘｐ）のタイプは、前提条件『Ｌｙｅｅ要件である宣言のリストεをセキュリティ・タイピング環境とする式ＥｘｐのタイプがＴｓ』が成立するとき、Ｔｓである。
（ＥｘｐＵ）式が「Ｏｐ  Ｅｘｐ」の場合の規則：
前提条件『Ｌｙｅｅ要件である宣言のリストεをセキュリティ・タイピング環境とするＥｘｐ（式）のタイプがＴｓである』が成立するとき、Ｌｙｅｅ要件である宣言のリストεをセキュリティ・タイピング環境とするＯｐ  Ｅｘｐ（演算子式）のタイプは、Ｔｓである。
（ＥｘｐＢ）式が「Ｅｘｐ  ｏｐ  Ｅｘｐ」の場合の規則：
前提条件『Ｌｙｅｅ要件である宣言のリストεをセキュリティ・タイピング環境とする、式Ｅｘｐ１のタイプがＴｓ１であって、式Ｅｘｐ２のタイプがＴｓ２である』が成立するとき、Ｌｙｅｅ要件である宣言のリストεをセキュリティ・タイピング環境とする式Ｅｘｐ１  Ｏｐ  Ｅｘｐ２のタイプは、Ｓｕｐ（Ｔｓ１，Ｔｓ２）である。
（７−１−５）宣言のセキュリティ・タイピング
次の関数は、Ｌｙｅｅ要件εの中の任意の宣言ｓにセキュリティ・タイプを関連づける。
2004081788.tif 000121
上記関数ＳｅｃＴｙｐＯｆＳｔａｔ（（Ｉｄ，Ｅｘｐ，Ｃｏｎｄ，ｉｏ，Ｔ，Ｔｓｅｃ），ε）の意味は以下のとおりである。関数の引数（Ｉｄ，Ｅｘｐ，Ｃｏｎｄ，ｉｏ，Ｔ，Ｔｓｅｃ）は、Ｌｙｅｅ要件εに属す任意の宣言を構成する項目の値（Ｉｄ＝単語の識別子、Ｅｘｐ＝定義式、Ｃｏｎｄ＝定義式実行条件、ｉｏ＝入出力属性、Ｔ＝単語の値のタイプ、Ｔｓｅｃ＝単語のセキュリティレベルを示すタイプ）である。
＜開始＞
＜Ｉｆ文開始＞もし、ｉｏ＝ＩＦまたはｉｏ＝ＩＳ、かつＴｓｅｃが空であるなら［すなわち、入出力属性ｉｏが入力でセキュリティ・タイプの情報が与えられていないなら］、ＥｒｒＭｓｇを印刷し、「０」を返す［セキュリティ・タイプの判定ができないので、エラーメッセージを印刷し、０を返す］
そうでないなら、
2004081788.tif 000122
リティ・タイプが定義式のセキュリティ・タイプより上位］で、かつ、ｏｉ≠ＯＳかつｏｉ≠ＯＦである［ｉｏが出力でない、すなわち入力］なら、（Ｉｄ，Ｅｘｐ，Ｃｏｎｄ，ｉｏ，Ｔ，Ｔｓｅｃ）を返す
＜Ｉｆ処理終了＞
2004081788.tif 000123
のセキュリティ・タイプ（ｓｅｃｒｅｔでない）が定義式のセキュリティ・タイプより上位］で、かつ、ｉｏ＝ＯＳまたはｉｏ≠ＯＦ［ｉｏが画面への出力、またはファイルへの出力］であるなら、（Ｉｄ，Ｅｘｐ，Ｃｏｎｄ，ｉｏ，Ｔ，Ｔｓｅｃ）を返す
そうでないなら、ＥｒｒＭｓｇ（エラーメッセージ）を返す
＜Ｉｆ処理終了＞
＜Ｉｆ処理終了＞
＜終了＞
図２４は、この関数ＳｅｃＴｙｐｅＯｆＳｔａｔ（（Ｉｄ，Ｅｘｐ，Ｃｏｎｄ，ｉｏ，Ｔ，Ｔｓｅｃ），ε）をフローチャートに示したものである。図２４を説明すると以下のとおりである。まず、「宣言のｉｏ項目がＩＦ［ファイルへの入力］またはＩＳ［画面への入力］、かつ項目Ｔが空［タイプ情報がない］か否か」を判定する（ステップ１６０１）。判定の結果が真なら、ステップ１６０２に進み、エラーメッセージ（ＥｒｒＭｓｇ）を印刷して「０」を返し、処理を終了する。
2004081788.tif 000124
Ｔｓｅｃ［宣言のセキュリティ・タイプが定義式のセキュリティ・タイプより上位］で、かつ、ｏｉ≠ＯＳかつｏｉ≠ＯＦである［ｉｏが出力でない、すなわち入力］か否か」を判定する。判定結果が真なら、ステップ１５０４でなら、（Ｉｄ，Ｅｘｐ，Ｃｏｎｄ，ｉｏ，Ｔ，Ｔｓｅｃ）を返し、処理を終了する。
ステップ１５０３の判定結果が偽なら、ステップ１５０５に進み、
2004081788.tif 000125
（ｓｅｃｒｅｔでない）が定義式のセキュリティ・タイプより上位］で、かつ、ｉｏ＝ＯＳまたはｉｏ≠ＯＦ［ｉｏが画面への出力、またはファイルへの出力］か否か」を判定する。結果が真なら、ステップ１５０６で（Ｉｄ，Ｅｘｐ，Ｃｏｎｄ，ｉｏ，Ｔ，Ｔｓｅｃ）の値を返し、処理を終了する。
ステップ１５０５の結果が偽なら、エラーメッセージ（ＥｒｒＭｓｇ）を返し（ステップ１５０７）、処理を終了する。
形式的に記述すると、この関数に関連づけられたタイピング規則は以下のとおりである。
2004081788.tif 000126
すなわち、上記形式的記述は、次の意味である。
（Ｓｔａｔ１）出力単語の欠けているセキュリティ・タイプ情報を生成する場合：
前提条件『Ｌｙｅｅ要件である宣言のリストεをセキュリティ・タイピング環境とする定義式ＥｘｐのタイプがＴｓ１であって、宣言の入出力属性が入力でない（ｉｏ≠ＩＳかつｉｏ≠ＩＦ）』が成立するとき、Ｌｙｅｅ要件である宣言のリストεをセキュリティ・タイピング環境とする宣言（Ｉｄ，Ｅｘｐ，Ｃｏｎｄ，ｉｏ，Ｔ，“”）のタイプは、（Ｉｄ，Ｅｘｐ，Ｃｏｎｄ，ｉｏ，Ｔ，Ｔｓ１）である。
（Ｓｔａｔ２）出力単語のセキュリティ・タイプ情報をチェック、訂正する場合：
前提条件『Ｌｙｅｅ要件である宣言のリストεをセキュリティ・タイピング環境とする、定義式ＥｘｐのタイプがＴｓ１であって、そのＴｓ１が宣言
2004081788.tif 000127
属性が入力でない（ｉｏ≠ＩＳかつｉｏ≠ＩＦ）』が成立するとき、Ｌｙｅｅ要件である宣言のリストεをセキュリティ・タイピング環境とする宣言（Ｉｄ，Ｅｘｐ，Ｃｏｎｄ，ｉｏ，Ｔ，Ｔｓｅｃ）のタイプは、（Ｉｄ，Ｅｘｐ，Ｃｏｎｄ，ｉｏ，Ｔ，Ｔｓ１）である。
（７−１−６）Ｌｙｅｅ要件のセキュリティ・タイピング
順序付された宣言のリストεがあったとき、下記の関数によって、その宣言の各々にセキュリティ・タイプを関連づけることができる。
2004081788.tif 000128
上記の関数ＳｅｃＴｙｐｅＯｆＬｙｅｅ（＜ｓ１，．．．，ｓｎ＞）の意味は以下のとおりである。
関数の引数＜ｓ１，．．．，ｓｎ＞は、任意の宣言のリストである。変数ε０の値は宣言のリストである。
＜開始＞
ε０に宣言のリスト＜ｓ１，．．．，ｓｎ＞を記録する。
ｉは１からｎをとる時、下記を実行する
ｓ’ｉに、ＳｅｃＴｙｐｅＯｆＳｔａｔ（ｓｉ，εｉ−１）の値を記録する
εｉに、εｉ−１の値を記録する
εｉのｉ番目の要素を、ｓ’ｉで置き換える。
＜Ｆｏｒ処理終了＞
εｎを返す
＜終了＞
図２５は、この関数ＳｅｃＴｙｐｅＯｆＬｙｅｅ（＜ｓ１，．．．，ｓｎ＞）をフローチャートに示したものである。図２５を説明すると次のとおりである。まず、変数ε０の領域に、宣言のリスト＜ｓ１，．．．，ｓｎ＞を記録する（ステップ１７０１）。次に、ｉに１を加算す（ステップ１７０２）、ステップ１７０３に進む。ステップ１４０３で「ｉの値がｎか否か」を判定し、結果が偽であれば、ｓ’ｉにＳｅｃＴｙｐｅＯｆＳｔａｔ（ｓｉ，εｉ−１）の結果を記録、εｉにεｉ−１の結果を記録し、εｉのｉ番目の要素をｓ’ｉに置き換える（ステップ１７０４）。ステップ１７０４終了後、ステップ１７０２に戻り再度実行する。ステップ１４０３の結果が偽である限り、ステップ１７０２からステップ１７０４の再起処理（１７０６）を繰り返す。
ステップ１７０３の結果が真になった時、ステップ１７０５でεｎの値を返して処理を終了する。このとき、εｎの値は＜ｓ’１，・・・，ｓ’ｎ＞になっている。
形式的に記述すると、上記関数のセキュリティ・タイピング規則は以下のとおりである。
2004081788.tif 000129
上記形式的記述が示す規則は、「前提条件『Ｌｙｅｅ要件である宣言のリストεをセキュリティ・タイピング環境とする宣言ｓ１のセキュリティ・タイプがｓ’１、ｓ１にｓ’１が代入されたのちの宣言のリストεをセキュリティ・タイプの環境とするせ＜ｓ２，．．．，ｓ’ｎ＞のセキュリティ・タイプが＜ｓ’２，．．．，ｓ’ｎ＞である』が成立するとき、Ｌｙｅｅ要件である宣言のリストεをセキュリティ・タイピング環境とする宣言のリスト＜ｓ１，．．．，ｓｎ＞のセキュリティ・タイプは、＜ｓ’１，．．．，ｓ’ｎ＞である」、ことを意味している。
2004081788.tif 000130
最後に、順序付け済みＬｙｅｅ要件に関する完全なセキュリティ・タイプシステムは次のとおりである。
（Ｃｓｔ）式が定数の場合の式のセキュリティ・タイプ：
Ｌｙｅｅ要件である宣言のリストεをセキュリティ・タイピング環境とする定数ｃのタイプは、前提条件なしで、関数ＳｅｃＴｙｐｅＯｆＣｓｔ（ｃ）が返す値である。
（Ｗｒｄ）式が単語の場合の式のセキュリティ・タイプ：
Ｌｙｅｅ要件である宣言のリストεをセキュリティ・タイピング環境とする単語ｗのタイプは、前提条件なしで、関数ＳｅｃＴｙｐｅＯｆＷｒｄ（ｗ，ε）が返す値である。
（ＥｘｐＰ）式が括弧付き式の場合の式のセキュリティ・タイプ：
Ｌｙｅｅ要件である宣言のリストεをセキュリティ・タイピング環境とする式（Ｅｘｐ）のタイプは、前提条件『Ｌｙｅｅ要件である宣言のリストεをセキュリティ・タイピング環境とする式ＥｘｐのタイプがＴｓ』が成立するとき、Ｔｓである。
（ＥｘｐＵ）式が「Ｏｐ  Ｅｘｐ」の場合の式のセキュリティ・タイプ：
前提条作『Ｌｙｅｅ要件である宣言のリストεをセキュリティ・タイピング環境とするＥｘｐ（式）のタイプがＴｓである』が成立するとき、Ｌｙｅｅ要件である宣言のリストεをセキュリティ・タイピング環境とするＯｐ  Ｅｘｐ（演算子式）のタイプは、Ｔｓである。
（ＥｘｐＢ）式が「Ｅｘｐ  ｏｐ  Ｅｘｐ」の場合の式のセキュリティ・タイプ：
前提条件『Ｌｙｅｅ要件である宣言のリストεをセキュリティ・タイピング環境とする、式Ｅｘｐ１のタイプがＴｓ１であって、式Ｅｘｐ２のタイプがＴｓ２である』が成立するとき、Ｌｙｅｅ要件である宣言のリストεをセキュリティ・タイピング環境とする式Ｅｘｐ１  Ｏｐ  Ｅｘｐ２のタイプは、Ｓｕｐ（Ｔｓ１，Ｔｓ２）である。
（Ｓｔａｔ１）出力単語の欠けているセキュリティ・タイプ情報を生成する場合：
前提条件『Ｌｙｅｅ要件である宣言のリストεをセキュリティ・タイピング環境とする定義式ＥｘｐのタイプがＴｓ１であって、宣言の入出力属性が入力でない（ｉｏ≠ＩＳかつｉｏ≠ＩＦ）』が成立するとき、Ｌｙｅｅ要件である宣言のリストεをセキュリティ・タイピング環境とする宣言（Ｉｄ，Ｅｘｐ，Ｃｏｎｄ，ｉｏ，Ｔ，“”）のタイプは、（Ｉｄ，Ｅｘｐ，Ｃｏｎｄ，ｉｏ，Ｔ，Ｔｓ１）である。
（Ｓｔａｔ２）出力単語のセキュリティ・タイプ情報をチェック、訂正する場合：
前提条件『Ｌｙｅｅ要件である宣言のリストεをセキュリティ・タイピング環境とする、定義式ＥｘｐのタイプがＴｓ１であって、そのＴｓ１
2004081788.tif 000131
Ｔｓｅｃ）、入出力属性が入力でない（ｉｏ≠ＩＳかつｉｏ≠ＩＦ）』が成立するとき、Ｌｙｅｅ要件である宣言のリストεをセキュリティ・タイピング環境とする宣言（Ｉｄ，Ｅｘｐ，Ｃｏｎｄ，ｉｏ，Ｔ，Ｔｓｅｃ）のタイプは、（Ｉｄ，Ｅｘｐ，Ｃｏｎｄ，ｉｏ，Ｔ，Ｔｓ１）である。
（Ｒｅｑ）順序付けされたＬｙｅｅ要件のセキュリティ・タイプ：
前提条件『Ｌｙｅｅ要件である宣言のリストεをセキュリティ・タイピング環境とする宣言ｓ１のセキュリティ・タイプがｓ’１、ｓ１にｓ’１が代入された後の宣言のリストεをセキュリティ・タイプの環境とする＜ｓ２，．．．，ｓ’ｎ＞のセキュリティ・タイプが＜ｓ’２，．．．，ｓ’ｎ＞である』が成立するとき、Ｌｙｅｅ要件である宣言のリストεをセキュリティ・タイピング環境とする宣言のリスト＜ｓ１，．．．，ｓｎ＞のセキュリティ・タイプは、＜ｓ’１，．．．，ｓ’ｎ＞である。
（７−２）ケーススタディ
前述の表３１のＬｙｅｅ要件に、セキュリティ・タイピングを行うと、次のエラーが検出される。
・宣言ｃのエラー：単語ｃのタイプは、ｐｕｂｌｉｃ（公開）となっているが、定義式はｓｅｃｒｅｔ（非公開）の単語を含み（定義式ａ＝６の単語ａがｓｅｃｒｅｔ）、その影響を受けるので矛盾する。
・宣言ｂのエラー：単語ｂのタイプは、ｐｕｂｌｉｃ（公開）となっているが、定義式はｓｅｃｒｅｔ（非公開）の単語を間接的に含み（定義式ｃの単語ｃの定義式ａ＝６の単語ａがｓｅｃｒｅｔ）、その影響を受けるので矛盾する。
・宣言ｄのエラー：単語ｄのタイプは、ｐｕｂｌｉｃ（公開）となっているが、定義式はｓｅｃｒｅｔ（非公開）の単語を含み（定義式ａ＋６の単語ａがｓｅｃｒｅｔ）、その影響を受けるので矛盾する。
・宣言ｇのエラー：単語ｇのタイプは、ｐｕｂｌｉｃ（公開）となっているが、定義式はｓｅｃｒｅｔ（非公開）の単語を間接的に含み（定義式ｄ＝９の単語ｄの定義式ａ＋６の単語ａがｓｅｃｒｅｔ）、その影響を受けるので矛盾する。
・宣言ｆのエラー：単語ｆのタイプはｓｅｃｒｅｔ（非公開）であるが、単語ｆは出力の１つであるので矛盾する（セキュリティ・タイプがｓｅｃｒｅｔである値は出力しない方針であるから）。
・宣言ｈのエラー：単語ｈのタイプは、ｐｕｂｌｉｃ（公開）となっているが、定義式はｓｅｃｒｅｔ（非公開）の単語を間接的に含み（定義式ｆの単語ｆの定義式がｇ、単語ｇの定義式がｄ＝９、単語ｄの定義式がａ＋６で単語ａがｓｅｃｒｅｔ）、その影響を受けるので矛盾する。
８．Ｌｙｅｅ要件分析器
Ｌｙｅｅ要件分析器は、我々が以前に議論した静的な分析技術を部分的に実現するために生み出した原型である。それは入力としてＬｙｅｅ要件をうけ取り、ＬｙｅｅＡｌｌツールでの最適化コードの生成に適したスライスと順序を整えられた要件を出力として与えることができる。その上、それは定数伝播などの他の要件最適化を実行することができる。図２６で示されるように、この原型の基本的な構成要素は以下の通りである：
・語彙及び構文の分析器：この部分は入力としてＬｙｅｅ要件として取って、出力として一般的に中間的表現と呼ばれる構文の木を与える。要件のこの新しい表現方法は我々が行おうと望んでいるすべての静的な分析技術の出発点である。その上、Ｌｙｅｅ要件を分析するとき、語彙、または、構文上の誤りを検出しユーザに伝えることが可能である。
・フローベースの分析器：フローベースの分析要素は、前の部分で行われた中間的表現から始めて、１要件ポイントから別の１ポイントまで至るデータフロー制御の循環に関係あるすべての情報を生み出す。これらの分析の結果は制御フロー図（Ｃｏｎｔｒｏｌ  Ｆｌｏｗ  Ｇｒａｐｈ：ＣＦＧ）及びデータ・フロー図（Ｄａｔａ−Ｆｌｏｗ  Ｇｒａｐｈ：ＤＦＧ）から成る。
・最適化：他のものの中では、この要素は定数伝播技術を実行し、ＬｙｅｅＡｌｌツールが、より速く実行でき消費するメモリがより少ないプログラムを生成するのに適する、規則正しくて簡易化された宣言の系列を生産する。
・スライサ：この要素は入力として、フローベース分析要素及びスライシング評価基準によって生み出されるフローに関する（各単語に関連づけられるＤｅｆ／Ｕｓｅなどの）情報を受け取り、これらの与えられた評価基準に対応するスライスを出力として与える。
９．結論と将来への展望
我々は本稿でＬｙｅｅ要件に対して静的分析技術を用いることとその場合の衝撃的影響について報告した。まず最初に、我々は定数伝播やパターン検出などの古典的な最適化のテクニックがＬｙｅｅプログラムの実行時間をいかに改良することができるかを提示した。また、我々は、どのように要件における誤り（死んでいる定義、周期的な定義、不完全もしくは余計な定義）を発見するかを示した。２番目に、我々はスライシングというテクニックがＬｙｅｅシステムの理解と維持をいかに改良することができるかについて議論した。その上で、我々は、このスライシング技術を用いることで、平行実行可能なＬｙｅｅシステム中の独立部分をどうやって見つけるかを示した。３番目に、我々はタイピング誤りを発見しと中間介在物及び出力単語のタイプを自動的に生成することを可能とするタイプシステムを提案した。４番目に、我々はＬｙｅｅ方法論がどうセキュリティ側面などの何らかの拡大に適しているかを例証した。提示された静的分析技術の中には現在、Ｌｙｅｅ要件分析器と呼ばれる原型で実行されているものもある。
そして今後の作業として我々はまず、Ｌｙｅｅ要件分析ツールを完成させ、Ｌｙｅｅ方法論のある他の側面を改良するための他の静的及び動的な分析技術を調査したい。
１０．
以上詳細に説明したように、本実施形態に係る本発明の静的分析方法によれば、Ｌｙｅｅ要件に対して静的分析手法を用いるので、Ｌｙｙｅ要件とＬｙｅｅによって生成されるコード列の双方の品質を改善することができ、もって、Ｌｙｅｅ方法論におけるより良い品質（より少ないメモリと実行時間の消費）を有するコード生成が可能となる。
（７）発展形態として、上述した静的分析方法もしくは静的分析器をＬｙｅｅ要件（要求定義）に対して用いることで、より改善されたＬｙｅｅ要件を得、これを上述の「Ｌｙｅｅ発明の概要」で説明した方法により、或いは、特許文献１、２、４乃至６に記載されるＬｙｅｅによるソフトウェア生成方法により、更には、特許文献３記載のソフトウェア生成装置に入力することで、より少ないメモリ空間や処理時間でＬｙｅｅによって所望のソフトウェアを生成する方法或いは生成する生成装置を実現することができる。
即ち、Ｌｙｅｅによるソフトウェア生成の上流段階であるＬｙｅｅ要件（要求定義）段階で効率化を実現すれば、それ以降の処理を既存のＬｙｅｅ方法論を適用することで、一層の高品質の最終製品たるソフトウェアを得ることができる。
こうしたＬｙｅｅ要件（要求定義）を得た後の段階の方法或いは装置の詳細な説明については、上述の「Ｌｙｅｅ発明の概要」で説明した内容、或いは、特許文献１乃至６に記載される方法によるものとし、ここでは割愛する。
また本発明によれば、古典的な静的分析のテクニックを用いることでＬｙｅｅ方法論を一層増進させることが可能となる。
さらに本発明に係るＬｙｅｅ指向ソフトウェアに関する静的分析器によれば、Ｌｙｅｅ要件をうけ取り、ＬｙｅｅＡｌｌツールでの最適化コードの生成に適したスライスと順序を整えられた要件を出力として与えることができる。その上、それは定数伝播などの他の要件最適化を実行することができる。
本発明の多くの特徴および利点は明細書の詳細な説明から明白である。更に、当該技術分野における通常の知識を有する者にとって修正および改変が容易に数多くなし得るので、図示および記述されたものと寸分違わぬ構成および動作に本発明を限定することは望ましくないことであり、従って、あらゆる適切な改変体および等価体は本発明の範囲に含まれるものと見なされうる。前述の本発明に係る実施形態の説明および例示によって詳細に記述されたが、添付の特許請求の範囲のみならず本発明に係る開示事項全体に定義された本発明の範囲から逸脱することなしに、修正、置換、および、変更が数多く可能である。
また、本願に係る発明は、その適用において、上記の記述において説明されるか、或いは、図面に示された要素の詳細な解釈及び組み合わせに限定されるものではない。本発明は、他の実施形態が可能であり、種々の方法で実用および実施可能である。また、ここで用いられた語法および用語は記述を目的とするものであり、限定的に働くものとみなされてはならない。
従って、当該技術分野における通常の知識を有する者は、本開示の基調となる概念は、本発明の幾つかの目的を実施するための他の構造、方法、及び、システムを設計するための基礎として容易に利用され得ることを理解するはずである。従って、本発明の趣旨および範囲から逸脱しない限り、本願の特許請求の範囲にはそのような等価な解釈が含まれるものと見なされるものである。
また、上記ではＬｙｅｅ方法論におけるソフトウェアの静的分析法及び静的分析器について主として説明したが、本発明に係る技術思想は、例えばコンピュータソフトウェアの自動開発装置、自動開発プログラム、自動開発プログラムを記録した記録媒体、伝送媒体、紙媒体としても、また、自動開発プログラムを登載したコンピュータ・装置、自動開発プログラムを実行するクライアント・サーバ形式等といったカテゴリーにおいても実現、利用可能であることはいうまでもない。
さらに本発明は、単一プロセッサ、単一ハードディスクドライブ、及び、単一ローカルメモリを備えたコンピュータシステムに限らず、当該システムのオプションとして、任意の複数または組み合わせプロセッサ又は記憶デバイスを装備するにも適している。コンピュータシステムは、精巧な計算器、掌タイプコンピュータ、ラップトップ／ノートブックコンピュータ、ミニコンピュータ、メインフレームコンピュータ、及び、スーパーコンピュータ、ならびに、これらの処理システムネットワーク組合わせを含む。本発明の原理に従って作動する任意の適切な処理システムによって代替されうるし、また、これらと組合せて用いることも可能である。
また、本発明に係る技術思想は、もとよりあらゆる種類のプログラミング言語に対応可能である。さらに本発明に係る技術思想は、あらゆる種類・機能のアプリケーションソフトウェアに対しても適用可能である。
またさらに本願発明は、その技術思想の同一及び等価に及ぶ範囲において様々な変形、追加、置換、拡大、縮小等を許容するものである。また、本願発明を用いて生産されるソフトウェアが、その２次的生産品に登載されて商品化された場合であっても、本願発明の価値は何ら減ずるものではない。
【産業上の利用可能性】  本発明では、Ｌｙｅｅ要件に対して静的分析手法を用いるので、Ｌｙｙｅ要件とＬｙｅｅによって生成されるコード列の双方の品質を改善することができ、もって、Ｌｙｅｅ方法論におけるより良い品質（より少ないメモリと実行時間の消費）を有するコード生成を可能にすることで、ソフトウェア生産の大幅な効率向上、生産性向上、品質向上等、ソフトウェア産業上に大きな効果をもたらす。
【図１】
2004081788.tif 000132
【図２】
2004081788.tif 000133
【図３】
2004081788.tif 000134
【図４】
2004081788.tif 000135
【図５】
2004081788.tif 000136
【図６】
2004081788.tif 000137
【図７】
2004081788.tif 000138
【図８】
2004081788.tif 000139
【図９】
2004081788.tif 000140
【図１０】
2004081788.tif 000141
【図１１】
2004081788.tif 000142
【図１２】
2004081788.tif 000143
【図１３】
2004081788.tif 000144
【図１４】
2004081788.tif 000145
【図１５】
2004081788.tif 000146
【図１６】
2004081788.tif 000147
【図１７】
2004081788.tif 000148
【図１８】
2004081788.tif 000149
【図１９】
2004081788.tif 000150
【図２０】
2004081788.tif 000151
【図２１】
2004081788.tif 000152
【図２２】
2004081788.tif 000153
【図２３】
2004081788.tif 000154
【図２４】
2004081788.tif 000155
【図２５】
2004081788.tif 000156
【図２６】
2004081788.tif 000157
【国際調査報告】
2004081788.tif 000158
2004081788.tif 000159
2004081788.tif 000160
2004081788.tif 000161
2004081788.tif 000162