(57)【要約】【課題】テストデータチェックやロジックチェックでは検出が困難なソフトウェアの不具合(バグ)を数学的見地から検証する方法を提供する。【解決手段】プログラムのソースコードを、変数宣言の領域、写像処理領域、写像力学系領域に分類して数学モデルに変換し、モデル表示画面５０１のオリジナル領域５０２、中間領域５０３、解析結果領域５０４に表示して、「プログラムコードの無限桁演算の論理関係の整合性のエラーが引き起こすプログラム動作のエラー」の検出、「プログラムコードの無限桁演算の論理関係の整合性は検証されているが、有限桁演算の論理関係の整合性のエラーが引き起こすプログラム動作のエラー」の検出、「エラーレベル１とエラーレベル２の論理関係の整合性は検証されており、局所的な決定的なルールには問題ないが、プログラムコード中のカオスの存在が引き起こすプログラム動作のエラー」の検出、を行う。【選択図】  図２６
2008197851.tif 000002
【特許請求の範囲】
【請求項１】
手続き型プログラミング言語のプログラムコードを写像および／または写像力学系に置き換える第１ステップと、
前記写像および／または写像力学系に数学的手法を適用することにより、前記プログラムコードの信頼性の検証を行う第２ステップと、
を含むことを特徴とするプログラム論理の検証方法。
【請求項２】
請求項１記載のプログラム論理の検証方法において、
前記プログラムコードを置き換えた写像を利用して、前記プログラムコードに含まれる分岐処理の検証を行うことを特徴とするプログラム論理の検証方法。
【請求項３】
請求項１記載のプログラム論理の検証方法において、
前記プログラムコードを置き換えた前記写像力学系を利用して無限ループ型処理の検証を行うことを特徴とするプログラム論理の検証方法。
【請求項４】
請求項１記載のプログラム論理の検証方法において、
前記第１ステップでは、
前記プログラムコードを、変数宣言領域、写像処理領域、写像力学系処理領域に区別するステップと、
前記変数宣言領域では変数宣言の変換を行うステップと、
前記写像処理領域では、条件分岐文および反復実行文を、連続微分可能写像を用いてモデル化するステップと、
前記写像力学系処理領域では、終了条件を含む入力と出力が定義される写像を再帰的に構成するステップと、
を含むことを特徴とするプログラム論理の検証方法。
【請求項５】
請求項１記載のプログラム論理の検証方法において、
前記第２ステップにおける前記信頼性の検証は、
前記プログラムコードの無限桁演算の論理関係の整合性のエラーが引き起こすプログラム動作のエラーである第１エラーレベルの検出と、
前記プログラムコードの無限桁演算の論理関係の整合性は検証されているが、有限桁演算の論理関係の整合性のエラーが引き起こすプログラム動作のエラーである第２エラーレベルの検出と、
前記第１エラーレベルおよび前記第２エラーレベルの論理関係の整合性は検証されており、局所的な決定的なルールには問題ないが、前記プログラムコード中のカオスの存在が引き起こすプログラム動作のエラーである第３エラーレベルの検出と、
によって行われることを特徴とするプログラム論理の検証方法。
【請求項６】
手続き型プログラミング言語のプログラムコードを写像および／または写像力学系に置き換える第１ステップと、
前記写像および／または写像力学系に数学的手法を適用することにより、前記プログラムコードの信頼性の検証を行う第２ステップと、
をコンピュータに実行させることを特徴とするプログラム論理の検証プログラム。
【請求項７】
請求項６記載の検証プログラムにおいて、
前記第１ステップでは、元のプログラムコードと、当該プログラムコードを変換して得られた前記写像および／または写像力学系を対比して可視化して表示する動作を前記コンピュータに実行させることを特徴とする検証プログラム。
【請求項８】
請求項６記載の検証プログラムにおいて、
前記第２ステップにおける前記信頼性の検証では、
前記プログラムコードの無限桁演算の論理関係の整合性のエラーが引き起こすプログラム動作のエラーである第１エラーレベルの検出と、
前記プログラムコードの無限桁演算の論理関係の整合性は検証されているが、有限桁演算の論理関係の整合性のエラーが引き起こすプログラム動作のエラーである第２エラーレベルの検出と、
前記第１エラーレベルおよび前記第２エラーレベルの論理関係の整合性は検証されており、局所的な決定的なルールには問題ないが、前記プログラムコード中のカオスの存在が引き起こすプログラム動作のエラーである第３エラーレベルの検出と、
を前記コンピュータに実行させることを特徴とする検証プログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、プログラム論理の検証技術に関し、たとえば、手続き型プログラミング言語のプログラムコードの検証等に適用して有効な技術に関する。
【背景技術】
【０００２】
近年、金融、医療、通信、交通、教育、防犯など社会のさまざまな分野でコンピュータが利用され、我々は利便性を享受している。
ところが、コンピュータソフトウェアの不具合が原因による銀行業務の停止や証券業務の停止、混乱、鉄道交通システムの混乱などが多発し、日本のみならず、世界中がこの脅威にさらされている。
【０００３】
ソフトウェア開発者や関係会社は設計段階でのロジックチェック体制の強化や、プログラムテストを入念に行うなど対策を行っているが、テストデータでのチェックでは、データ数に限界があり、すべての場合の動作保証はできない問題がある。たとえば、想定外のデータ入力やデータどうしの関係、複合条件により不具合となる場合が多い。
【０００４】
一般的なソフトウェアテストは、テストデータでのチェックであり、不具合を起こすパラメータそのものを与えること及びそのパラメータの存在を証明することができない。
また、手続き型言語のプログラムコードには、変数の定義、関数の定義、写像力学系の定義と、ｉｆ，ｓｗｉｔｃｈなどで与えられる関数部分の操作、ｗｈｉｌｅ文で与えられる写像力学系部分の操作が、混合して記述されており、関数部分の操作の論理的整合性、写像力学系部分の操作の論理的整合性を体系的に検証できなかった。そのため、コンピュータソフトウェアの不具合が原因による銀行業務の停止や証券業務の停止、混乱、鉄道交通システムの混乱を回避する決定打が存在しなかった。
【０００５】
以下、従来におけるコンピュータソフトウェアの検証技術について概観する。なお、本発明者らの未発表の論文に基づいて本明細書を作成するため、原論文の章立てを踏襲し、従来技術については、原論文の第１章の開示内容を記載し、後述の実施の形態には、原論文の第２章以降を記載している。
【０００６】
第１章  序論
図１は、非特許文献１に掲載された、手続き型プログラミング言語の一種のＭａｔｌａｂ（数値解析ソフトウェア）（登録商標）による標準的な二分法プログラムのソースコードである。このプログラムは実際にＭａｔｌａｂ上で使用することができる。しかしこのプログラムは本当に何の問題も無いのであろうか。
【０００７】
一般的にコンパイル時にエラーも無く一見何も問題が無いように見えても、実際に使用した時に意図しない挙動をしてしまうというのはソフトウェアの世界ではよくあることである。
【０００８】
このようなプログラムが本当に正しく作動するかどうか確かめる方法とこのようなプログラムが、複数のコンピュータ上で並列分散されても正しく作動するかどうか確かめる方法を確立することが、ソフトウェア開発では重要な技術的課題となっている。
【０００９】
以下に、本発明に関連する従来の研究について、非特許文献２，非特許文献３を参照してまとめる。
１．１プログラムの品質
プログラムの品質を分類する試みがいくつか存在する。例えば、Ｃ．Ａ．Ｒ．Ｈｏａｒｅ  は１７項目の品質のリストを提案している。１９７６年の第２回ソフトウェア工学国際会議において、Ｂ．Ｗ．Ｂｏｅｈｏｍが品質を３レベルに階層化して分類した表を発表している。その一番下のレベルでは正確さ・安全性・装置効率など１５の性質が列挙されている。
【００１０】
本明細書において、プログラムの品質の中でプログラムの信頼性に注目する。プログラムの信頼性とは、プログラムが仕様に定められた機能をいかに正しく実現しているか、ということである。機能の実現の仕方から誤りが無いかというだけでなく、仕様に定められた機能は漏れなく実現しているかという意味での完全性の要求も含まれる。さらに仕様が定められた入力条件を満たさないでデータが入力された場合にもプログラムが暴走するなどの異常事態を引き起こさないという頑健性も重要である。
【００１１】
このようなプログラムの品質を調べるには、そのプログラムが正しく作動するかを確かめなければならない。プログラムの品質を保証するにはプログラムに対するテストが重要な役割を担っている。
【００１２】
１．２プログラム検証論
プログラム検証論は１９６０年代から盛んに研究されているが、１９９５年にはかなり下火になっている。しかし構造化プログラミングや言語設計に影響を与えて、「プログラミングの正しさ」の証明方法の研究は、形をかえてソフトウェア工学に引き継きつがれている。
【００１３】
プログラム検証論は、「ホーア論理」をベースとしている。このホーア論理（Ｈｏａｒｅ  Ｌｏｇｉｃ）では、正しさの問題を、より小さなプログラムの正しさの問題に帰着させる。ホーアはプログラムの最初と最後に「表明」と呼ばれる条件を付加した形式を考案し、これをもとにプログラムを検証する「論理学的方法」を作った。「表明」は普通の数学の命題と同じ方法でその正しさを確認できる。ホーア論理の証明とは、「プログラムの正しさ」を「表明の正しさ」に還元する方法であり、最後まで証明の面倒をみるのではなく最後は数学などの証明力に責任転嫁してしまう。
【００１４】
１．２．１  ホーア論理の理論的限界
ホーア論理の理論的限界として、Ａｌｇｏ−ｌｉｋｅなプログラム言語に対しては（健全で）相対完全なホーア論理を作ることができないということが挙げられている。Ａｌｇｏ−ｌｉｋｅな、とは、１．手続き（＝関数）を定義することができ、局所手続き（＝ｇｏｔｏ文）も定義できる、２．手続きを手続きの引数として渡すことができる、３．再帰呼び出しができる、４．静的スコープルールを使える、５．大域変数を使える、といった特徴を備えることをいう。
【００１５】
またプログラム検証全般の現実的限界として、第１に、仕様記述と証明コストが膨大、第２に、証明にバグがないという保証がない、第３に、仕様にバグがないという保証がない、という問題点もあり１９８０年代には、「プログラム検証は不可能である」という意見が支配的になり、実現されたシステムが「仕様」を満たしているか？ということを確認する「検証」の手法としては実っていない。しかしシステムが「要求」に対して正しく作られているか？を確認する「有効性確認」にホーア理論が用いられるなど、「現実のプログラムの安全性を保証する」研究はソフトウェア工学として発展している。
【００１６】
１．３ソフトウェア工学におけるテスト技法
ソフトウェア工学などと言われる前からソフトウェアに対するテストは広く行われてきたが、１９６０年代末からのソフトウェア工学の大きなうねりはテストの考えにも様々な影響を与えた。
【００１７】
１．  テスト技術の研究
テストが工学的な分析の対象として意識的に研究され、その結果が実践され始めた。代表的な技術としては経路解析やテストデータ生成などが挙げられる。
【００１８】
２．  テストツールの作成・利用
ソフトウェア工学の浸透に伴い、ソフトウェア開発を助けるツールの作成・利用が一般化したが、テストの分野でもテストベッド・テストカバレージ計測などのツールが作られ、使用され始めた。
【００１９】
３．ライフサイクルでのテストの位置づけ
ソフトウェアのライフサイクルという概念が重視されるようになった。ライフサイクル・モデルではソフトウェアの誕生から死までをいくつかのフェーズに分ける。典型的な分割は要求定義・設計・プログラミング・テスト・運用保守というフェーズわけである。そこでテストは１つのフェーズという位置づけを与えられたとともに、先行する各フェーズとテストとの関係も明確化された。即ち要求仕様に対するテストとして受け入れテスト（あるいはシステムテスト）、設計に対するテストとして統合テスト、プログラムに対するテストとして単体テスト、というようにテストの対象となるべき基準が明らかになった。
【００２０】
４．正当性証明技法の研究
プログラムの正当性証明技法は、１９７０年代半ばから末にかけ、理論的な研究が進められるとともに、実験的なシステムもいくつか作られ、ソフトウェア工学の中で活気のあるテーマのひとつとなった。これらの研究はその後、大規模プログラムに適用できるような実用段階にまで育ってきてはいないが、種々の点で従来からのテスト技術にも影響を与えた。
【００２１】
５．  テスト効果の計測
ソフトウェア工学では開発や保守のコストに対して目が向けられたことも１つの大きな特徴となっているが、その結果テストにもコスト意識が持ち込まれてきている。例えばテストにかかるコストはプログラムの開発コストの５０％を占めるといった数字がよく挙げられる。テストの場合はテスト自身の効率を上げてコストを下げるという面と効果的なテストを行いバグを早期に発見して取り除くことにより、ライフサイクル全体を通してのコスト削減に寄与するという面との両面を考えなくてはならない。いずれにせよテストの効果を評価することが必要で、そのために故障率の測定などが工夫され、さらには信頼性モデルなどの分析手法も研究され始めた。
【００２２】
１．４アルゴリズムの数学モデル
またプログラムとは別の観点からソフトウェアの動作を把握しようとする取り組みもある。１９８９年にL.Blum,M.Shub,S.Smaleの三名によってコンピュータ上の演算における力学系理論的定式化が提唱された。これはアルゴリズムや演算処理を数学関数や写像としてモデル化したものである（非特許文献４，非特許文献５，非特許文献６，非特許文献７、参照）。
【００２３】
しかしながら、いずれの方法もプログラムの動きを完全に把握しているとは言い難い現状である。
【非特許文献１】A.Neumaier, Introduction to Numerical Analysis,Cambridge University Press,2001.
【非特許文献２】玉井哲雄,松田茂広,三嶋良武,ソフトウェアのテスト技法,共立出版,1988.
【非特許文献３】林晋,プログラム検証論,共立出版、1995年.
【非特許文献４】L.Blum,M.Shub and S.Smale,On a Theory of Computation and Complexity over the Real Numbers:NP-Copleteness, Recursive Functions and Universal Machines,Bull.Amer.Math. Soc.(N.S.)Vol.21,no.1,pp.1-46(1989).
【非特許文献５】(ed.)F.Cucker,and (ed.)R.Wong,The Collected Papers of Stephen Smale,World Scienti?c Pub.Co.Inc.,2000.
【非特許文献６】L.Blum,Lectures on a Theory of Computation and Complexity over the Reals(or an Arbitrary Ring),1989 Lectures in Complex Systems, SFI Studies in the Scenics of ComplexityLect. Vol.II, Addison-Wesley,pp.1-46(1990).
【非特許文献７】S.Smale, Some Remarks on the Foundations of Numerical Analysis,SIAM Review Vol.52,no.2,pp.211-220(1989).
【発明の開示】
【発明が解決しようとする課題】
【００２４】
本発明の目的は、テストデータチェックやロジックチェックでは検出が困難なソフトウェアの不具合(バグ)を数学的見地から検証する方法を提供することにある。
【課題を解決するための手段】
【００２５】
本発明の第１の態様は、手続き型プログラミング言語のプログラムコードを写像および／または写像力学系に置き換える第１ステップと、
前記写像および／または写像力学系に数学的手法を適用することにより、前記プログラムコードの信頼性の検証を行う第２ステップと、
を含むプログラム論理の検証方法を提供する。
【００２６】
本発明の第２の態様は、第１の態様に記載のプログラム論理の検証方法において、
前記プログラムコードを置き換えた写像を利用して、前記プログラムコードに含まれる分岐処理の検証を行うプログラム論理の検証方法を提供する。
【００２７】
本発明の第３の態様は、第１の態様に記載のプログラム論理の検証方法において、
前記プログラムコードを置き換えた前記写像力学系を利用して無限ループ型処理の検証を行うプログラム論理の検証方法を提供する。
【００２８】
本発明の第４の態様は、第１の態様に記載のプログラム論理の検証方法において、
前記第１ステップでは、
前記プログラムコードを、変数宣言領域、写像処理領域、写像力学系処理領域に区別するステップと、
前記変数宣言領域では変数宣言の変換を行うステップと、
前記写像処理領域では、条件分岐文および反復実行文を、連続微分可能写像を用いてモデル化するステップと、
前記写像力学系処理領域では、終了条件を含む入力と出力が定義される写像を再帰的に構成するステップと、
を含むプログラム論理の検証方法を提供する。
【００２９】
本発明の第５の態様は、第１の態様に記載のプログラム論理の検証方法において、
前記第２ステップにおける前記信頼性の検証は、
前記プログラムコードの無限桁演算の論理関係の整合性のエラーが引き起こすプログラム動作のエラーである第１エラーレベルの検出と、
前記プログラムコードの無限桁演算の論理関係の整合性は検証されているが、有限桁演算の論理関係の整合性のエラーが引き起こすプログラム動作のエラーである第２エラーレベルの検出と、
前記第１エラーレベルおよび前記第２エラーレベルの論理関係の整合性は検証されており、局所的な決定的なルールには問題ないが、前記プログラムコード中のカオスの存在が引き起こすプログラム動作のエラーである第３エラーレベルの検出と、
によって行われるプログラム論理の検証方法を提供する。
【００３０】
本発明の第６の態様は、手続き型プログラミング言語のプログラムコードを写像および／または写像力学系に置き換える第１ステップと、
前記写像および／または写像力学系に数学的手法を適用することにより、前記プログラムコードの信頼性の検証を行う第２ステップと、
をコンピュータに実行させるプログラム論理の検証プログラムを提供する。
【００３１】
本発明の第７の態様は、第６の態様に記載の検証プログラムにおいて、
前記第１ステップでは、元のプログラムコードと、当該プログラムコードを変換して得られた前記写像および／または写像力学系を対比して可視化して表示する動作を前記コンピュータに実行させる検証プログラムを提供する。
【００３２】
本発明の第８の態様は、第６の態様に記載の検証プログラムにおいて、
前記第２ステップにおける前記信頼性の検証では、
前記プログラムコードの無限桁演算の論理関係の整合性のエラーが引き起こすプログラム動作のエラーである第１エラーレベルの検出と、
前記プログラムコードの無限桁演算の論理関係の整合性は検証されているが、有限桁演算の論理関係の整合性のエラーが引き起こすプログラム動作のエラーである第２エラーレベルの検出と、
前記第１エラーレベルおよび前記第２エラーレベルの論理関係の整合性は検証されており、局所的な決定的なルールには問題ないが、前記プログラムコード中のカオスの存在が引き起こすプログラム動作のエラーである第３エラーレベルの検出と、
を前記コンピュータに実行させる検証プログラムを提供する。
【００３３】
一般的にソフトウェアはプログラム言語を用いて作成されている。本発明者らは、そのプログラムを部分ロジックモジュールに分割し、その部分ロジックモジュールを数式に置き換える研究を行い、置き換え技術を確立した。
【００３４】
さらに、そこで生成された数式の関数特性を調べ、その特性により、その部分ロジックモジュールがどのような条件の時に暴走や発散、振動を起こすかどうかを判断する技術を確立した。
【００３５】
この手法を用いてプログラムのロジックモジュール単体とその結合特性を調べることにより、プログラムの安定動作範囲と不安定動作範囲を検証可能とする。
すなわち、従来のテストデータチェックやロジックチェックでは検出が困難なソフトウェアの不具合(バグ)、すなわち、有限桁の浮動小数点演算が引き起こす、論理の不整合性の検証とソフトウェアが不具合を起こすパラメータそのものを与え、そのパラメータが存在することを証明できる方法を確立した。
【発明の効果】
【００３６】
本発明によれば、テストデータチェックやロジックチェックでは検出が困難なソフトウェアの不具合(バグ)を数学的見地から検証する方法を提供することができる。
【発明を実施するための最良の形態】
【００３７】
以下、図面を参照しながら、本発明の実施の形態について詳細に説明する。
本実施の形態においては、プログラムの動作を検証するため、L.Blum,M.Shub,S.Smaleが提唱した力学系理論的定式化を導入し、プログラムの動作の力学系モデル化を行う（L.Blum,M.Shub and S.Smale,On a Theory of Computation and Complexity over the Real Numbers:NP-Copleteness, Recursive Functions and Universal Machines,Bull.Amer.Math. Soc.(N.S.)Vol.21,no.1,pp.1-46(1989).参照）。実施の形態の前半において、単一のコンピュータ上のプログラムの動作の力学系モデルを構築し、Ｍａｔｌａｂ等の数値解析ツール環境上で、その力学系モデルの近似シミュレーションを行いプログラムの動作の力学系モデルによる検証の有効性について説明する。
【００３８】
第２章  論理関数
この章では手続きプログラム言語中に現われるｉｆ文、ｓｗｉｔｃｈ文、ｗｈｉｌｅ文の分岐条件の論理演算の数学モデルを与えるのに必要な論理演算のためのＢｏｏｌｅａｎ関数を定義し、その性質をまとめる。
【００３９】
２．１  Ｂｏｏｌｅａｎ関数の定義
Ｚ：整数  Ｒ：実数
Ｂｏ：Ｂｏｏｌｅａｎ Ｂｏ＝｛０，１｝⊂Ｚ⊂Ｒ
０のとき、偽（Ｆａｌｓｅ），１のとき、真（Ｔｒｕｅ）となる。
全てのｅｘ∈Ｂｏに対して、Ｎｏｔ（ｅｘ）＝１−ｅｘ
任意のｅｘ，ｅｙに対して、ｅｘＡＮＤｅｙ＝ｅｘ・ｅｙ
任意のｅｘ，ｅｙ∈Ｂｏに対して、ｅｘＯＲｅｙ＝１−（１−ｅｘ）・（１−ｅｙ）
各論理演算の真理表を図２に示す。このＮｏｔ，ＡＮＤ，ＯＲの論理演算を複数組み合わせた一般的なＢｏｏｌｅａｎ関数を以下のように定義できる。なお、一般的なＢｏｏｌｅａｎ関数については、たとえば、木村正行、水野尚,しきい値論理とその応用,昭晃堂、1979年、等の文献に記載されている。
【００４０】
Ｂｏｎ：Ｂｏのｎ個の直積、ｅｖ＝（ｅ１，ｅ２，．．．，ｅｎ），ｅｋ∈Ｂｏ，ｋ＝１，．．．，ｎとおく。ｎ変数の論理関数ｆｌｏｇｉｃ：Ｂｏｎ→Ｂｏをｆｌｏｇｉｃ（ｅ１，ｅ２，．．．，ｅｎ）または、ｆｌｏｇｉｃ（ｅｖ）と記述する。
【００４１】
また、ｅ（バー）ｋ＝１−ｅｋとおく。さらに、ｅｉｖをＢｏｎの任意に与えられた点として、点ｅｉｖにおいてのみ１をとり、その他の点では、０をとるｎ変数の論理関数をｆｌｏｇｉｃ（ｉ）で表す。このとき、ｆｌｏｇｉｃ（ｉ）：＝ｅ＊１ｅ＊２．．．．ｅ＊ｎと与えられる。ここに、
【００４２】
【数１】
2008197851.tif 000003
このとき、ｆｌｏｇｉｃ（ｅ１，ｅ２，．．．，ｅｎ）は次のように展開できる。
【００４３】
【数２】
2008197851.tif 000004
上の展開は、任意の変数ｅｋ，ｋ＝１，．．．，ｎについても同様に成立する。この展開とｅｉｖ、ｆｌｏｇｉｃ（ｉ）を用いて、ｆｌｏｇｉｃ（ｅ１，ｅ２，．．．，ｅｎ）は一般的に次の形に表すことができる。
【００４４】
【数３】
2008197851.tif 000005
以上より、ｆｌｏｇｉｃ（ｅ１，ｅ２，．．．，ｅｎ）はｎ変数の多項式で記述されることがわかる。
【００４５】
２．２  条件分岐に用いる論理関数の Ｂｏｏｌｅａｎ関数表現
上のＢｏｏｌｅａｎ関数の定義をｉｆ，ｓｗｉｔｃｈ，ｗｈｉｌｅ文などの条件分岐に用いる代表的な論理関数に適用して、以下のようなＢｏｏｌｅａｎ関数として与える。
【００４６】
【数４】
2008197851.tif 000006
第３章  浮動小数点
この章では、コンピュータの演算で使用される浮動小数点についてまとめる。特に、一般的に用いられるＩＥＥＥ７５４フォーマットを中心に取り上げ、有限桁の浮動小数点演算における問題についても触れる。
【００４７】
３．１  ＩＥＥＥ７５４フォーマット
ＩＥＥＥは米国電気電子技術者協会（Ｔｈｅ Ｉｎｓｔｉｔｕｔｅ ｏｆ Ｅｌｅｃｔｒｉｃａｌ ａｎｄ Ｅｌｅｃｔｒｏｎｉｃｓ Ｅｎｇｉｎｅｅｒｓ）のことを指し、アメリカに本部があって世界中に会員がいる大きな学会である。コンピュータ関係の規格も作成しており、ＩＥＥＥが作成した規格が国際規格に採用されることも多い。７５４というのは、ＩＥＥＥの中のワーキンググループの番号で、規格の番号でもある。ＩＥＥＥ７５４は浮動小数点演算の規格である。昔は浮動小数点数のデータ形式はコンピュータによってバラバラであり、データをやりとりするときに変換処理が必要になり、とても不便であった。そのため、コンピュータの技術者が集まり共通のデータ形式と計算方法を決定した。その時作成されたのがＩＥＥＥ７５４規格である。一つの浮動小数点数を３２ビットまたは６４ビットで表現する。３２ビットを単精度（Ｓｉｎｇｌｅ Ｐｒｅｃｉｓｉｏｎ）と呼び、６４ビットを倍精度（Ｄｏｕｂｌｅ Ｐｒｅｃｉｓｉｏｎ）と呼ぶ。これらの拡張形式を実装するように推奨し、相互運用や演算規則などが規定されている。
【００４８】
ＩＥＥＥ７５４では、ビットの使い方として、符号（ｓｉｇｎ）／指数（ｅｘｐｏｎｅｎｔ）／仮数（ｍａｎｔｉｓｓａ）を次のように定義している。有為な数を仮数と呼び、残りのビットは指数部、符号ビットとする。３２ビット表現を単精度と呼び、符号ビットを１ビット、仮数部を２３ビット、指数部を８ビットとする。６４ビット表現を倍精度と呼び、符号ビットを１ビット、仮数部を５２ビット、指数部を１１ビットとする。２進数を使うため、ほとんどの１０進数の小数は正確に表現できない。
【００４９】
ＩＥＥＥ７５４のビット表現について説明する。
単精度のビットパターンによる表現
単精度のＩＥＥＥ７５４浮動小数点数は、符号ビット（１ビット）、指数部（８ビット）、仮数部（２３ビット）の３２ビットで表現される。
【００５０】
指数（ｅｘｐｏｎｅｎｔ）
指数部は２の０乗のときは、０１１１１１１１となる。
指数部の２進数表現
１０００   ００１１  ＋４乗
１０００   ００１０  ＋３乗
１０００   ０００１  ＋２乗
１０００   ００００  ＋１乗
０１１１   １１１１   ０乗
０１１１   １１１０  −１乗
０１１１   １１０１  −２乗
０１１１   １１００  −３乗
仮数（ｍａｎｔｉｓｓａ）
仮数部は２を基数として整数部が一桁になるように正規化した数の２進数表現になる。正規化によって仮数部の最上位ビットは常に１になるので、実際に用意しておく必要はなく、倍精度の５２ビットであれば、最上位の１をｈｉｄｄｅｎ ｂｉｔにして含めなければ、５３ビット分の情報が含まれることになる。
【００５１】
小数の２進数表現
０．１０００     １／２            ＝０．５
０．０１００     １／（２＊２）    ＝０．２５
０．００１０     １／（２＊２＊２）      ＝０．１２５
０．０００１     １／（２＊２＊２＊２＊）＝０．０６２５
符号（ｓｉｇｎ）
符号ビットは１ビットで、１は負の数、０は正の数を表す。代表的な１０進数表現の差異のビットパターンを、図３に示す。
【００５２】
３．２  有限桁の浮動小数点演算と論理演算の問題
Ｒ：実数の集合、Ｍｆ：ＩＥＥＥ７５４のフォーマットの単精度の浮動小数点の集合、Ｍｄ：ＩＥＥＥ７５４のフォーマットの倍精度の浮動小数点の集合とする。任意のａ，ｂ＞０，ａ，ｂ∈Ｒに対して、論理的に、ａ＋ｂ＞ａが成立する。しかしながら、任意のａ，ｂ＞０，ａ，ｂ∈Ｍｆ、またはａ，ｂ＞０，ａ，ｂ∈Ｍｄに対して、ａ＋ｂ＝ａとなるｂが存在する。ＩＥＥＥ７５４のフォーマットに限らず、有限桁の浮動小数点演算では同様なことが発生し、ある桁幅を超えた数どうしの四則演算は成立しない。これらの現象は桁落ち、情報落ちと呼ばれる。ｉｆ文などの分岐条件がこのような桁落ち、情報落ちの影響を受けた場合、プログラマの意図しない動作を引き起こす原因となる。この節では、Ｍｄの浮動小数点の演算を対象として、ａ，ｂ＞０，ａ，ｂ∈Ｍｄに対して、ａ＋ｂ＝ａとなるｂが存在する例をＭａｔｌａｂを用いて示す。その実行結果が図４である。
【００５３】
上記の（１＋２−５２＞１），（２＋２−５２＞２），（２＋２−５２＝＝２）はそれぞれ２章の代表的な論理関数であり、それぞれのａｎｓの値はＢｏ値を示している。したがって、その結果は、（１＋２−５２＞１）＝１，（２＋２−５２＞２）＝０，（２＋２−５２＝＝２）＝１となっており、１＋２−５２＞１は真であるが、２＋２−５２＞２は偽であり、２＋２−５２＝＝２が真となっており、２−５２がａ，ｂ＞０，ａ，ｂ２∈Ｍｄに対して、２＋ｂ＝２となるｂの解２−５２になることを示している。次に、このような結果が起きる理由をさらに詳しく調査する。
【００５４】
ｈｅｘ２ｂｉｎ（ｎｕｍ２ｓｔｒ（ｘ，“％ｂｘ”））の浮動小数点ｘをＩＥＥＥ７５４のビットパターン表現に変換するＭａｔｌａｂの関数（本実施の形態の説明の末尾に記載された（付記）に例示された関数プログラムを参照）を用いて以下に、１，１＋２−５２，２，２＋２−５２のＩＥＥＥ７５４のビットパターン表現をＭａｔｌａｂによって得た結果を、図５に示す。
【００５５】
１と１＋２−５２のＩＥＥＥ７５４のビットパターン表現は最後の１が異なり、加算が行われていることがわかる。しかし、２と（２＋２−５２）のＩＥＥＥ７５４のビットパターン表現は全く同一であり、加算が成立せず、情報落ちが発生していることがわかる。上の極めて簡単な例からでも、このような桁落ち、情報落ちの影響が、プログラマの意図しない動作を引き起こす原因となることが容易に理解できる。
【００５６】
第４章  プログラミング数学モデル
４．１  条件分岐に用いる論理関数の連続変形型の Ｂｏｏｌｅａｎ関数表現
上述の第２章のＢｏｏｌｅａｎＢｏを連続変形型のＢｏｏｌｅａｎ：Ｂｈ＝［０，１］に拡張して、ｉｆ，ｓｗｉｔｃｈ，ｗｈｉｌｅ文などの条件分岐に用いる代表的な論理関数を連続変形型の論理関数に拡張する。
【００５７】
今、連続変形型のＢｏｏｌｅａｎ：Ｂｈ＝［０，１］と連続変形型の論理関数を定義するため、ＢｏｏｌｅａｎＢｏ＝｛０，１｝の領域を：Ｂｈ＝［０，１］⊃Ｂｏに埋め込む。
【００５８】
このとき、区間［０，１］：＝｛ｘ∈Ｒ｜０≦ｘ≦１｝とおく。連続変形型の論理関数は、それぞれ、以下の式５、式６、式７ように定義する。
【００５９】
【数５】
2008197851.tif 000007
【００６０】
【数６】
2008197851.tif 000008
【００６１】
【数７】
2008197851.tif 000009
通常の論理関数を、連続変形型の論理関数と置き換えることにより、論理関数を微分可能な関数に変形可能である。さらに、連続変形型の論理関数の導関数を以下の式８、式９、式１０ように定義する。図６、図７、図８、図９にそれぞれの連続変形型の論理関数とその導関数の例を示す。
【００６２】
【数８】
2008197851.tif 000010
【００６３】
【数９】
2008197851.tif 000011
【００６４】
【数１０】
2008197851.tif 000012
４．２  連続変形型の Ｂｏｏｌｅａｎ関数表現の応用
３章において、有限桁の浮動小数点演算と論理演算の問題に触れたが、ここでは、連続変形型のＢｏｏｌｅａｎ関数表現を用いて、有限桁の浮動小数点演算において、論理演算が成立しない場合の浮動小数点を求める方法について述べる。２章では、一般的な論理関数ｆｌｏｇｉｃ（ｅ１，ｅ２，．．．，ｅｎ）はｎ変数の多項式で記述されることを示した。ｆｌｏｇｉｃ（ｅ１，ｅ２，．．．，ｅｎ）＝１，またはｆｌｏｇｉｃ（ｅ１，ｅ２，．．．，ｅｎ）＝０のどちらかであり、このどちらかが成立する（ｅ１，ｅ２，．．．，ｅｎ）の値を求めるには、これらのｎ変数の多項式の方程式の解を求めれば良い。ｉｆ文、ｓｗｉｔｃｈ文、ｗｈｉｌｅ文の分岐条件は、ｆｌｏｇｉｃ（ｅ１，ｅ２，．．．，ｅｎ）で与えられ、一般的に、ｅｋ，ｋ＝１，２，．．．，ｎは、例えばｅｋ（ｘ｛ｋ１，ｘ｛ｋ１，．．．，ｘ｛ｋｍ）＝（ｘｋ１＞ａｋ１）＋（ｘｋ２＞ａｋ２）＋．．．＋（ｘｋｍ＞ａｋｍ），ｘｋｊ，ａｋｊ２Ｍｄ，ｊ＝１，２，．．．，ｍのように、有限桁の浮動小数点を入力変数（ｘ｛ｋ１，ｘ｛ｋ１，．．．，ｘ｛ｋｍ）とするそれぞれのＢｏｏｌｅａｎ型論理関数の多項式で与えられる。
【００６５】
したがって、有限桁の浮動小数点を入力変数とするＢｏｏｌｅａｎ型論理関数の多項式の方程式の解を求める問題に帰着するが、このＢｏｏｌｅａｎ型論理関数の多項式の方程式は微分可能ではないので、ニュートン法などの通常の数値解析の方法を用いることができない。
【００６６】
そのため、前節で定義した連続変形型のＢｏｏｌｅａｎ関数表現を用いて、β＝１とした場合の微分可能な近似Ｂｏｏｌｅａｎ型論理関数の多項式の方程式の良い近似解（β≠０）を求め（このとき、連続変形型のＢｏｏｌｅａｎ関数の他のパラメータγ，δなどは、適切になるように決め、β＝１からだんだんβの値を小さくしながら、繰り返し近似解を求める。）、十分良い近似解が求まった後で、その解をβ＝０の場合のＢｏｏｌｅａｎ型論理関数の多項式に代入して、その方程式の解であるかを確認する手法を本実施の形態では提案する。
【００６７】
以下に、（１０５＋ｘ＞１０５）＝＝０となるｘ∈Ｍｄを求める例を示す。この場合、式（６）からｌｏｇｉｃｐ（１０５＋ｘ，β，１０５，γ，δ）＝＝０，β＝［０，１］の連続変形型のＢｏｏｌｅａｎ関数方程式を用いる。このとき、ｌｏｇｉｃｐ（１０５＋ｘ，β，１０５，γ，δ）の導関数（式（１１））は、式（９）によって与えられる。そして、次の式（１２）で関数を定義する。
【００６８】
【数１１】
2008197851.tif 000013
【００６９】
【数１２】
2008197851.tif 000014
あるβ≠０，かつ十分小さなｄｅｌｔａ０（＞０）∈Ｍｄに対して、｜ｇ（ｘ，β，１０５，γ，δ）｜＜ｄｅｌｔａ０が成立するｘが近似解となる。
【００７０】
以下の図１０に、（初期値ｘ０＝２−３８，β＝１，γ＝１＝２，δ＝２５０）のパラメータに対して、Ｍａｔｌａｂによって得た結果を示す。
上記のように、関数ｇ（・・・）は収束し、４回繰り返して得られた近似解ｘ＝３：６３４４２６０９３４１２９１３・・・１０−１２を（１０５＋ｘ＞１０５）に代入した結果は、（１０５＋ｘ＞１０５）＝０となり、ｘ＝３：６３４４２６０９３４１２９１３・・・１０−１２が（１０５＋ｘ＞１０５）＝０の解であることを数値的に証明できる。
４．３  変数の表記方法
１．変数の時間的発展
コンピュータに行わせる作業の「手順」の記述に重きを置いた言語（手続き型プログラム言語）では、各処理の時間的発展はソース記述順の上から下へと流れる。このプログラム上の変数ｘの時間的発展を、添え字ｎを導入して表すことにする。ただし、プログラム言語の仕様によっては、関数の中で変数を宣言することができるが、その場合、変数のスコープ（有効範囲）はその関数の中に限定される。変数の時間的発展は、各変数のスコープごとに固有であると考えられるため、先の添え字ｎを、スコープが識別できるように、ｎ−ｓｃｏｐｅと表す。
【００７１】
例えば変数ｘが関数ｆで宣言されており、その時点での時間的発展が３である場合。ｓｃｏｐｅを−ｘ−ｆなどと表記することにして、ｘ３−ｘ−ｆと表す。
３．操作回数
ある変数ｘに対して代入文が記述されているとき、実際のプログラム実行時にこの処理が行われるときには、その変数ｘに対して代入文で定義された操作が行なわれることになる。変ｘに対し、１つの代入文が定義されていれば、その変数の時間的発展は＋１されるとみなす。つまり、関数ｆで宣言されている変数ｘに対する１回の操作ｓは、ｘ（ｎ＋１）−ｘ−ｆ＝ｓ（ｘｎ−ｘ−ｆ）、と表す。
【００７２】
４．実引数を「どのように」仮引数に渡すか
関数を使用する際に、「関数に引き渡す変数」を実引数（ａｒｇｕｍｅｎｔ）といい、関数定義時に使用される変数を仮引数（ｐａｒａｍｅｔｅｒ）といい、区別する。
【００７３】
４．４実引数と仮引数（Ｃ言語の例）
図１１は、仮引数で呼び出されるＣ言語のプログラム例を示している。
関数を呼び出すとき、プログラム言語の仕様によっては、実引数が「左辺値」として評価し得る式であるときに、左辺値を渡す（ｃａｌｌ−ｂｙ−ｒｅｆｅｒｅｎｃｅ）のか、右辺値を渡す（ｃａｌｌ−ｂｙ−ｖａｌｕｅ）のかを任意に選択できる。
【００７４】
ここで、左辺値とは代入が許される（代入式の左辺になりうる）値のことであり、右辺値とは代入式の右辺になりうる、参照のみ許された値のことである。
次の図１２に例示されるプログラム例のように、実引数として左辺値が渡されるとき、関数内で仮引数に対して操作を行なうということは、呼び出し元で実引数となった変数に対して操作を行うことと等しい。
【００７５】
４．５ ｉｆ，ｅｌｓｅｉｆ，ｓｗｉｔｃｈ，ｆｏｒ，ｗｈｉｌｅ文の表記方法
ここでｉｆ，ｅｌｓｅｉｆ，ｓｗｉｔｃｈ文のような条件分岐やｆｏｒ，ｗｈｉｌｅ文などのループ（反復実行文）についてモデル化を提案する。
【００７６】
ｉｆ，ｅｌｓｅｉｆ，ｓｗｉｔｃｈ文の一般的な操作とループのブレーク条件を代表させるため、
Ｘ＝（ｘ１，ｘ２，・・・，ｘｎ）∈Ｒｎ，ｘｋ∈Ｒ
ｆｋ：Ｒｎ→Ｒを連続微分可能写像とし、Ｆ：Ｒｎ→ＲｎをＦ＝（ｆ１（Ｘ），ｆ２（Ｘ），．．．，ｆｎ（Ｘ））Ｔのような連続微分可能ベクトル写像とする。
【００７７】
また、ｉｆ，ｅｌｓｅｉｆ，ｓｗｉｔｃｈ，ｆｏｒ，ｗｈｉｌｅ文などの分岐条件、終了条件の変数をｅｋ∈Ｂ０とし、ｅｋがプログラム内の変数の関数の場合、ｅｋ＝ｅｋｆ（ｘ）とおく。
【００７８】
さらに、ｈ：Ｒｎ→Ｒをｈ（Ｘ）＝０，Ｘ∈Ｒｎの解が存在するある実関数とする。このとき、全微分ｄｆｋ（β，Ｘ），ｄＦ（β，Ｘ）＝ＤＦ（β，Ｘ）ｄＸ，＜ｄｈ（Ｘ），ｄＸ＞＝０が存在する。ここに、ＤＦ（β，Ｘ）はヤコビアンを、（・・・）Ｔはベクトルの転置を＜，＞は内積をそれぞれ表す。
【００７９】
以下において、ｆｋ（Ｘ）とｈ（ｘ）＝０はそれぞれ、ｉｆ，ｅｌｓｅｉｆ，ｓｗｉｔｃｈ文の操作とｗｈｉｌｅ文のループのブレーク条件を表すことにする。
また、ｉｆ，ｅｌｓｅｉｆ，ｓｗｉｔｃｈ文の条件分岐変数とｗｈｉｌｅ文のループのブレーク条件変：ｅｘ（β，Ｘ）を連続変形型のＢｏｏｌｅａｎ：Ｂｈ＝［０，１］関数とおき、β＝１の時、微分可能な関数に変形し、β＝０の時、Ｂｏ＝｛０，１｝の微分不可能な変形するβをパラメータとする連続変形関数とおく。したがって、ｄｅｘ（１，Ｘ）となる全微分が存在する。
【００８０】
図１３は、ｉｆ文を含むプログラム例であり、それに対応する写像の例が、次の式（１３）である。
【００８１】
【数１３】
2008197851.tif 000015
同様に、図１４は、ｅｌｓｅｉｆ文のプログラム例であり、それに対応する写像の例が、次の式（１３）である。
【００８２】
【数１４】
2008197851.tif 000016
同様に、図１５は、ｓｗｉｔｃｈ文のプログラム例であり、それに対応する写像の例が、次の式（１５）である。
【００８３】
【数１５】
2008197851.tif 000017
同様に、図１６は、ｆｏｒ文のプログラム例であり、それに対応する写像の例が、次の式（１６）である。
【００８４】
【数１６】
2008197851.tif 000018
同様に、図１７は、ｆｏｒ文のプログラム例であり、それに対応する写像の例が、次の式（１７）である。
【００８５】
【数１７】
2008197851.tif 000019
上記のように、ｉｆ文、ｅｌｓｅｉｆ文、ｓｗｉｔｃｈ文、ｆｏｒ文は、写像、合成写像によって、簡単にモデル化できる。一方、ｗｈｉｌｅ文は、初期値Ｘ０を持つ離散写像力学系Ｆｎ（Ｘ０）の軌道｛Ｘ０，Ｘ１，Ｘ２，．．．，｝を求め、ｈ（ｎ）＝ｈ（Ｘｎ）＝ｈ（Ｆｎ（Ｘ０））＝０＄を満たすｎを未知変数とする関数方程式としてモデル化されることに注目されたい。
【００８６】
このモデル化を用いて、プログラム中のｉｆ文、ｅｌｓｅｉｆ文、ｓｗｉｔｃｈ文、ｆｏｒ文の分岐条件が、プログラマの意図どおりになっているか、検証することができる。
本実施の形態の場合には、以下の３種類のエラーを検出することによって、プログラムコードの信頼性の検証を行う。
【００８７】
ａ）エラーレベル１「プログラムコードの無限桁演算の論理関係の整合性のエラーが引き起こすプログラム動作のエラー」の検出。
ｂ）エラーレベル２「プログラムコードの無限桁演算の論理関係の整合性は検証されているが、有限桁演算の論理関係の整合性のエラーが引き起こすプログラム動作のエラー」の検出。
【００８８】
ｃ）エラーレベル３「エラーレベル１とエラーレベル２の論理関係の整合性は検証されており、局所的な決定的なルールには問題ないが、プログラムコード中のカオスの存在が引き起こすプログラム動作のエラー」の検出。
【００８９】
各変数の増減の変化と極値の推定：上の全微分ｄｙｌ（Ｘ），ｄｙ（Ｘ）について、ｄｙｌ（Ｘ）＝０，ｄｙ（Ｘ）＝０となるＸが極値の条件であるので、これを解いて、極値を求め、極値を含みかつ｜ｄｙｌ（Ｘ）｜＜ε，｜ｄｙ（Ｘ）｜＜εとなる範囲をプログラムコードの動作試験用の入力パラメータ範囲とする（εの大きさはユーザーが決定する）。
【００９０】
全微分ｄＦｎ（Ｆｎ（Ｘ０））ｄＸについてはｄＦｎ（Ｆｎ（Ｘ０））ｄＸ＝（ｄｆ１（Ｘ），．．．，ｄｆｎ（Ｘ），）Ｔとなっているので、各成分ｄｆｋ（Ｘ），ｋ＝１，．．．，ｎについて、ｄｆｋ（Ｘ）＝０，ｋ＝１，．．．，ｎとなるＸが極値の条件であるので、これを解いて、極値を求め、極値を含みかつ｜ｄｆｋ（Ｘ）｜＜εとなる範囲をプログラムコードの動作試験用の入力パラメータ範囲とする（εの大きさはユーザーが決定する）。
【００９１】
エラーレベル１の検証：
ｉｆ文のｅｋ（β，Ｘ），ｋ＝１，．．．，ｌが全て相異なっているかチェックする。ひとつでも同じであれば、エラーレベル１の警告を出力する（エラーレベル１とは限らない）。
【００９２】
ｅｌｓｅｉｆ文の＝Σｌｋ＝１ｅｋ（β，Ｘ）＝１を満足するかチェックする。満足しなければ、エラーレベル１が発生する。
ｓｗｉｔｃｈ文のｌｏｇｉｃｄ（ｘ，β，ａｋ，σ）のａｋが全て相異なっているかチェックする。ひとつでも同じであれば、エラーレベル１の警告を出力する（エラーレベル１とは限らない）。
【００９３】
エラーレベル２の検証：
Ｓｔｅｐ１：ｙｌ（Ｘ），ｙ（Ｘ），Ｆｎ（Ｘ０）を有限桁の浮動小数点演算（Ｍａｔｌａｂ，ＪＡＶＡ（登録商標），Ｃ＋＋（登録商標）など）と有理数演算（Ｍａｐｌｅ（登録商標），Ｍａｔｈｅｍａｔｉｃａ（登録商標））で求めて比較する。異なっていれば、エラーレベル２が発生している。
【００９４】
Ｓｔｅｐ２：（無限桁の論理演算と有限桁の論理演算関係が一致しない有限桁の数値の探索）β＝１：対象とする写像の無限桁の論理演算の関係が不整合となる有限桁浮動小数点の数値の近似解を求めて、β＝１からβ＝０にだんだん近づけて、無限桁の論理演算が不整合となる有限桁浮動小数点の数値を確定する。
【００９５】
エラーレベル３の検証：
ｗｈｉｌｅ文の写像Ｆｎ（β，Ｘ０）の１変数をフラクタル次元解析にかけて、カオス性、フラクタル性の検証を行うフラクタル次元が非整数となった場合、エラーレベル３が発生している。
【００９６】
第５章  Ｍａｔｌａｂソースコードの力学系モデル
ここでは、前章の数学モデルを用いて、上述の図１の二分法のプログラムを書き換えることにする。ただし、Ｍａｔｌａｂ上でこの書き換えの近似シミュレーションが行えるように、Ｍａｔｌａｂが処理できない写像、関数フォーマットは、Ｍａｔｌａｂの文法のままとする。
【００９７】
図１８は、書き換えた結果の写像処理領域を示している。この場合、図１の行番号１、２、３、４、６、７の行の変換結果が、図１８の行番号４、５、６、８、２０、２１に対応している。また、図１の行番号８−１４の行の変換結果が、図１８の行番号２２に対応している。
【００９８】
図１９は、書き換えた結果の写像力学系処理領域を示している。この場合、図１８の写像領域に配置される関数ｂｗｄｓ（）のコード等が置かれている。
上記において、元のＭａｔｌａｂの二分法プログラムのｗｈｉｌｅループ内を離散力学系を含む写像ｂｗｄｓ（ａ，ｂ，ｉ，ｄｅｌｔａ０）として取り出し、ｗｈｉｌｅループがない、写像（または関数）処理領域と離散写像力学系を含む写像力学系処理領域に分けて記述し、写像処理領域ＦＲ１で写像力学系処理領域ＳＲ１のｗｈｉｌｅのｂｗｄｓ（ａ，ｂ，ｉ，ｄｅｌｔａ０）を呼び出して使用する。ｉｆ文やｗｈｉｌｅ文の分岐条件のＢｏｏｌｅａｎ変数は、更新番号をつけないこととする。そして、プログラムの実行が開始されてから、終了するまでの写像処理領域と写像力学系処理領域のプログラムの各変数の更新回数は、その変数名の配列の個数で与えられ、要素番号が、更新回数を表し、そのときの要素番号の配列の内容がそのときの変数の状態を与えるようになっている。ただし、Ｍａｔｌａｂの配列は、Ｃ言語やＪＡＶＡ言語と異なり、１番からしか定義できないため、数学的モデル化の定義と１番づつずれている。
【００９９】
６ Ｍａｔｌａｂコードの力学系モデルの近似シミュレーション
以下において、上述の図１８、図１９のＭａｔｌａｂコードの力学系モデルを用いて、ａ（１）＝２：５，ｂ（１）＝１．１、ｄｅｌａｔａ０＝１０−２，として、ｆ（ｘ）＝ｘ２−２＝０の解を求めるときのプログラムの各変数の動きを近似シミュレーションで求める。
【０１００】
本実施の形態の末尾に、そのシミュレーション結果（［シミュレーション開始］〜［シミュレーション終了］のでのリスト）と、実行に用いられたMatlabのプログラムのリストを示す。
【０１０１】
すなわち、後述の（付記）に示したシミュレーション結果は、シミュレーション実行時における画面へのテキスト出力のリストである。
以下のＭａｔｌａｂ上のシミュレーション結果において、プログラムの実行が開始されてから、終了するまでの写像処理領域と写像力学系処理領域のプログラムの各変数の更新回数は、その変数名の配列の個数で与えられ、要素番号が、更新回数を表し、そのときの要素番号の配列の内容がそのときの変数の状態を与えている。したがって、このＭａｔｌａｂコードの力学系モデルの有効性を確認できた。
【０１０２】
以下、図面を参照して、上述の原理を用いた本実施の形態のプログラム論理の検証方法を実施するプログラム論理の検証プログラム（検証ツール）の一例についてより具体的に説明する。
【０１０３】
図２０は、本実施の形態のプログラム論理の検証方法、プログラム論理の検証プログラムが実施される情報処理システムの構成例を紙面ブロック図である。
図２１、図２２、図２３、図２４は、本実施の形態の検証ツールの作用の一例を示すフローチャートである。
【０１０４】
図２０に例示されるように、本実施の形態の情報処理システム２００は、一例として、マイクロプロセッサ（ＭＰＵ）２０１、主記憶２０２、外部記憶装置２０３、ディスプレイ２０４、キーボード２０５、ネットワークインタフェース２０６を含むコンピュータからなる。
【０１０５】
ＭＰＵ２０１は、主記憶２０２に格納されたソフトウェアを実行することで、情報処理システム２００の全体を制御する。
主記憶２０２は、ＭＰＵ２０１が実行するソフトウェアやデータが格納される。本実施の形態の場合、主記憶２０２には、たとえば、基本ソフトウェアであるオペレーティングシステム３０１、このオペレーティングシステム３０１の制御の下で稼働する検証ツール３０２、言語処理系３０３が実装されている。
【０１０６】
オペレーティングシステム３０１は、ＭＰＵ２０１によって実行されることで情報処理システム２００の全体を制御する。
言語処理系３０３は、情報処理システム２００において、所望のプログラム言語によるソフトウェアの開発環境を提供するものであり、ソースコードの編集を行うソースエディタ、さらにはコンパイラ、インタプリタ、等のソフトウェアツール群で構成されている。
【０１０７】
検証ツール３０２は、上述のような数学的な手法によって、言語処理系３０３におけるソフトウェアの開発過程において、プログラムのソースコードの検証を行う機能を提供する。
【０１０８】
外部記憶装置２０３には、言語処理系３０３で開発されるソースコード４０１、検証ツール３０２が出力する情報が格納される判定結果ファイル４０２およびログファイル４０３が格納される。
【０１０９】
ディスプレイ２０４は、情報処理システム２００のユーザに情報を可視化して表示する。
キーボード２０５は、ユーザが情報処理システム２００に情報を入力するために用いられる。
【０１１０】
ネットワークインタフェース２０６は、情報処理システム２００を外部のシステムと図示しない情報ネットワークを介して接続する機能を有する。したがって、外部記憶装置２０３に格納された情報は、情報ネットワークを介して外部の情報処理装置のものを用いることもできる。
【０１１１】
あるいは、ネットワークインタフェース２０６を介した外部から情報処理システム２００への遠隔アクセスにより、検証ツール３０２や言語処理系３０３の機能を外部から遠隔操作で利用することもできる。
【０１１２】
次に図２１〜図２４のフローチャートを参照して、本実施の形態の検証ツール３０２の機能を説明する。
まず、本実施の形態の検証ツール３０２では、以下のように定義される情報が用いられる。
変数宣言：コード内の変数宣言を行う。（例：  ｄｏｕｂｌｅ  ｘ；  ，  ｉｎｔ  ｉ；など）
写像処理：ｗｈｉｌｅ文、ｄｏ〜  ｗｈｉｌｅ文、回数指定のないｆｏｒ文を使用しない。Ｉｆ文、ｅｌｓｅｉｆ文、ｓｗｉｔｃｈ文、回数指定のあるｆｏｒ文を含む処理である。
写像力学系処理：ｗｈｉｌｅ文、ｄｏ〜  ｗｈｉｌｅ文、回数指定のないｆｏｒ文に囲まれた処理である。この中に、Ｉｆ文、ｅｌｓｅｉｆ文、ｓｗｉｔｃｈ文、回数指定のあるｆｏｒ文を含む処理も含む。
【０１１３】
検証ツール３０２は、ソースコード４０１を入力し（ステップ１０１）、ソースコード４０１を複数の領域に分類し（ステップ１０２）、各領域毎に数学モデルへの変換処理を実行し（ステップ１０３）、導関数の応用による推定処理を実行して（ステップ１０４）、後述の判定処理のための支援データを出力する。
【０１１４】
上述のステップ１０２では、ソースコード４０１を、変数宣言の領域１−１、写像処理領域１−２、写像力学系領域１−３に分類する。このとき、写像力学系領域１−３を、再帰的に、変数宣言の領域１−１、写像処理領域１−２、写像力学系領域１−３に分類し、変数宣言の領域１−１と写像処理領域１−２の領域だけになるまで繰り返し分類する。
【０１１５】
上述のステップ１０３は、以下のステップ２−１、ステップ２−２、ステップ２−３を含んでいる。
ステップ２−１：変数宣言の領域１−１は、変数宣言の変換を用いて数学定義に置き換える。
【０１１６】
ステップ２−２：写像処理領域１−２は、ｉｆ文、ｅｌｓｅｉｆ文、ｓｗｉｔｃｈ文、回数指定のあるｆｏｒ文のそれぞれの変換を用いて数学モデルに置き換える。そして、写像処理領域１−２に含まれる写像力学系領域１−３を写像処理領域１−２の領域で呼び出して使用する入力と出力が定義される。また、写像力学系領域１−３で定義される写像または関数に置き換える。
【０１１７】
ステップ２−３：写像力学系領域１−３は、ｗｈｉｌｅ文、ｄｏ〜ｗｈｉｌｅ文、回数指定のないｆｏｒ文の変換を用いて数学モデルに置き換える。そして、ｗｈｉｌｅ文、ｄｏ〜ｗｈｉｌｅ文、回数指定のないｆｏｒ文の終了条件変数を含む入力と出力が定義される写像または関数を定義する。さらに、写像力学系領域１−３に含まれる変数宣言の領域１−１と写像処理領域１−２は、それぞれ、上述のステップ２−１とステップ２−２の処理を行う。
【０１１８】
上述のステップ１０４では、上述の式（１３）〜式（１７）の数学モデルの導関数において、β＝１として、プログラムコード（ソースコード４０１）への入力パラメータの増減の変化に対する、プログラムコードの各変数の増減の変化と極値の推定を行う。
【０１１９】
上述のステップ１０５では、ステップ１０４の推定結果に基づいて、プログラムコードの動作試験用の入力パラメータ範囲（式（１３）〜式（１７）の数学モデルのパラメータ）の決定の支援データ（後述の図３０に例示される解析する識別子、時間的発展、数式、位置情報、等）をログファイル４０３等に出力する。
【０１２０】
こうして得られた支援データに基づいて、以下のようにして、上述のエラーレベル１〜３の各エラーレベルの検証処理が行われる。
すなわち、エラーレベル１の検証は、図２２に例示されるフローチャートの処理にて行われる。
【０１２１】
まず、ログファイル４０３に上述のようにして格納されている支援データから、動作試験用のパラメータ範囲を読み込む（ステップ１１１）。
次に、β＝０に設定し、プログラムコードのｉｆ文、ｅｌｓｅｉｆ文、ｓｗｉｔｃｈ文、回数指定のあるｆｏｒ文の条件分岐変数関数とｗｈｉｌｅ文、ｄｏ〜ｗｈｉｌｅ文、回数指定のないｆｏｒ文の停止条件変数関数の無限桁の論理演算の整合性の検証を行う（ステップ１１２）。
【０１２２】
そして、無限桁の論理演算の整合性はOKか判別し（ステップ１１３）、不整合と判定された場合には、エラーレベル１の発生とみなして、プログラムコードの内の不整合のある条件分岐変数関数と停止条件変数関数とその分岐変数関数を含む元のソースコードの行番号とその行のコードを判定結果ファイル４０２に出力する（ステップ１１４）。また、ステップ１１３で整合性がＯＫと判定された場合には、エラーレベル１のクリアを判定結果ファイル４０２に出力する（ステップ１１５）。
【０１２３】
また、エラーレベル２の検証は、図２３に例示されるフローチャートの処理にて行われる。
まず、ログファイル４０３に上述のようにして格納されている支援データから、動作試験用のパラメータ範囲を読み込む（ステップ１２１）。
【０１２４】
次に、β＝０に設定し、プログラムコードの各変数、特にプログラムコードのｉｆ文、ｅｌｓｅｉｆ文、ｓｗｉｔｃｈ文、回数指定のあるｆｏｒ文の条件分岐変数とｗｈｉｌｅ文、ｄｏ〜ｗｈｉｌｅ文、回数指定のないｆｏｒ文の停止条件変数関数の無限桁の論理演算の関係と有限桁の浮動小数点演算を含む論理演算の関係との比較検証を行う（ステップ１２２）。
【０１２５】
そして、無限桁の論理演算と有限桁の論理演算の関係は一致するか判別し（ステップ１２３）、一致する場合には、エラー無しとしてエラーレベル２のクリアを判定結果ファイル４０２に出力して終了する（ステップ１２４）。
【０１２６】
ステップ１２３で不一致と判定された場合には、さらに、無限桁の論理演算と有限桁の論理演算関係が一致しない有限桁の数値の探索を行うか否かを判別し（ステップ１２５）、行わない場合には、プログラムコードの内の不整合のある条件分岐変数関数と停止条件変数関数とその分岐変数関数を含む元のソースコードの行番号とその行のコードを判定結果ファイル４０２に出力して（ステップ１２６）、終了する。
【０１２７】
ステップ１２５で探索を行うと判定され場合には、さらに、プログラムコードの動作試験用の入力パラメータ範囲を入力するとともに、対象とする、無限桁と有限桁論理演算が不整合となる論理関係を設定する（ステップ１２７）。
【０１２８】
そして、β＝１に設定し、対象とする無限桁の論理演算の関係が不整合となる有限桁浮動小数点の数値の近似解を求めて、β＝１からβ＝０にだんだん近づけて、無限桁の論理演算が不整合となる有限桁浮動小数点の数値を確定する（ステップ１２８）。
【０１２９】
そして、エラーレベル２が発生する無限桁の論理演算が不整合となる有限桁浮動小数点の数値を判定結果ファイル４０２に出力して（ステップ１２９）、終了する。
また、エラーレベル３の検証は、図２４に例示されるフローチャートの処理にて行われる。
【０１３０】
まず、ログファイル４０３に上述のようにして格納されている支援データから、動作試験用のパラメータ範囲を読み込む（ステップ１３１）。
次に、写像力学系処理内の最も更新番号が多くなる1変数をフラクタル次元解析にかけて、カオス性、フラクタル性の検証を行う（ステップ１３２）。
【０１３１】
そして、フラクタル次元は整数か否かを判別し（ステップ１３３）、整数でない場合には、エラーレベル３の発生とみなして、プログラムコードの内の写像力学系処理内でフラクタル次元が非整数となる元のソースコードの行番号とその行のコードを判定結果ファイル４０２に出力して（ステップ１３５）、終了する。
【０１３２】
ステップ１３３で整数と判定された場合には、エラーレベル３のクリアを判定結果ファイル４０２に出力して（ステップ１３４）、終了する。
以下、本実施の形態の検証ツール３０２の実際の運用の流れを説明する。
【０１３３】
まず、ユーザは、コンパイル可能なプログラムソース（テキストファイル）を入力する。
情報処理システム２００の検証ツール３０２は、プログラムソースを可数学モデル化プログラムソースに変換する。
【０１３４】
なお、可数学モデル化プログラムソースとは、以下のような特徴をもつ。
a) if文などの条件式の「条件判定式」が、
<固有の識別子>=<条件式>;
の形でif文の前に定義されており、条件判定はこの識別子の値で行われる。
【０１３５】
b)繰り返し回数が不定な繰り返し文（繰り返しの条件判定が常に真。または、繰り返し制御中に、繰り返し条件判定とは別の条件により繰り返しの制御を脱出する文）は、関数として定義されている。
【０１３６】
c)プログラムソースは、上述のように以下の領域に分類されている。
i）変数宣言の領域
ii）写像処理領域
iii）写像力学系領域
これらの特徴を備えた可数学モデル化プログラムソースは、通常のプログラム文法で作成可能である。
【０１３７】
ユーザは、予め可数学モデル化プログラムソースとして、プログラムをコーディングすることも可能である。
予め可数学モデル化プログラムソースとして、プログラムをコーディングしている場合は、この変換ステップは不要である。
【０１３８】
検証ツール３０２は、可数学モデル化プログラムソースに対応する数学モデルを、以下のような手順で算出する。
a)可数学モデル化プログラムソースを全精査し、定義文を抽出する。
【０１３９】
b)以下の情報を定義文ごとに、自動的に算出する。
定義義文とは、単純な形では、代入文として現れる。ここでいう定義文とは、if文などの条件文や、while文などの繰り返し文などの制御を考慮した「代入文」のことである。
【０１４０】
図２５Ａ、図２５Ｂ、図２５Ｃは、本実施の形態の検証ツール３０２にて用いられる定義文の一例を示す概念図である。
この図２５Ａ、図２５Ｂ、図２５Ｃに例示される定義文において、識別子は、プログラム中では、変数を識別するためにされる。
【０１４１】
また、定義文における時間的発展は、手続き型言語で記述された、同一識別子の変数に対して、定義文が記述されているとき、この変数は時間的発展をするとみなし、添え字をインクリメントする。この時間的発展は、数式の形で出力する。
【０１４２】
また、定義文における数式は、数式モデルとして出力される。
また、オリジナルの位置情報は、数式モデル変換前の識別子の位置情報（行、列）である。
【０１４３】
上述の可数学モデル化プログラムソースの変換処理において数学モデルが算出されていれば、ユーザは、オリジナルのプログラムソース、中間的な可数学モデル化プログラムソース、数学モデルの３つのテキストデータを並べて見ることができる。
【０１４４】
図２６は、ディスプレイ２０４に表示されるモデル表示画面５０１を示している。モデル表示画面５０１は、プログラムソースが表示されるオリジナル領域５０２、可数学モデル化プログラムソースが表示される中間領域５０３、数学モデルのリストが表示される解析結果領域５０４からなる。
【０１４５】
このうち重要なのは、オリジナルのプログラムソースと数学モデルであるので、可数学モデル化プログラムソースの中間領域５０３は、必ずしも表示する必要はない。
検証ツール３０２に対し、ユーザは以下のような操作が可能である。
【０１４６】
ａ）エラーレベル１「プログラムコードの無限桁演算の論理関係の整合性のエラーが引き起こすプログラム動作のエラー」の検出
例えば、ユーザは任意の条件文を選択し、排他条件になっているかを確認できる。
【０１４７】
ｉ）  ｉｆ  条件式１  ｅｌｓｅｉｆ条件式２  ｅｌｓｅｉｆ  条件式３  ・・・というプログラムがある場合、各条件式は排他な関係であることが好ましい。
ｉｉ）  ユーザは、数学モデルのリストのうち、検証したい条件式（の識別子）を選択する。
【０１４８】
ｉｉｉ）  システムはユーザが選択した条件式の論理和を求め、１以下となればＯＫ。１を超える場合ＮＧとし、エラーメッセージを出力する。
たとえば、図２７に例示されるＣ言語のプログラムはコンパイル可能だが、実行すると無限ループしてしまう。
【０１４９】
１０行目のｉｆ文の条件式ａ＞３  と１２行目のｉｆ文の条件式  ａ＝＝５の数学モデルを検証すれば、この条件が排他ではないことが分かる。
ｂ）エラーレベル２「プログラムコードの無限桁演算の論理関係の整合性は検証されているが、有限桁演算の論理関係の整合性のエラーが引き起こすプログラム動作のエラー」の検出
例えば、ユーザは任意の変数を選択し、無限桁演算の場合と有限桁演算の場合を比較することができる。
【０１５０】
ｉ）ユーザは、数学モデルのリストのうち、検証したい変数（の識別子）を選択する。
ｉｉ）ユーザは、有限桁演算の規格、例えばＩＥＥＥ７５４を選択する。
ｉｉｉ）システムは、ｉ）で選択した変数の数学モデルについて、無限桁演算の場合とｉｉ）で選択した有限桁演算の場合とをグラフ化し、重ね合わせて表示する。また、有限桁演算のグラフの変極点を算出して表示する。
【０１５１】
図２８に例示されるＣ言語のプログラムはコンパイル可能で、１０行目のｃの演算について、無限桁演算ならば問題がないが、有限桁演算を考えると、ｉｎｔには２１４７４８３６４７〜−２１４７４８３６４８までの値しか格納できないため、ａ＋ｂが２１４７４８３６４７または−２１４７４８３６４８に近づく場合、正しい計算結果にならない。
【０１５２】
１０行目のｃの演算を行う数学モデルを、無限桁演算の場合と有限桁演算の場合で比較することにより、ア）〜ウ）の利点がある。
ア）変極点から、通常のソフトウェアテストで重点的に検証する必要があるポイントを確認できる。
【０１５３】
イ）どういう入力のとき、無限桁計算と同じ結果にならないことがあるか確認できる。
ウ）中点を求める数学モデルを、ｃ＝（ａ＋ｂ）／２ではなく、ｃ＝ａ−（ｂ−ａ）／２、とする、などの発想の足がかりとなる。
【０１５４】
ｃ）エラーレベル３「エラーレベル１とエラーレベル２の論理関係の整合性は検証されており、局所的な決定的なルールには問題ないが、プログラムコード中のカオスの存在が引き起こすプログラム動作のエラー」の検出
上述のように、検証ツール３０２では、プログラムソースは以下の領域に分類されて処理される。
【０１５５】
ｉ）変数宣言の領域
ｉｉ）写像処理領域
ｉｉｉ）写像力学系領域
このうち、写像力学系領域において、カオスが発生する可能性がある。
【０１５６】
ユーザは、数学モデルのリストのうち、任意の写像力学系領域を表す関数（の識別子）を選択することができる。
検証ツール３０２は、選択された写像力学系領域について、カオスが発生する可能性があるか検証し、解析結果としてメッセージを出力する。
【０１５７】
以下に、図２９に例示されるＣ言語のプログラムを解析する場合の識別子、時間的発展、数式、位置情報等の支援データの出力の推移を、図３０の出力例に示す。
図３０のように出力される情報は、ログファイル４０３に記録され、モデル表示画面５０１のオリジナル領域５０２、中間領域５０３、解析結果領域５０４に表示されるとともに、必要に応じて、上述の図２２、図２３、図２４のフローチャートに例示したエラーレベル１、エラーレベル２、エラーレベル３の判定に用いられる。
【０１５８】
この図３０の出力結果の生成過程について例示すると、以下のようになる。
［変数の時間的発展について］
プログラムに登場する変数は、代入文によってその値を定義される。つまり、プログラムソースにおける「変数＝式」で表現される数式は、問題を解くべき数式ではなく、その変数を特徴づける定義式である。
【０１５９】
定義式が与えられるたび、刻々と変化していく変数をモデル化し、管理するために、上述のように各変数の識別子に添え字を導入している。
時間的発展の増加幅は、定義文が与えられるたびに＋１と定める。
【０１６０】
各変数の時間的発展は、各変数ごとに固有であることに注意する。
各変数の時間的発展は、スコープごとに定義し、宣言されただけで、まだ一度も定義が与えられていない場合の添え字を０とし、以降インクリメントしていく。
なお、添え字が０である変数の実際の値は、プログラミング言語に依存し、ｊａｖａでは変数型によって固有の値が与えられるが、Ｃ言語の場合は不定（メモリ状態に依存する）。不定な状態は、Ｎｏｒａｔｏｒ（ノレータ）と表記する。
【０１６１】
実際のプログラムにおいて、定義式が与えられるかは、制御構造に依存するケースがある。
分岐のない、直線形のプログラムの場合、図３１に例示されるように添え字が変化する。この場合の数学モデルは、単純に時間的発展は＋１されるので、たとえば、ａｎ＋１＝Ｘ；となる。
【０１６２】
分岐のあるプログラムの場合には、図３２に例示されるように添え字が変化する。この場合の数学モデルは、単純に時間的発展は＋１されないので、たとえば、ａｎ−１・ｅ＝Ｘ・ｅ＋ａｎ（１−ｅ）：、などとなり、実際のaの値だけではなく、時間的発展がされるかどうかも条件式eに依存する。
一般的には、
if(e1){
a=X;
}else if(e2){
a=X;
} else if(e3){
a=X;
:
などとあった場合、
ａｎ＋１・ｅ１＋１・ｅ２＋１・ｅ３＝Ｘ・ｅ１＋Ｘ・ｅ２＋Ｘ・ｅ３＋．．．
となる。
【０１６３】
［写像力学系領域］
写像力学系領域の場合には、図３３に例示されるように添え字が変化する。写像力学系領域Ｆは、独立した関数として扱う。
【０１６４】
Ｆの作用により、ａが定義されるということは、Ｆの戻り値によってａが定義されている場合が考えられる。この場合の数学モデルは、単純に時間的発展は＋１されると考えて、ａｎ＋１＝Ｆ；、となる。
【０１６５】
以上説明したように、本実施の形態のプログラム論理の検証方法、プログラム論理の検証プログラムによれば、従来のテストデータチェックやロジックチェックでは検出が困難なソフトウェアの不具合(バグ)を数学的見地から検証することが可能になる。
【０１６６】
すなわち、本実施の形態の検証ツール３０２を使って、プログラムソースを数学モデルに変換することにより、従来にない視点でソフトウェアの信頼性を検証することが可能となる。
【０１６７】
すなわち、従来、数学モデルを用いてアルゴリズムを考案したり、アルゴリズムの計算量を数学モデルを用いて算出することはあったが、本実施の形態のように、プログラムソース全体を数学モデルに変換する試みはなかった。
【０１６８】
コンピュータの歴史より、数学の歴史の方がはるかに長いため、問題解決のためのさまざまな環境が整っており、正しさを「証明」するには数学の世界の方が有利である。証明の概念自体が数学の概念なので、プログラムの正しさの証明が確実である。
【０１６９】
プログラムソースを変換して得た数学モデルと、プログラムの作成仕様書のもととなった数学モデルを比較することで、間違いに気が付いたり、新しい数学モデル、新しいアルゴリズムを考案するきっかけになりうる。
【０１７０】
つまり、従来のソフトウェアテストが仕様書を出発点にしていたのに対し、より高次の検証も可能となる。
この結果、すべてのコンピュータ上で利用されるソフトウェアの品質向上と動作保障を調査、検証する技術の提供を実現できる。
【０１７１】
ソフトウェアを利用するすべての産業が対象となり、世界規模の市場での広範な利用が見込める。さらに今まで開発されたソフトウェア資産とこれから開発される新規ソフトウェアすべてが適用範囲となり、本発明の市場価値は計り知れない。
【０１７２】
なお、本発明は、上述の実施の形態に例示した構成に限らず、その趣旨を逸脱しない範囲で種々変更可能であることは言うまでもない。
（付記）
以下は、上述の６ Ｍａｔｌａｂコードの力学系モデルの近似シミュレーションの実行結果、および、それに用いられたＭａｔｌａｂプログラムのソースコードである。
［シミュレーション開始］
>> testbmap
a_ = 2.500000000000000
b_ = 1.100000000000000
f_ = 4.250000000000000
f2_ = -0.790000000000000
e1 = 0
e2 = 1
n_x = 2
x_ = 0 2.500000000000000
n_a = 2
a_ = 2.500000000000000 1.100000000000000
n_b = 2
b_ = 1.100000000000000 2.500000000000000
e3 = 0
n2_x = 2
x_ =              0 1.800000000000000
n_i = 2
b_ = 2.500000000000000 1.800000000000000
a_ = 1.100000000000000
x_ =              0 1.800000000000000 1.450000000000000
n_i = 3
b_ = 2.500000000000000 1.800000000000000 1.450000000000000
a_ = 1.100000000000000
x_ =
Columns 1 through 3
0 1.800000000000000 1.450000000000000
Column 4
1.275000000000000
n_i =       4
b_ = 2.500000000000000 1.800000000000000 1.450000000000000
a_ = 1.100000000000000 1.275000000000000
x_ =
Columns 1 through 3
0 1.800000000000000 1.450000000000000
Columns 4 through 5
1.275000000000000 1.362500000000000
n_i =       5
b_ = 2.500000000000000 1.800000000000000 1.450000000000000
a_ = 1.100000000000000 1.275000000000000 1.362500000000000
x_ =
Columns 1 through 3
0 1.800000000000000 1.450000000000000
Columns 4 through 6
1.275000000000000 1.362500000000000 1.406250000000000
n_i = 6
b_ = 2.500000000000000 1.800000000000000 1.450000000000000
a_ =
Columns 1 through 3
1.100000000000000 1.275000000000000 1.362500000000000
Column 4
1.406250000000000
x_ =
Columns 1 through 3
0 1.800000000000000 1.450000000000000
Columns 4 through 6
1.275000000000000 1.362500000000000 1.406250000000000
Column 7
1.428125000000000
n_i = 7
b_ =
Columns 1 through 3
2.500000000000000 1.800000000000000 1.450000000000000
Column 4
1.428125000000000
a_ =
Columns 1 through 3
1.100000000000000 1.275000000000000 1.362500000000000
Column 4
1.406250000000000
x_ =
Columns 1 through 3
0 1.800000000000000 1.450000000000000
Columns 4 through 6
1.275000000000000 1.362500000000000 1.406250000000000
Columns 7 through 8
1.428125000000000 1.417187500000000
n_i =       8
b_ =
Columns 1 through 3
2.500000000000000 1.800000000000000 1.450000000000000
Columns 4 through 5
1.428125000000000 1.417187500000000
a_ =
Columns 1 through 3
1.100000000000000 1.275000000000000 1.362500000000000
Column 4
1.406250000000000
x_ =
Columns 1 through 3
0 1.800000000000000 1.450000000000000
Columns 4 through 6
1.275000000000000 1.362500000000000 1.406250000000000
Columns 7 through 9
1.428125000000000 1.417187500000000 1.411718750000000
n_i = 9
b_ =
Columns 1 through 3
2.500000000000000 1.800000000000000 1.450000000000000
Columns 4 through 5
1.428125000000000 1.417187500000000
a_ =
Columns 1 through 3
1.100000000000000 1.275000000000000 1.362500000000000
Columns 4 through 5
1.406250000000000 1.411718750000000
x_ =
Columns 1 through 3
0 1.800000000000000 1.450000000000000
Columns 4 through 6
1.275000000000000 1.362500000000000 1.406250000000000
Columns 7 through 9
1.428125000000000 1.417187500000000 1.414453125000000
n_i = 9
b_ =
Columns 1 through 3
2.500000000000000 1.800000000000000 1.450000000000000
Columns 4 through 6
1.428125000000000 1.417187500000000 1.414453125000000
a_ =
Columns 1 through 3
1.100000000000000 1.275000000000000 1.362500000000000
Columns 4 through 5
1.406250000000000 1.411718750000000
xsol = 1.414453125000000
x_ =              0 1.414453125000000
［シミュレーション終了］
以下は、上述の本実施の形態で用いられるMatlabのプログラムのソースコードである。
-----------------------------------------------------------------------
function [b]=hex2bin(h);
% hex2bin- this function converts an array of% hex numbers into binary digits
% Inputs
% h - array of hexadecimal numbers,each row is% a number, the output is a string array
% Outputs
% b- array of binary numbers, each row is a number%
% written by J. Dickerson, ISU, 7/96% updated for matlab 5, 3/98
[nsamp,nbits]=size(h);
nb_bits=ceil(nbits*4);% number of binary bits
% convert to binary
b=zeros(nsamp,nb_bits);
b=num2str(round(b),'%1d');
%b=reshape(bs',nb_bits,nsamp)';
for i=1:nsampfor j=1:nbits
htmp=h(i,j);%i,j,
if (htmp=='0')
b(i,(j-1)*4+1:j*4)='0000';
elseif (htmp=='1')
b(i,(j-1)*4+1:j*4)='0001';
elseif (htmp=='2')
b(i,(j-1)*4+1:j*4)='0010';
elseif (htmp=='3')
b(i,(j-1)*4+1:j*4)='0011';
elseif (htmp=='4')
b(i,(j-1)*4+1:j*4)='0100';
elseif (htmp=='5')
b(i,(j-1)*4+1:j*4)='0101';
elseif (htmp=='6')
b(i,(j-1)*4+1:j*4)='0110';
elseif (htmp=='7')
b(i,(j-1)*4+1:j*4)='0111';
elseif (htmp=='8')
b(i,(j-1)*4+1:j*4)='1000';
elseif (htmp=='9')
b(i,(j-1)*4+1:j*4)='1001';
elseif (htmp=='A')|(htmp=='a')
b(i,(j-1)*4+1:j*4)='1010';
elseif (htmp=='B')|(htmp=='b')
b(i,(j-1)*4+1:j*4)='1011';
elseif (htmp=='C')|(htmp=='c')
b(i,(j-1)*4+1:j*4)='1100';
elseif (htmp=='D')|(htmp=='d')
b(i,(j-1)*4+1:j*4)='1101';
elseif (htmp=='E')|(htmp=='e')
b(i,(j-1)*4+1:j*4)='1110';
elseif (htmp=='F')|(htmp=='f')
b(i,(j-1)*4+1:j*4)='1111';
end;
end;
end;
------------------------------------------------------------------------
function [ret] = logicd(x,beta,a,sigma)
ret=(1-beta)*(x==a)+beta*exp(-sigma*(x-a)^2);
------------------------------------------------------------------------
function [ret]=logicp(x,beta,a,gamma,sigma)
if x>a
dd=1;sg=1;
elseif x<a
dd=0;sg=-1;
else
dd=0;sg=-1;
end
ret=(1-beta)*(x>a)+beta*(dd-(1/2+(1/2-gamma)*sg)*sg*exp(-sg*sigma*(x-a)));
------------------------------------------------------------------------
function [ret]=blogicn(x,beta,a,gamma,sigma)
%eps1=2^-10;ifx>a
dd=1;sg=1;
elseif x<a
dd=0;sg=-1;
else
dd=0;sg=-1;
end
ret=(1-beta)*(x<a)+beta*(1-(dd-(1/2+(gamma-1/2)*sg)*sg*exp(-sg*sigma*(x-a))));
------------------------------------------------------------------------
function [ret]=dblogicd(x,beta,a,sigma)
ret=(1-beta)*(x==a)-2*beta*sigma*(x-a)*exp(-sigma*(x-a)^2);
------------------------------------------------------------------------
function [ret]=dlogicp(x,beta,a,gamma,sigma)
if x>a
dd=0;sg=1;
elseif x<a
dd=0;sg=-1;
else
dd=0;sg=-1;
end
ret=(1-beta)*(x==a)+beta*(dd+sigma*(1/2+(1/2-gamma)*sg)*exp(-sg*sigma*(x-a)));
------------------------------------------------------------------------
function [ret]=dlogicn(x,beta,a,gamma,sigma)
if x>a
dd=0;sg=1;
elseif x<a
dd=0;sg=-1;
else
dd=0;sg=-1;
end
ret=-(1-beta)*(x==a)+beta*(-(dd+sigma*(1/2+(gamma-1/2)*sg)*exp(-sg*sigma*(x-a))));
------------------------------------------------------------------------
function y=testf2(x)
y=x^2-2;
------------------------------------------------------------------------
%写像力学系処理領域：DS_R1 while
function xsol=bwds(a,b,i,delta0)na=1;
nb=1;ni=1;nx=1;nf=1;
n_a=na;n_b=nb;n_i=ni;n_x=nx;n_f=nf;a_(n_a)=a;b_(n_b)=b;i_(n_i)=i;e1=0;
while e1==0
e1=(abs(b_(n_b)-a_(n_a))<delta0);n_x=(nx+1)*(1-e1)+nx*e1;
x_(n_x)=(a_(n_a)+b_(n_b))/2n_i=(ni+1)*(1-e1)+ni*e1i_(n_i)=(i_(ni)+1)*(1-e1);
n_f=(nf+1)*(1-e1)+nf*e1;
f(n_f)=testf2(x_(n_x));e2=(f_(n_f)>=0);e3=(f_(n_f)<=0);
%e4=1-(1-(1-e2))*(1-e3);
n_b=(nb+1)*e2+nb*(1-e2);
b_(n_b)=x_(n_x)*e2+b_(nb)*(1-e2)n_a=(na+1)*e3+na*(1-e3);
a_(n_a)=x_(n_x)*e3+a_(na)*(1-e3)na=n_a;
nb=n_b;ni=n_i;nx=n_x;nf=n_f;end
xsol=x_(n_x)
------------------------------------------------------------------------
% 写像処理領域：F_R1
format longa_(1)=2.5
b_(1)=1.1
f_(1)=testf2(a_(1))
f2_(1)=testf2(b_(1))e1=(f_(1)*f2_(1)>0)
% error('no sign change').*e1+phi.*(1-e1)if e1==1error('no sign change');
end
e2=(f_(1)>0)
% n_x=0.*e2+phi.*(1-e2)n_x=1+e2
%x_(n_x)=a_(1)*e2+phi.*(1-e2)x_(n_x)=a_(1)*e2
n_a=1+e2
a_(n_a)=b_(1)*e2+a_(1)*(1-e2)n_b=1+e2
b_(n_b)=x_(n_x)*e2+b_(1)*(1-e2)
% now f(a)<=0<=f(b)
i_(1)=2; 
% counts number of function evaluationse3 =(f_(1)==0)
n2_x=(n_x+1)*e3+(n_x+1)*(1-e3)
x_(n2_x)=a_(n_a)*e3+bwds(a_(n_a),b_(n_b),i_(1),10^(-3))*(1-e3)
---------------------------------------------------------------------
以上、ソースコード終わり。
【図面の簡単な説明】
【０１７３】
【図１】手続き型プログラミング言語の一種による標準的な二分法プログラムのソースコードを示す説明図である。
【図２】本発明の一実施の形態であるプログラム論理の検証方法、プログラム論理の検証プログラムにて用いられる論理演算のためのＢｏｏｌｅａｎ関数の真理値表の一例を示す概念図である。
【図３】ＩＥＥ７５４における数値の内部表現を示す説明図である。
【図４】浮動小数点の演算例の出力結果を示す対話画面の説明図である。
【図５】浮動小数点の演算例の出力結果を示す対話画面の説明図である。
【図６】連続変形型の論理関数とその導関数の例を示す線図である。
【図７】連続変形型の論理関数とその導関数の例を示す線図である。
【図８】連続変形型の論理関数とその導関数の例を示す線図である。
【図９】連続変形型の論理関数とその導関数の例を示す線図である。
【図１０】浮動小数点の演算例の出力結果を示す対話画面の説明図である。
【図１１】Ｃ言語のプログラム例を示す説明図である。
【図１２】Ｃ言語のプログラム例を示す説明図である。
【図１３】ｉｆ文を含むプログラム例を示す説明図である。
【図１４】ｅｌｓｅｉｆ文のプログラム例を示す説明図である。
【図１５】ｓｗｉｔｃｈ文のプログラム例を示す説明図である。
【図１６】ｆｏｒ文のプログラム例を示す説明図である。
【図１７】ｗｈｉｌｅ文のプログラム例を示す説明図である。
【図１８】書き換えた結果の写像処理領域のプログラムコード例を示す説明図である。
【図１９】書き換えた結果の写像力学系処理領域のプログラムコード例を示す説明図である。
【図２０】本発明の一実施の形態であるプログラム論理の検証方法、プログラム論理の検証プログラムが実施される情報処理システムの構成例を紙面ブロック図である。
【図２１】本発明の一実施の形態である検証ツールの作用の一例を示すフローチャートである。
【図２２】本発明の一実施の形態である検証ツールの作用の一例を示すフローチャートである。
【図２３】本発明の一実施の形態である検証ツールの作用の一例を示すフローチャートである。
【図２４】本発明の一実施の形態である検証ツールの作用の一例を示すフローチャートである。
【図２５Ａ】本発明の一実施の形態である検証ツールにて用いられる定義文の一例を示す概念図である。
【図２５Ｂ】本発明の一実施の形態である検証ツールにて用いられる定義文の一例を示す概念図である。
【図２５Ｃ】本発明の一実施の形態である検証ツールにて用いられる定義文の一例を示す概念図である。
【図２６】本発明の一実施の形態である検証ツールによってディスプレイに表示されるモデル表示画面を示す説明図である。
【図２７】潜在的な問題を含むＣ言語のプログラムを示す説明図である。
【図２８】潜在的な問題を含むＣ言語のプログラムを示す説明図である。
【図２９】解析対象となるＣ言語のプログラムを示す説明図である。
【図３０】本発明の実施の形態である検証ツールの解析中に出力される情報例を示す説明図である。
【図３１】本発明の実施の形態である検証ツールの解析中における変数の時間的発展を説明する説明図である。
【図３２】本発明の実施の形態である検証ツールの解析中における変数の時間的発展を説明する説明図である。
【図３３】本発明の実施の形態である検証ツールの解析中における変数の時間的発展を説明する説明図である。
【符号の説明】
【０１７４】
１〜３  エラーレベル
１−１  変数宣言の領域
１−２  写像処理領域
１−３  写像力学系領域
２００  情報処理システム
２０１  ＭＰＵ
２０２  主記憶
２０３  外部記憶装置
２０４  ディスプレイ
２０５  キーボード
２０６  ネットワークインタフェース
３０１  オペレーティングシステム
３０２  検証ツール
３０３  言語処理系
４０１  ソースコード
４０２  判定結果ファイル
４０３  ログファイル
５０１  モデル表示画面
５０２  オリジナル領域
５０３  中間領域
５０４  解析結果領域
【図１３】
2008197851.tif 000020
【図１４】
2008197851.tif 000021
【図１５】
2008197851.tif 000022
【図１６】
2008197851.tif 000023
【図１７】
2008197851.tif 000024
【図１８】
2008197851.tif 000025
【図１９】
2008197851.tif 000026
【図２０】
2008197851.tif 000027
【図２１】
2008197851.tif 000028
【図２２】
2008197851.tif 000029
【図２３】
2008197851.tif 000030
【図２４】
2008197851.tif 000031
【図２５Ｃ】
2008197851.tif 000032
【図２７】
2008197851.tif 000033
【図２８】
2008197851.tif 000034
【図２９】
2008197851.tif 000035
【図３１】
2008197851.tif 000036
【図３２】
2008197851.tif 000037
【図３３】
2008197851.tif 000038
【図１】
2008197851.tif 000039
【図２】
2008197851.tif 000040
【図３】
2008197851.tif 000041
【図４】
2008197851.tif 000042
【図５】
2008197851.tif 000043
【図６】
2008197851.tif 000044
【図７】
2008197851.tif 000045
【図８】
2008197851.tif 000046
【図９】
2008197851.tif 000047
【図１０】
2008197851.tif 000048
【図１１】
2008197851.tif 000049
【図１２】
2008197851.tif 000050
【図２５Ａ】
2008197851.tif 000051
【図２５Ｂ】
2008197851.tif 000052
【図２６】
2008197851.tif 000053
【図３０】
2008197851.tif 000054