(57)【要約】形式言語で記述したソフトウェア仕様から生成したソースコードが、上記ソフトウェアを詳細化した結果であり、上記ソフトウェアを実現するソースコードであることを証明する。少なくともｉｆ条件分岐構造およびｄｏループ構造を含む制御構造を定義するスケジューラを編集するスケジューラ編集手段と、ソフトウェア仕様および編集されたスケジューラから、少なくともｉｆ条件分岐構造あるいはｄｏループ構造を含むソースコードを生成するソースコード生成手段と、ソフトウェア仕様および編集されたスケジューラから、形式言語で記述された制御構造を含むＳｃｈｅｄｕｌｅｄモデルを生成するＳｃｈｅｄｕｌｅｄモデル生成手段と、ソフトウェア仕様および編集されたスケジューラから、プログラミング言語で記述され、ｉｆ条件分岐構造およびｄｏループ構造を含まずにｇｏｔｏ文を含むＦｌａｔｔｅｎｅｄコードを生成するＦｌａｔｔｅｎｅｄコード生成手段と、を備えるソースコード生成装置。
2015087409.tif 000002
【特許請求の範囲】
【請求項１】
形式言語で記述されたソフトウェア仕様から、プログラミング言語で記述されたソースコードを生成するソースコード生成装置であって、  制御構造を含まない前記ソフトウェア仕様の処理について、少なくともif条件分岐構造およびdoループ構造を含む制御構造を定義するスケジューラを編集するスケジューラ編集手段と、  前記ソフトウェア仕様および編集されたスケジューラから、少なくともif条件分岐構造あるいはdoループ構造を含むソースコードを生成するソースコード生成手段と、  前記ソフトウェア仕様および編集されたスケジューラから、前記形式言語で記述された制御構造を含むScheduledモデルを生成するScheduledモデル生成手段と、  前記ソフトウェア仕様および編集されたスケジューラから、前記プログラミング言語で記述され、if条件分岐構造およびdoループ構造を含まずにgoto文を含むFlattenedコードを生成するFlattenedコード生成手段と、  を備えることを特徴とするソースコード生成装置。
【請求項２】
前記ソフトウェア仕様と前記Scheduledモデルとの間の詳細化関係を証明する詳細化証明手段と、  前記Scheduledモデルと前記Flattenedコードとの間の等価性を証明する中間物等価性証明手段と、  前記Flattenedコードと前記ソースコードとの間の等価性を証明するコード等価性証明手段と、  を備えることを特徴とする請求項１に記載のソースコード生成装置。
【請求項３】
前記ソフトウェア仕様は、ガード条件と代入アクションから構成されるイベントを含み、  前記スケジューラ編集手段は、前記イベントを処理とするif条件分岐構造であるif条件分岐要素と、前記イベントを処理とするdoループ構造であるdoループ要素と、前記イベントの逐次結合とを記述し、前記イベント、前記if条件分岐要素、および前記doループ要素に対して、それらの実行前および実行後に成立すべき条件として、それぞれ事前状態および事後状態を記述し、  前記if条件分岐要素と、前記doループ要素と、前記逐次結合と、前記事前状態および事後状態とが記述された前記スケジューラを検査するスケジューラ検査手段を備え、  前記スケジューラ検査手段は、前記事前条件および前記事後条件が、前記スケジューラに記述された前記if条件分岐要素、前記doループ要素、および前記逐次結合おいて、矛盾していないことを確認する、  ことを特徴とする請求項１または２に記載のソースコード生成装置。
【請求項４】
形式言語で記述された別のソフトウェア仕様であって、上限値あるいは下限値を有さない変数や定数を含む制約前仕様から、上限値および下限値を有する変数や定数を含む前記ソフトウェア仕様を生成し、前記ソフトウェア仕様が算術式を含む場合、前記算術式によって、前記上限値および前記下限値を超える値が前記変数に代入されることがないように、前記定数の前記上限値および前記下限値を設定するソフトウェア仕様生成手段、  を備えることを特徴とする請求項１〜３のいずれか１項に記載のソースコード生成装置。
【請求項５】
形式言語で記述され、制御構造を含まないソフトウェア仕様と、制御構造を含まない前記ソフトウェア仕様の処理について、少なくともif条件分岐構造およびdoループ構造を含む制御構造を定義するスケジューラと、プログラミング言語で記述されたソースコードと、前記ソフトウェア仕様および編集されたスケジューラから生成された前記形式言語で記述された制御構造を含むScheduledモデルと、前記ソフトウェア仕様および編集されたスケジューラから生成された前記プログラミング言語で記述され、if条件分岐構造およびdoループ構造を含まずにgoto文を含むFlattenedコードとを、ソースコード生成装置から前記ソフトウェア仕様に対する前記ソースコードの正しさを証明する証拠として受け付ける受付手段と、  前記ソフトウェア仕様と前記Scheduledモデルの詳細化関係を証明する詳細化証明手段と、  前記Scheduledモデルと前記Flattenedコードの等価性を証明する中間物等価性証明手段と、  前記Flattenedコードと前記ソースコードの等価性を証明するコード等価性証明手段と、  を備えることを特徴とするソースコード証明装置。
【請求項６】
形式言語で記述されたソフトウェア仕様から、プログラミング言語で記述されたソースコードを生成するソースコード生成方法であって、  制御構造を含まない前記ソフトウェア仕様の処理について、少なくともif条件分岐構造およびdoループ構造を含む制御構造を定義するスケジューラを編集するスケジューラ編集ステップと、  前記ソフトウェア仕様および編集されたスケジューラから、少なくともif条件分岐構造あるいはdoループ構造を含むソースコードを生成するソースコード生成ステップと、  前記ソフトウェア仕様および編集されたスケジューラから、前記形式言語で記述された制御構造を含むScheduledモデルを生成するScheduledモデル生成ステップと、  前記ソフトウェア仕様および編集されたスケジューラから、前記プログラミング言語で記述され、if条件分岐構造およびdoループ構造を含まずにgoto文を含むFlattenedコードを生成するFlattenedコード生成ステップと、  を含むことを特徴とするソースコード生成方法。
【請求項７】
コンピュータに、  制御構造を含まない形式言語で記述されたソフトウェア仕様の処理について、少なくともif条件分岐構造およびdoループ構造を含む制御構造を定義するスケジューラを編集するスケジューラ編集ステップと、  前記ソフトウェア仕様および編集されたスケジューラから、少なくともif条件分岐構造あるいはdoループ構造を含むプログラミング言語で記述されたソースコードを生成するソースコード生成ステップと、  前記ソフトウェア仕様および編集されたスケジューラから、前記形式言語で記述された制御構造を含むScheduledモデルを生成するScheduledモデル生成ステップと、  前記ソフトウェア仕様および編集されたスケジューラから、前記プログラミング言語で記述され、if条件分岐構造およびdoループ構造を含まずにgoto文を含むFlattenedコードを生成するFlattenedコード生成ステップと、  を実行させることを特徴とするソースコード生成プログラム。
【発明の詳細な説明】
【技術分野】
【０００１】  本発明は、ソフトウェア開発を支援する技術に関し、特に、ソフトウェア仕様からソースコードを生成する技術に関する。
【背景技術】
【０００２】  ソフトウェア仕様の正しさの形式手法による検証は、当該ソフトウェアの仕様を、数学的意味を持つ形式言語によって記述し、上記形式言語で記述されたソフトウェア仕様（以下、形式モデルと呼ぶ）の正しさを、数学的手法に基づいて証明することで行われる。特許文献１ではさらに、上記証明済みの形式モデルからソースコードを生成する方法を開示している。証明済み形式モデルからソースコードを生成することで、人手でのソースコード開発における不具合の混入を回避するとともに、ソースコード開発の手間を削減することができる。その結果、ソフトウェア開発工数の低減や、ソフトウェア不具合の削減といった効果が得られる。【０００３】  形式手法の一種であるEvent-Bなどでは、不確定要素の多い開発上流工程の仕様を証明対象としているため、処理（イベント）の制御構造を特定しない抽象度の高い形式言語で形式モデルを記述する。一方、C言語などの一般的なソースコード記述言語（プログラミング言語）においては、処理の制御構造を詳細に記述する。よって、Event-Bの形式モデルのように上記制御構造を含まない形式モデルからソースコードを生成するためには、上記制御構造を定義する必要がある。【０００４】  非特許文献１では、Event-B言語を拡張し、上記制御構造を定義できるようにすることで、Event-B言語で記述した形式モデルからのソースコード生成を可能にする方法を開示している。この方法により、上記制御構造を含まない形式モデルからソースコードを生成できるようになる。その結果、上記制御構造を含まない形式モデルにてソフトウェア仕様を証明した場合でも、ソースコード生成によるソフトウェア開発工数の低減といった効果が得られるようになる。
【先行技術文献】
【特許文献】
【０００５】
【特許文献１】特許２９４６７１５号公報
【非特許文献】
【０００６】
【非特許文献１】Edmunds、 Andrew and Butler、 Michael著、「Tasking Event-B: An Extension to Event-B for Generating Concurrent Code」、In PLACES 2011、 Saarbrucken、 Germany。
【発明の概要】
【発明が解決しようとする課題】
【０００７】  上記従来技術によって、形式モデルに対して制御構造を定義でき、さらにその制御構造を含む形式モデルからソースコードを生成できるようになる。上記ソースコードの生成は、ツールによって実現される。この時、上記ツールの実装に誤りがあった場合、生成されたソースコードにも誤りが混入する可能性がある。ここで言う「誤り」とは、生成したソースコードが、生成元の形式モデルが表すソフトウェア仕様を詳細化した結果ではなく、上記ソフトウェア仕様を実現しないということを意味する。【０００８】  つまり従来技術では、ツールの不具合などによって、誤りのあるソースコードが生成される可能性がある。そして、Event-Bのように上記制御構造を含まない抽象度の高い形式言語で形式モデルを記述した場合、上記形式モデルと上記ソースコードには上記制御構造を含む／含まないという差異が生じる。また、上記形式言語ではイベント形式で処理を記述するが、上記ソースコード記述言語では手続き形式で処理を記述するなど、言語上の違いもある。上記理由から、上記形式モデルと生成したソースコードとの比較は困難であり、上記誤りを検出できないという問題がある。【０００９】  上記誤りのあるソースコードの検出にはテストが有効ではあるが、テストでは上記誤りを必ず検出できるとは限らないため、上記問題を解決する手段としては不十分である。【００１０】  以上より、Event-Bのような制御構造を特定しない抽象度の高い形式言語で形式モデルを記述し、上記形式モデルからソースコードを生成した場合に、上記ソースコードの誤りを検出できるようにすることが課題となる。【００１１】  上記に鑑み、上記課題に対処し、上記形式モデルから生成したソースコードの誤りを検出可能にすることで、ソフトウェアの不具合を削減するための技術を提供することを目的とする。
【課題を解決するための手段】
【００１２】  上述した課題を解決し、目的を達成するために、本発明にかかるソースコード生成装置は、形式言語で記述されたソフトウェア仕様から、プログラミング言語で記述されたソースコードを生成するソースコード生成装置であって、制御構造を含まない前記ソフトウェア仕様の処理について、少なくともif条件分岐構造およびdoループ構造を含む制御構造を定義するスケジューラを編集するスケジューラ編集手段と、前記ソフトウェア仕様および編集されたスケジューラから、少なくともif条件分岐構造あるいはdoループ構造を含むソースコードを生成するソースコード生成手段と、前記ソフトウェア仕様および編集されたスケジューラから、前記形式言語で記述された制御構造を含むScheduledモデルを生成するScheduledモデル生成手段と、前記ソフトウェア仕様および編集されたスケジューラから、前記プログラミング言語で記述され、if条件分岐構造およびdoループ構造を含まずにgoto文を含むFlattenedコードを生成するFlattenedコード生成手段と、を備えることを特徴とするソースコード生成装置として構成される。【００１３】  また、本発明は、上記ソースコード生成装置で行われるソースコード生成方法、ソースコード生成プログラムとしても把握される。また、本発明は、上記ソースコード生成装置から受け付けたデータを用いて詳細化および等価性を証明するソースコード証明装置として構成される。
【発明の効果】
【００１４】  本発明によれば、形式モデルから生成したソースコードの誤りを検出可能にすることで、ソフトウェアの不具合を削減するための技術を提供することができる。
【図面の簡単な説明】
【００１５】
【図１】ソースコード生成装置の構成例を示すブロック図である。
【図２】ソソースコード生成装置のハードウェア構成例を示すブロック図である。
【図３】ソースコード証明装置の構成例を示すブロック図である。
【図４Ａ】Developedモデル（マシン）の例である。
【図４Ｂ】Developedモデル（マシン）の例である。
【図５】Developedモデル（コンテクスト）の例である。
【図６Ａ】Restrictedモデル（マシン）の例である。
【図６Ｂ】Restrictedモデル（マシン）の例である。
【図７】Restrictedモデル（コンテクスト）の例である。
【図８】スケジューラの例である。
【図９Ａ】Scheduledモデルの例である。
【図９Ｂ】Scheduledモデルの例である。
【図９Ｃ】Scheduledモデルの例である。
【図１０】Flattenedコードの例である。
【図１１】Targetコードの例である。
【図１２】モデル変換部の手順例を示すフローチャートである。
【図１３Ａ】中間物生成部の手順例を示すフローチャート（Scheduledモデル生成手順）である。
【図１３Ｂ】中間物生成部の手順例を示すフローチャート（Scheduledモデル生成手順）である。
【図１３Ｃ】中間物生成部の手順例を示すフローチャート（Scheduledモデル生成手順）である。
【図１４Ａ】中間物生成部の手順例を示すフローチャート（Flattenedコード生成手順）である。
【図１４Ｂ】中間物生成部の手順例を示すフローチャート（Flattenedコード生成手順）である。
【図１４Ｃ】中間物生成部の手順例を示すフローチャート（Flattenedコード生成手順）である。
【図１５】Event-B言語からC言語への変換ルールの例である。
【図１６Ａ】コード生成部の手順例を示すフローチャートである。
【図１６Ｂ】コード生成部の手順例を示すフローチャートである。
【図１７】モデル詳細化証明部の手順例を示すフローチャートである。
【図１８Ａ】中間物等価性証明部の手順例を示すフローチャートである。
【図１８Ｂ】中間物等価性証明部の手順例を示すフローチャートである。
【図１９】コード等価性証明部の手順例を示すフローチャートである。
【図２０Ａ】goto変換処理の手順例を示すフローチャートである。
【図２０Ｂ】goto変換処理の手順例を示すフローチャートである。
【発明を実施するための形態】
【００１６】  以下、本発明の実施の一形態を、図面を参照しながら詳細に説明する。
【００１７】  本実施形態は、ソースコード生成装置に適用される。本実施形態では、ソフトウェア仕様の正しさを形式的に証明した形式モデルであるRestrictedモデルから、生成対象のソースコードであるTargetコードを生成する際において、制御構造を含む形式モデルであるScheduledモデルと、if分岐やdoループの代わりにgoto文を使用したソースコードであるFlattenedコードを併せて生成する。上記Scheduledモデルと上記Flattenedコードは、上記Restrictedモデルと上記Targetコードとの制御構造の有無に関する差異や、言語上の差異を橋渡しする役割を担う。つまり、上記Restrictedモデルと上記Scheduledモデルの詳細化関係の証明、上記Scheduledモデルと上記Flattenedコードの等価性の証明、および上記Flattenedコードと上記Targetコードの等価性の証明を行うことで、上記Targetコードが、上記Restrictedモデルが表す仕様を詳細化した結果であることを証明できるようになる。
【００１８】  よって本実施形態によれば、生成したソースコードである上記Targetコードに誤りがあることを検出できるようになるため、上記Targetコードを使用するソフトウェアの不具合を削減できる。
【００１９】  また本実施形態では、上記Restrictedモデルから上記Targetコード、上記Scheduledモデル、および上記Flattenedコードを生成するために、上記Restrictedモデルの処理の制御構造を表すスケジューラの入力を受け付ける。上記スケジューラでは、上記Restrictedモデルが含むイベントを使って、if条件分岐構造、doループ構造、及び逐次結合を記述できる。さらに、上記スケジューラでは、上記イベント、上記if条件分岐構造、および上記doループ構造に対して、それらの実行前および実行後に成立すべき条件である事前状態および事後状態を記述できる。
【００２０】  加えて本実施形態では、上記スケジューラにおいて、上記事前条件および上記事後条件に関する矛盾がないことを確認することで、上記スケジューラが示す制御構造が実行可能であることを確認できる。上記スケジューラにおいて実行不可能な制御構造を設計した場合、上記Scheduledモデルは上記Restrictedモデルを詳細化した結果にはならない。つまり、上記スケジューラの設計誤りを、上記Scheduledモデル、上記Flattenedコード、および上記Targetコードの生成前に確認できる。よって本実施形態によれば、上記スケジューラに設計誤りがあった場合の手戻り工数を削減できる。
【００２１】  また本実施形態では、上記Restrictedモデルに含まれる変数や定数は、上限値および下限値を持つという制約がある。同様に、上記Restrictedモデルが算術式を含む場合、上記算術式によって、上記上限値および上記下限値を超える値が、上記変数に代入されることはないという制約を持つ。さらに本実施例では、上記Restrictedモデルを、上記のような制約を持たないDevelopedモデルから生成する。そして、上記Restrictedモデルは、上記Developedモデルを詳細化した結果であることを証明できる。よって本実施形態によれば、上記Targetコードを得るために、上記Developモデルから上記Restrictedモデルを作成する工数を削減できる。
【００２２】  図１は、Event-Bを対象とした本実施形態におけるソースコード生成装置２０１の構成例を示すブロック図である。
【００２３】  ソースコード生成装置２０１は、モデル編集部１０１、Developedモデル保持部１０２、モデル変換部１０３、Restrictedモデル保持部１０４、コード生成部１０５、Scheduledモデル保持部１０６、Flattenedコード保持部１０７、Targetコード保持部１０８、モデル詳細化証明部１０９、詳細化証明結果保持部１１０、スケジューラ保持部１１１、スケジューラ編集部１１２、スケジューラ検査部１１３、中間物等価性証明部１１４、中間物証明結果保持部１１５、コード等価性証明部１１６、コード証明結果保持部１１７、及び中間物生成部１１８を含む。
【００２４】  モデル編集部１０１は、Event-B言語で記述されたDevelopedモデルの作成・編集を受け付け、Developedモデル保持部１０２に登録する。Developedモデルは、上限値あるいは下限値を持たない変数や定数を含む形式モデルである。
【００２５】  モデル変換部１０３は、Developedモデル保持部１０２からDevelopedモデルを取得し、Event-B言語で記述されたRestrictedモデルに変換する。変換の手順例は図１２に示す。Restrictedモデルに含まれる変数や定数は、上限値および下限値を持つ。また、上記Restrictedモデルが算術式を含む場合、上記算術式によって、上記上限値および上記下限値を超える値が、上記変数に代入されることがないように上記定数の上記上限値および上記下限値が設定されている。作成したRestrictedモデルは、Restrictedモデル保持部１０４に登録する。
【００２６】  コード生成部１０５は、Restrictedモデル保持部１０４からRestrictedモデルを取得し、取得したRestrictedモデルから、C言語などのプログラミング言語で記述されたTargetコードを生成し、Targetコード保持部１０８に登録する。上記Targetコードは、if条件分岐構造やdoループ構造を含むソースコードである。コード生成の手順例は図１６Ａ、Ｂに示す。
【００２７】  スケジューラ編集部１１２は、スケジューラの作成・編集を受け付け、スケジューラ保持部１１１に登録する。上記スケジューラでは、上記Restrictedモデルが含むイベント（EVENTS）を使って、if条件分岐構造、doループ構造、及び逐次結合を記述できる。さらに、上記スケジューラでは、上記イベント、上記if条件分岐構造、および上記doループ構造に対して、それらの実行前および実行後に成立すべき条件である事前状態および事後状態を記述できる。
【００２８】  スケジューラ検査部１１３は、スケジューラ保持部１１１からスケジューラを取得し、上記スケジューラにおいて、上記事前条件および上記事後条件に関する矛盾がないことを検査する。例えば、ある条件condを持つif条件分岐構造branにおいて、条件が成立する場合に実行されるイベントevtがあるとする。この場合、if条件分岐構造branの事前条件および条件condから、イベントevtの事前条件を導出できなければならない。同時に、イベントevtの事後条件から、if条件分岐構造branの事後条件が導出できなければならない。また、イベントevtの代わりに、イベントevt1とイベントevt2の逐次結合を実行する場合は、イベントevt1の事後条件から、イベントevt2の事前条件が導出できなければならない。これらの導出が不可能である場合、上記スケジューラが示す制御構造は実行不可能な誤りのある制御構造ということになる。
【００２９】  図８は、上記スケジューラの例を表しており、[]で囲まれた行８０３は、上にあるdoループ構造の事後条件を表している。また、{}で囲まれた行８０４は、下にあるイベントfinalの事前条件を表している  中間物生成部１１８は、Restrictedモデル保持部１０４からRestrictedモデルを取得し、Event-B言語で記述されたScheduledモデル、及びC言語などのプログラミング言語で記述されたFlattenedコードを生成する。生成したScheduledモデル、及びFlattenedコードは、それぞれScheduledモデル保持部１０６、及びFlattenedコード保持部１０７に登録する。Scheduledモデルは、上記スケジューラにて定義した上記制御構造を、上記Restrictedモデルに反映したモデルである。上記Flattenedコードは、上記Targetコードとは異なり、if条件分岐構造およびdoループ構造を含まない。その代わりに、上記Flattenedコードは、goto文を含む。Scheduledモデル、及びFlattenedコードの生成手順の例は、それぞれ図１３Ａ〜Ｃ及び図１４Ａ〜Ｃに示す。
【００３０】  本実施形態では、Targetコードの記述言語の例としてC言語を使用しているが、他のプログラミング言語で記述されたTargetコードを生成することもできる。そのためには、上記FlattenedコードもTargetコードと同様の他のプログラミング言語で記述し、さらにコード等価性証明部１１６を上記他のプログラミング言語に対応させる必要がある。あるいは、上記Flattenedコードを抽象的な疑似コード（Pseudoコード）として記述し、コード等価性証明部１１６を、Targetコードの記述言語ごとに用意するという方法もある。
【００３１】  モデル詳細化証明部１０９は、Restrictedモデル保持部１０４およびScheduledモデル保持部１０６から、それぞれRestrictedモデルおよびScheduledモデルを取得し、上記Scheduledモデルが、上記Restrictedモデルを詳細化した結果であることを証明する。証明結果は、詳細化証明結果保持部１１０に登録する。上記証明手順の例は図１７に示す。詳細化証明結果保持部１１０が保持する上記証明結果は、上記Developedモデル及び上記Restrictedモデルと、「証明成功」あるいは「証明失敗」のメッセージから構成される。
【００３２】  また同様に、モデル詳細化証明部１０９は、Developedモデル保持部１０２からDevelopedモデルを取得し、上記Restrictedモデルが、上記Developedモデルを詳細化した結果であることを証明する。証明結果は、詳細化証明結果保持部１１０に登録する。上記証明は、図１７に示す手順と同様の手順で実施できる。詳細化証明結果保持部１１０が保持する上記証明結果は、上記Restrictedモデル及び上記Scheduledモデルと、「証明成功」あるいは「証明失敗」のメッセージから構成される。
【００３３】  中間物等価性証明部１１４は、Scheduledモデル保持部１０６およびFlattenedコード保持部１０７から、それぞれScheduledモデルおよびFlattenedコードを取得し、上記Scheduledモデルと上記Flattenedコードが等価であることを証明する。証明結果は、中間物証明結果保持部１１５に登録する。上記証明手順の例は、図１８Ａ、Ｂに示す。中間物証明結果保持部１１５が保持する証明結果は、上記Scheduledモデルおよび上記Flattenedコードと、「証明成功」あるいは「証明失敗」のメッセージから構成される。
【００３４】  コード等価性証明部１１６は、Flattenedコード保持部１０７およびTargetコード保持部１０８から、それぞれFlattenedコードおよびTargetコードを取得し、上記Flattenedコードと上記Targetコードが等価であることを証明する。証明結果は、コード証明結果保持部１１７に登録する。上記証明手順の例は、図１９および図２０Ａ、Ｂに示す。コード証明結果保持部１１７が保持する証明結果は、上記Flattenedコードおよび上記Targetコードと、「証明成功」あるいは「証明失敗」のメッセージから構成される。
【００３５】  図２は、本実施形態におけるソースコード生成装置のハードウェア構成例を示す図である。
【００３６】  ソースコード生成装置２０１は、ＣＰＵ２０２、メモリ２０３、外部記憶装置２０４、表示装置２０５、入力装置２０６、及び外部媒体入出力装置２０７を備える。
【００３７】  ＣＰＵ２０２は、メモリ２０３に記憶されたプログラムを実行することによって、各種処理を実行する。メモリ２０３は、ＣＰＵ２０２のワークエリアとして機能し、プログラム及びプログラムの実行に必要なデータを記憶する。具体的には、モデル編集部１０１、モデル変換部１０３、コード生成部１０５、モデル詳細化証明部１０９、スケジューラ編集部１１２、スケジューラ検査部１１３、中間物等価性証明部１１４、コード等価性証明部１１６、及び中間物生成部１１８を構成するプログラムが記憶され、同時にDevelopedモデル保持部１０２、Restrictedモデル保持部１０４、Scheduledモデル保持部１０６、Flattenedコード保持部１０７、Targetコード保持部１０８、詳細化証明結果保持部１１０、スケジューラ保持部１１１、中間物証明結果保持部１１５、及びコード証明結果保持部１１７の保持するデータが記憶される。
【００３８】  外部記憶装置２０４は、各種データを格納する。外部記憶装置２０４は、例えば、ハードディスク装置などである。具体的には、Developedモデル保持部１０２、Restrictedモデル保持部１０４、Scheduledモデル保持部１０６、Flattenedコード保持部１０７、Targetコード保持部１０８、詳細化証明結果保持部１１０、スケジューラ保持部１１１、中間物証明結果保持部１１５、及びコード証明結果保持部１１７が格納される。
【００３９】  あるいは、モデル編集部１０１、モデル変換部１０３、コード生成部１０５、モデル詳細化証明部１０９、スケジューラ編集部１１２、スケジューラ検査部１１３、中間物等価性証明部１１４、コード等価性証明部１１６、及び中間物生成部１１８を構成するプログラムの少なくとも一部についても、外部記憶装置２０４に格納され、各種処理実行の際にＣＰＵ２０２がメモリ２０３へ読み出してプログラムを実行することとしてもよい。また各プログラムは、あらかじめ、メモリ２０３または外部記憶装置２０４に格納されていても良いし、必要に応じ、利用可能な媒体を介して、他の装置からメモリ２０３または外部記憶装置２０４に導入されてもよい。媒体とは、例えば、外部媒体入出力装置２０７に着脱可能な記憶媒体、または、ネットワークや、ネットワークを伝搬する搬送波やデジタル信号などの通信媒体を指す。
【００４０】  表示装置２０５は、プログラムの処理結果などを表示する。表示装置２０５は、例えば、ディスプレイなどである。入力装置２０６は、処理の実行指示及び処理に必要な情報の入力などを利用者から受け付ける。入力装置２０６は、例えば、キーボード及びマウスなどである。
【００４１】  外部媒体入出力装置２０７は、外部媒体と、外部記憶装置２０４に格納されているデータなどの入出力を行う。外部媒体は、外部媒体入出力装置２０７に着脱可能で可搬性のある記憶媒体であり、外部媒体出力装置２０７は、外部媒体に読み書き可能なドライブ装置などである。
【００４２】  通信装置２１２は、外部媒体と、外部記憶装置２０４に格納されているデータなどの送受信を行う。例えば、ローカルエリアネットワークやインターネットなどである。
【００４３】  ソースコード生成装置２０１は、ネットワーク２０９を通じて、ソースコード証明装置２１０と接続される。ソースコード証明装置２１０は、ソースコード生成装置２０１と同様のハードウェア構成を持つ。
【００４４】  ソースコード生成装置２０１は、開発者２０８によって使用され、作成されたDevelopedモデル、Restrictedモデル、Scheduledモデル、Flattenedコード、及びTargetコードは、通信装置２１２およびネットワーク２０９を通じて、ソースコード証明装置２１０に送信される。検証者２１１は、ソースコード証明装置２１０を使用して上記のDevelopedモデル、Restrictedモデル、Scheduledモデル、Flattenedコード、及びTargetコードを受信する。そして、ソースコード生成装置２０１にも含まれる、モデル詳細化証明部１０９、中間物等価性証明部１１４、およびコード等価性証明部１１６を使用して各々の証明を行う。
【００４５】  本実施例では、Developedモデル、Restrictedモデル、Scheduledモデル、Flattenedコード、及びTargetコードを受け渡す手段としてネットワークを採用したが、外部媒体入出力装置２０７を使用して、外部媒体による受け渡しを行っても良い。
【００４６】  図３は、ソースコード証明装置２１０の構成例を示すブロック図である。
【００４７】  ソースコード証明装置２１０は、Developedモデル保持部１０２、Restrictedモデル保持部１０４、Scheduledモデル保持部１０６、Flattenedコード保持部１０７、Targetコード保持部１０８、モデル詳細化証明部１０９、詳細化証明結果保持部１１０、中間物等価性証明部１１４、中間物証明結果保持部１１５、コード等価性証明部１１６、コード証明結果保持部１１７、及び入力受付部３０１を含む。
【００４８】  入力受付部３０１は、Developedモデル、Restrictedモデル、Scheduledモデル、Flattenedコード、Targetコードの入力を受け付け、それぞれDevelopedモデル保持部１０２、Restrictedモデル保持部１０４、Scheduledモデル保持部１０６、Flattenedコード保持部１０７、Targetコード保持部１０８に登録する。ソースコード生成装置２０１と同様の方法によって、登録されたモデルおよびコードの詳細化関係や等価性を証明する。
【００４９】  図４Ａ、Ｂおよび図５は、Developedモデル保持部１０２が保持するDevelopedモデルを構成するマシンとコンテクストの例である。図６Ａ、Ｂおよび図７は、Restrictedモデル保持部１０４が保持するRestrictedモデルを構成するマシンとコンテクストの例である。
【００５０】  図８はスケジューラ保持部１１１が保持するスケジューラの例である。図９Ａ〜ＣはScheduledモデル保持部１０６が保持するScheduledモデルの例である。上記Scheduledモデルは，カウンタ変数pcを含んでおり，上記カウンタ変数を使って，処理（イベント）の制御構造を定義している．例えば，ガード９１３のようにガードとして使用することで，処理（イベント）の制御構造を定義する．  図１０はFlattenedコード保持部１０７が保持するFlattenedコードの例である。図１１はTargetコード保持部１０８が保持するTargetコードの例である。図１２はモデル変換部の手順例を示すフローチャートである。以下に示す処理は、ソースコード生成装置２０１の備えるＣＰＵ２０２が、メモリ２０３で実行するプログラムによって実現される。そしてこのプログラムは、以下に説明される各種の動作を行うためのコードから構成されている。
【００５１】  ＣＰＵ２０２は、モデル変換部１０３を実行することによって、Developedモデル保持部１０２から取得したDevelopedモデルにおいて、リファインメントによって最も詳細化された詳細マシンをさらに詳細化（REFINES）することで、新規マシンを作成する。同時に、上記詳細マシンの参照するコントクストを拡張（EXTENDS）することで、新規コンテクストを作成する。上記新規マシンは、上記新規コンテクストを参照（SEES）する（ステップ１２０１）。図６Ａ、Ｂの例では、新規マシンm_resはDevelopedモデルの詳細マシンm2を詳細化（REFINES）しており、さらに新規コンテクストc0_resを参照（SEES）している。また図７に示す通り、新規コンテクストc0_resは、上記詳細マシンm2の参照するコンテクストc0を拡張（EXTENDS）している。
【００５２】  Event-Bでは、リファインメントと呼ばれる形式モデルの設計手法を採用している（例えば、非特許文献２（Jean-Raymond Abrial著、「Modeling in Event-B」、Cambridge University Press、2010年。）、pp。21など参照）。リファインメントとは、対象のソフトウェア仕様の一部を抽象的にモデル記述した後、段階的に仕様を追加および詳細化していく設計手法である。上記リファインメントの正しさの証明は、リファインメントに関する証明責務と呼ばれる論理式を証明することで行われる。
【００５３】  モデル変換部１０３は、上記新規コンテクストにおいて、上記新規マシンや上記新規コンテクストに含まれる変数、定数、及びキャリア集合の値域を定義するための上限値および下限値を定義する（ステップ１２０２）。図７の例では、定数宣言７０１、および公理７０３にて、上記上限値MAX_INTおよび下限値MIN_INTを定義している。
【００５４】  モデル変換部１０３は、上記新規コンテクストにおいて、四則演算の算術用関数を定義する（ステップ１２０３）。図７の例では、定数宣言７０２、および公理７０４にて、上記算術用関数c_plus、c_minus、c_mul、及びc_divを定義している。
【００５５】  モデル変換部１０３は、ステップ１２０２で定義した上記上限値および上記下限値を用いて、上記新規コンテクストに含まれる定数、及びキャリア集合の値域を制限する（ステップ１２０４）。図７の例では、公理７０５にて、定数の値域を制限している。
【００５６】  モデル変換部１０３は、ステップ１２０２で定義した上記上限値および上記下限値を用いて、上記新規マシンに含まれる変数の値域を制限する（ステップ１２０５）。図６Ａ、Ｂの例では、インバリアント６０１にて、変数の値域を制限している。ただし、インバリアント６０１の制限は、公理７０５から導出可能のため、定理（THEOREMS）として定義している。
【００５７】  モデル変換部１０３は、上記新規マシンのイベントに含まれる算術式を、ステップ１２０３で作成した上記算術用関数を使った算術式に置き換える（ステップ１２０６）。図４Ａ、Ｂおよび図６Ａ、Ｂの例では、イベントincのアクション４０１を、アクション６０２に置き換えている。その他のイベントに対しても同様の置き換えを行っている。
【００５８】  モデル変換部１０３は、ステップ１２０６で置き換えた算術式について、算術の途中で算出される値が、ステップ１２０２で定義した上記上限値および上記下限値を超えることのないように、定数の値域を制限する（ステップ１２０７）。図７の例では、アクション６０２に含まれるアクションact2において、r+1+qの値が途中算出される。この値が上記上MAX_INTを超えることがないように、公理７０６にて定数nの値を制限している。
【００５９】  図１３Ａ〜Ｃは中間物生成部の手順のうち、Scheduledモデルを生成する手順例を示すフローチャートである。
【００６０】  以下に示す処理は、ソースコード生成装置２０１の備えるＣＰＵ２０２が、メモリ２０３で実行するプログラムによって実現される。そしてこのプログラムは、以下に説明される各種の動作を行うためのコードから構成されている。
【００６１】  ＣＰＵ２０２は、中間物生成部１１８を実行することによって、スケジューラの未処理の行のうち、先頭行を取得する（ステップ１３０１）。中間物生成部１１８は、ステップ１３０１で取得した取得行の種類によって、以下手順を実行する。上記取得行がイベントの場合、ステップ１３０３を実行する。上記取得行がif分岐条件の場合、ステップ１３０９を実行する。上記取得行がdoループ条件の場合、ステップ１３１４を実行する。その他の場合は、ステップ１３０８を実行する（ステップ１３０２）。
【００６２】  中間物生成部１１８は、取得したイベントがINITIALIZATIONか否かを判別する。上記イベントがINITIALIZATIONの場合、ステップ１３０５を実行する。上記イベントがINITIALIZATIONでない場合、ステップ１３０４を実行する（ステップ１３０３）。
【００６３】  中間物生成部１１８は、Restrictedモデルに含まれる上記イベントのガードを全て削除する（ステップ１３０４）。図６Ａ、Ｂのイベントincを例にとると、図９Ａ〜Ｃに示す通り、ガード６０３を削除している。
【００６４】  中間物生成部１１８は、Restrictedモデルに、イベントの実行順序を制御するためのカウンタ変数が追加されていることを確認する。未追加であれば上記カウンタ変数を追加する。その後、上記INITIALIZATIONイベントのアクションに、「上記カウンタ変数を１に初期化する」というアクションを追加する（ステップ１３０５）。図９Ａ〜Ｃの例では、アクション９０３を追加している。
【００６５】  中間物生成部１１８は、Restrictedモデルに、イベントの実行順序を制御するためのカウンタ変数が追加されていることを確認する。未追加であれば上記カウンタ変数を追加する。その後、上記イベントに対して、「上記カウンタ変数は、上記イベントのスケジューラ行番号と等しい」という意味のガードを追加する（ステップ１３０６）。スケジューラ行番号とは、ステップ１３０１にて取得した取得行の、行番号を意味する。図９Ａ〜Ｃの例では、上記ガードとしてガード９０１を追加している。
【００６６】  中間物生成部１１８は、上記イベントに対して、「上記カウンタ変数をインクリメントする」というアクションを追加する（ステップ１３０７）。図９Ａ〜Ｃの例では、アクション９０２を追加している。中間物生成部１１８は、上記スケジューラに未処理の行がある場合はステップ１３０１に戻る。全ての行を処理済みの場合、実行を終了する（ステップ１３０８）。
【００６７】  中間物生成部１１８は、取得したif分岐条件がtrueの場合の分岐イベントであるtrueイベントと、falseの場合の分岐イベントであるfalseイベントを作成する。上記trueイベントのガードには上記if分岐条件の肯定を設定する。上記falseイベントのガードには、上記if分岐条件の否定を設定する（ステップ１３０９）。図８のif分岐条件８０１を例にとると、図９Ａ〜Ｃに示す通り、trueイベントとしてイベントif1_trueを、falseイベントとしてイベントif1_falseを作成している。そして、それぞれのイベントにおいて、ガード９０４とガード９０５を追加している。
【００６８】  中間物生成部１１８は、上記true/falseイベントに、それぞれ「上記カウンタ変数は、上記if分岐条件のスケジューラ行番号と等しい」というガードを追加する（ステップ１３１０）。図９Ａ〜Ｃの例では、ガード９０６とガード９０７を追加している。
【００６９】  中間物生成部１１８は、上記trueイベントに、「上記カウンタ変数をインクリメントする」というアクションを追加する（ステップ１３１１）。図９Ａ〜Ｃの例では、イベント９０８を追加している。
【００７０】  中間物生成部１１８は、上記falseイベントに、「上記カウンタ変数に対して、上記if分岐条件に対応するelseのスケジューラ行番号に１を加えた値を代入する」というアクションを追加する（ステップ１３１２）。図８の例では、else８０７の行番号は４である。よって図９Ａ〜Ｃに示す通り、アクション９０９を追加している。
【００７１】  中間物生成部１１８は、if分岐条件がtrueの場合の分岐から脱出するためのexitイベントを作成する。上記exitイベントは、「上記カウンタ変数は、上記elseのスケジューラ行番号と等しい」というガードと、「上記カウンタ変数に対してfiのスケジューラ行番号に１を加えた値を代入する」というアクションを持つ（ステップ１３１３）。図８の例では、else８０７の行番号は４で、fi８０５の行番号は５である。よって、図９Ａ〜Ｃに示す通り、exitイベント９１０を追加している。
【００７２】  中間物生成部１１８は、取得したdoループ条件がtrueの場合の分岐イベントであるtrueイベントと、falseの場合の分岐イベントであるfalseイベントを作成する。上記trueイベントのガードにはdoループ条件の肯定を設定する。上記falseイベントのガードにはその否定を設定する（ステップ１３１４）。図８のdoループ条件８０２を例にとると、図９Ａ〜Ｃに示す通り、trueイベントとしてイベントloop1_trueを、falseイベントとしてイベントloop1_falseを作成している。そして、それぞれのイベントにおいて、ガード９１１とガード９１２を追加している。
【００７３】  中間物生成部１１８は、上記true/falseイベントに、「上記カウンタ変数が、doループ条件のスケジューラ行番号と等しい」というガードを追加する（ステップ１３１５）。図９Ａ〜Ｃの例では、ガード９１３とガード９１４を追加している。
【００７４】  中間物生成部１１８は、上記trueイベントに、「上記カウンタ変数をインクリメントする」というアクションを追加する（ステップ１３１６）。図９Ａ〜Ｃの例では、アクション９１５を追加している。
【００７５】  中間物生成部１１８は、上記falseイベントに、「カウンタ変数に対してodのスケジューラ行番号に１を加えた値を代入する」というアクションを追加する（ステップ１３１７）。図８の例ではodの行番号は６である。よって図９Ａ〜Ｃに示す通り、アクション９１６を追加している。
【００７６】  中間物生成部１１８は、doループによってodからdoに戻るためのreturnイベントを作成する。上記returnイベントは、「カウンタ変数が、odのスケジューラ行番号と等しい」というガードと、「カウンタ変数に対して、doのスケジューラ行番号を代入する」というアクションを持つ（ステップ１３１８）。図８の例では、odの行番号は６であるため、図９Ａ〜Ｃに示す通り、returnイベント９１７を追加している。
【００７７】  図１４Ａ〜Ｃは、中間物生成部の手順のうち、Flattenedコードを生成する手順例を示すフローチャートである。
【００７８】  以下に示す処理は、ソースコード生成装置２０１の備えるＣＰＵ２０２が、メモリ２０３で実行するプログラムによって実現される。そしてこのプログラムは、以下に説明される各種の動作を行うためのコードから構成されている。
【００７９】  ＣＰＵ２０２は、中間物生成部１１８を実行することによって、スケジューラの未処理の行のうち、先頭行を取得する（ステップ１４０１）。
【００８０】  中間物生成部１１８は、ステップ１４０１で取得した取得行の種類によって、以下手順を実行する。上記取得行がイベントの場合、ステップ１４０３を実行する。上記取得行がif分岐条件の場合、ステップ１４０９を実行する。上記取得行がdoループ条件の場合、ステップ１４１３を実行する。その他の場合は、ステップ１４０７を実行する（ステップ１４０２）。
【００８１】  中間物生成部１１８は、取得したイベントがINITIALIZATIONか否かを判別する。上記イベントがINITIALIZATIONの場合、ステップ１４０４を実行する。上記イベントがINITIALIZATIONでない場合、ステップ１４０５を実行する（ステップ１４０３）。
【００８２】  中間物生成部１１８は、取得したINITIALIZATIONイベントにて初期化される変数を宣言するコードを作成する（ステップ１４０４）。図６Ａ、Ｂの例では、INITIALIZATIONイベントにて変数p、q、rを初期化しているため、図１０に示す通り、コード１００１にてこれらの変数を宣言している。
【００８３】  中間物生成部１１８は、取得した上記イベントのアクションを、当該プログラミング言語のコードに変換する。上記変換ルールの例は、図１５に示す。（ステップ１４０５）。図６Ａ、Ｂのイベントincを例にとると、図１０に示す通り、コード１００２を作成する。
【００８４】  中間物生成部１１８は、上記イベントのスケジューラ行番号を、ステップ１４０５で作成したコードの先頭にラベルとして付与する（ステップ１４０６）。例えば図８の例では、イベントincのスケジューラ行番号は３であるため、図１０において、コード１００２にラベル３を付与している。
【００８５】  中間物生成部１１８は、上記スケジューラに未処理の行がある場合は、ステップ１４０１に戻る。全ての行を処理済みの場合は、ステップ１４０８に進む（ステップ１４０７）。中間物生成部１１８は、作成したコードをラベル番号順に整列する（ステップ１４０８）。
【００８６】  中間物生成部１１８は、取得したif分岐条件の否定を分岐条件として持つ、if文のコードを作成する。上記if文コードの処理には、上記取得したif分岐条件に対応するelseのスケジューラ行番号に１を加えたラベルへジャンプするgoto文コードを記述する（ステップ１４０９）。図８のif分岐条件８０１を例にとると、対応するelse８０７の行番号は４である。そのため、図１０のコード１００４を作成している。
【００８７】  中間物生成部１１８は、上記if分岐条件のスケジューラ行番号を、上記if文コードのラベルとして付与する（ステップ１４１０）。図１０の例では、コード１００４に示す通り、ラベル２を付与している。
【００８８】  中間物生成部１１８は、上記if分岐条件に対応するfiのスケジューラ行番号に１を加えたラベルへジャンプする、goto文のコードを作成する（ステップ１４１１）。図８の例ではfi８０５の行番号は５であるため、図１０の例では、コード１００５を作成している。
【００８９】  中間物生成部１１８は、上記if分岐条件に対応するelseのスケジューラ行番号を、上記goto文コードのラベルとして付与する（ステップ１４１２）。図８の例では、else８０７の行番号は４であるため、図１０の例では、コード１００５に示す通りラベル４を付与している。
【００９０】  中間物生成部１１８は、取得したdoループ条件の否定を分岐条件として持つ、if文のコードを作成する。上記if文コードの処理には、上記取得したdoループ条件に対応するodのスケジューラ行番号に１を加えたラベルへジャンプするgoto文コードを記述する（ステップ１４１３）。図８のdoループ条件８０２を例にとると、対応するod８０６の行番号は６である。そのため、図１０のコード１００３を作成している。中間物生成部１１８は、上記doループ条件のスケジューラ行番号を、上記if文コードのラベルとして付与する（ステップ１４１４）。図１０の例では、コード１００３に示す通り、ラベル１を付与している。
【００９１】  中間物生成部１１８は、上記if文コードのラベルにジャンプするgoto文のコードを作成する（ステップ１４１５）。図１０の例では、コード１００６を作成している。中間物生成部１１８は、上記doループ条件に対応するodのスケジューラ行番号を、上記goto文コードのラベルとして付与する（ステップ１４１６）。図１０の例では、コード１００６に示す通り、ラベル６を付与している。
【００９２】  図１５はEvent-B言語からC言語への変換ルールの例である。変換ルール１５０１は、Event-B記述１５０２と、C言語記述１５０３を含む。Event-B記述１５０２は、変換元のEvent-B言語の記述を表しており、記述中に表れるxやyは、真偽値を表す任意の論理式が代入されるメタ変数である。同様にaやbは、数値を表す任意の論理式が代入されるメタ変数である。C言語記述１５０３は、変換先のC言語の記述を表しており、記述中に表れるxやy、およびaやbは、Event-B記述１５０２に表れる同記号と対応する。またT(x)などの記述は、xを本変換ルールにて変換した結果を表している。例えば変数p、qについて、T(p∧q)は(p&&q)を意味する。
【００９３】  図１６Ａ、Ｂはコード生成部の手順例を示すフローチャートである。以下に示す処理は、ソースコード生成装置２０１の備えるＣＰＵ２０２が、メモリ２０３で実行するプログラムによって実現される。そしてこのプログラムは、以下に説明される各種の動作を行うためのコードから構成されている。
【００９４】  ＣＰＵ２０２は、コード生成部１０５を実行することによって、スケジューラの未処理の行のうち、先頭行を取得する（ステップ１６０１）。
【００９５】  コード生成部１０５は、ステップ１６０１で取得した取得行の種類によって、以下手順を実行する。上記取得行がイベントの場合、ステップ１６０３を実行する。上記取得行がif分岐条件の場合、ステップ１６０７を実行する。上記取得行がdoループ条件の場合、ステップ１４０８を実行する。上記取得行がelseの場合、ステップ１６１１を実行する。上記取得行がfiの場合、ステップ１６０９を実行する。上記取得行がodの場合、ステップ１６１０を実行する。上記取得行が事前条件あるいは事後条件の場合、ステップ１６０６を実行する（ステップ１６０２）。
【００９６】  コード生成部１０５は、取得したイベントがINITIALIZATIONか否かを判別する。上記イベントがINITIALIZATIONの場合、ステップ１６０４を実行する。上記イベントがINITIALIZATIONでない場合、ステップ１６０５を実行する（ステップ１６０３）。
【００９７】  コード生成部１０５は、取得したINITIALIZATIONイベントにて初期化される変数を宣言するコードを作成する（ステップ１６０４）。図６Ａ、Ｂの例では、INITIALIZATIONイベントにて変数p、q、rを初期化しているため、図１１に示す通り、コード１１０１にてこれらの変数を宣言している。
【００９８】  コード生成部１０５は、取得した上記イベントのアクションを、当該プログラミング言語のコードに変換する。上記変換ルールの例は、図１５に示す通りである。（ステップ１６０５）。図６Ａ、Ｂのイベントincを例にとると、図１１に示す通り、コード１１０２を作成する。
【００９９】  コード生成部１０５は、上記スケジューラに未処理の行がある場合は、ステップ１６０１に戻る。全ての行を処理済みの場合は、処理を終了する（ステップ１６０６）。コード生成部１０５は、取得したif分岐条件を分岐条件として持つif文コードと、処理の始点ブラケット（｛）を作成する（ステップ１６０７）。図８のif分岐条件８０１の例では、図１１に示す通り、コード１１０３を作成する。
【０１００】  コード生成部１０５は、取得したdoループ条件をループ条件として持つwhile文コードと、処理の始点ブラケット（｛）を記述する（ステップ１６０８）。図８のdoループ条件８０２の例では、図１１に示す通り、コード１１０４を作成する。
【０１０１】  コード生成部１０５は、取得したfiに対応して、if文コードの終端ブラケット（｝）を記述する（ステップ１６０９）。図８のfi８０５の例では、図１１のコード１１０５を作成する。
【０１０２】  コード生成部１０５は、取得したodに対して、while文コードの終端ブラケット（｝）を記述する（ステップ１６１０）。図８のod８０６の例では、図１１のコード１１０６を作成する。
【０１０３】  コード生成部１０５は、取得したelseに対して、if文コードの終端ブラケット（｝）、else文コード、およびelse文コードの始点ブラケット（｛）を記述する（ステップ１６１１）。図８のelse８０７の例では、図１１のコード１１０７を作成する。
【０１０４】  図１７はモデル詳細化証明部の手順例を示すフローチャートである。以下に示す処理は、ソースコード生成装置２０１の備えるＣＰＵ２０２が、メモリ２０３で実行するプログラムによって実現される。そしてこのプログラムは、以下に説明される各種の動作を行うためのコードから構成されている。
【０１０５】  ＣＰＵ２０２は、モデル詳細化証明部１０９を実行することによって、Restrictedモデル保持部からRestrictedモデルを取得する。さらに、中間物生成部１１８が上記Restrictedモデルから生成したScheduledモデルを、Scheduledモデル保持部１０６から取得する。そして、上記Scheduledモデルのマシンを、上記Restrictedモデルの詳細マシンに設定する。具体的には、上記ScheduledモデルのマシンのREFINESに、上記Restrictedモデルの最も詳細化されたマシンの名称を設定する（ステップ１７０１）。
【０１０６】  モデル詳細化証明部１０９は、上記Scheduledモデルから、上記Restrictedモデルが参照するコンテクストを参照できるようにする。具体的には、上記ScheduledモデルのマシンのSEESに、Restrictedモデルの最も詳細化されたマシンが参照（SEES）しているコンテクストの名称を設定する（ステップ１７０２）。
【０１０７】  モデル詳細化証明部１０９は、上記RestrictedモデルとScheduledモデルからリファインメントに関する証明責務を生成する。リファインメントに関する証明責務の作成方法は、非特許文献２のpp。192-197などにて開示されている（ステップ１７０３）。
【０１０８】  モデル詳細化証明部１０９は、上記証明責務を、推論規則を用いて証明する。証明責務の証明方法は、非特許文献２のpp。306-352などに開示されている。証明結果は、詳細化証明結果保持部１１０に登録する（ステップ１７０４）。
【０１０９】  図１８Ａ、Ｂは中間物等価性証明部の手順例を示すフローチャートである。以下に示す処理は、ソースコード生成装置２０１の備えるＣＰＵ２０２が、メモリ２０３で実行するプログラムによって実現される。そしてこのプログラムは、以下に説明される各種の動作を行うためのコードから構成されている。
【０１１０】  ＣＰＵ２０２は、中間物等価性証明部１１４を実行することによって、Scheduledモデル保持部１０６からScheduledモデルを取得し、そのINITIALIZATIONイベントを取得する（ステップ１８０１）。
【０１１１】  中間物等価性証明部１１４は、上記Scheduledモデルの未処理のイベントのうち、ガードが制約するカウンタ変数の値が最小のイベントを取得する。カウンタ変数の値が最小のイベントは、複数存在する場合がある（ステップ１８０２）。
【０１１２】  中間物等価性証明部１１４は、ステップ１８０２で取得したイベントが、上記カウンタ変数を制約するガード以外のガードを含むかを判定する。含む場合はステップ１８０４に進む。含まない場合はステップ１８０５に進む（ステップ１８０３）。
【０１１３】  中間物等価性証明部１１４は、ステップ１８０２で取得したイベントから、否定形式のガードを持つイベントであるfalseイベントを抽出する（ステップ１８０４）。図９Ａ〜Ｃの例では、カウンタ変数pcが１に制約されるイベントとして、loop1_trueとloop1_falseの２つのイベントがあるが、このうち、否定形式のガード９１２を持つイベントloop1_falseを抽出する。
【０１１４】  中間物等価性証明部１１４は、ステップ１８０２で取得したイベントが含むアクションのうち、上記カウンタ変数を更新するアクションは「pc:=pc+1」であるかを確認する。上記アクションの場合はステップ１８０９を実行する。上記アクションでない場合は、ステップ１８０８を実行する（ステップ１８０５）。例えば図９Ａ〜Ｃのイベントincの場合、カウンタ変数pcに対する代入アクションは、アクション９０２に示す通り「pc:=pc+1」である。よってステップ１８０９を実行する。一方、イベントif1_exitの場合、pcに対する代入アクションは「pc:=6」である。よってこの場合はステップ１８０８を実行する。
【０１１５】  中間物等価性証明部１１４は、上記falseイベントのガードを分岐条件として持つ、if文コードを作成する（ステップ１８０６）。例えば図９Ａ〜Ｃのイベントloop1_falseの場合、コード１００４に相当するコードを生成する。
【０１１６】  中間物等価性証明部１１４は、上記falseイベントにおいて、上記カウンタ変数に代入される値のラベルへジャンプするgoto文コードを作成し、上記if文コードの処理として追加する（ステップ１８０７）。例えば図９Ａ〜Ｃにおけるイベントloop1_falseの場合、カウンタ変数pcに代入される値は７である。この場合、コード１００３のgoto文に相当するコードを生成する。
【０１１７】  中間物等価性証明部１１４は、上記取得したイベントの上記カウンタ変数を更新するアクションにおいて、上記カウンタ変数に代入している番号のラベルへジャンプする、goto文のコードを作成する（ステップ１８０８）。図９Ａ〜Ｃのイベントif1_exitの場合、カウンタ変数pcに代入している番号は６であるため、コード１００５に相当するコードを生成する。
【０１１８】  中間物等価性証明部１１４は、上記取得したイベントのアクションを、当該プログラミング言語のコードに変換する。上記変換ルールの例は、図１５に示す通りである（ステップ１８０９）。
【０１１９】  中間物等価性証明部１１４は、ステップ１８０２にて取得したイベントのガードにて制約しているカウンタ変数の値を、上記ステップで作成したコードの先頭行に、ラベルとして付与する。ただし、INITIALIZATIONイベントの場合はガードを含まないため、０をラベルとして付与する（ステップ１８１０）。例えば図９Ａ〜Ｃのイベントincの場合、ガード９０１にて制約しているカウンタ変数pcの値は３である。よって、図１０に示す通り、コード１００２にラベル２を付与している。
【０１２０】  中間物等価性証明部１１４は、上記Scheduledモデルに含まれるイベントのうち未処理のイベントがあるかを確認する。未処理のイベントがある場合はステップ１８０２に戻る。全てのイベントを処理済みの場合は、ステップ１８１２を実行する（ステップ１８１１）。
【０１２１】  中間物等価性証明部１１４は、Flattenedコード保持部１０７から、図１４Ａ〜Ｃに示した手順で作成した、上記Scheduledモデルに対応する生成済みFlattenedコードを取得し、上記ステップにて作成したコードと比較する（ステップ１８１２）。
【０１２２】  中間物等価性証明部１１４は、上記生成済みFlattenedコードと、上記作成したコードが一致する場合、ステップ１８１４を実行する。一致しない場合、ステップ１８１５を実行する（ステップ１８１３）。
【０１２３】  中間物等価性証明部１１４は、等価性証明成功を出力し、証明結果として中間物証明結果保持部１１５に登録する（ステップ１８１４）。中間物等価性証明部１１４は、等価性証明失敗を出力し、証明結果として中間物証明結果保持部１１５に登録する（ステップ１８１５）。
【０１２４】  図１９はコード等価性証明部の手順例を示すフローチャートである。以下に示す処理は、ソースコード生成装置２０１の備えるＣＰＵ２０２が、メモリ２０３で実行するプログラムによって実現される。そしてこのプログラムは、以下に説明される各種の動作を行うためのコードから構成されている。
【０１２５】  ＣＰＵ２０２は、コード等価性証明部１１６を実行することによって、Flattenedコード保持部１０７からFlattenedコードを取得し、図２０Ａ、Ｂに示すgoto変換処理にてコード変換を行う（ステップ１９０１）。
【０１２６】  コード等価性証明部１１６は、Targetコード保持部１０８から、図１６Ａ、Ｂに示した手順で作成した、上記Flattenedコードに対応する生成済みTargetコードを取得し、上記ステップ１９０１にて作成したコードと比較する（ステップ１９０２）  コード等価性証明部１１６は、上記生成済みTargetコードと、上記作成したコードが一致する場合、ステップ１９０４を実行する。一致しない場合、ステップ１９０５を実行する（ステップ１９０３）。
【０１２７】  コード等価性証明部１１６は、等価性証明成功を出力し、証明結果としてコード証明結果保持部１１７に登録する（ステップ１９０４）。コード等価性証明部１１６は、等価性証明失敗をを出力し、証明結果としてコード証明結果保持部１１７に登録する（ステップ１９０５）。
【０１２８】  図２０Ａ、Ｂはgoto変換処理の手順例を示すフローチャートである。以下に示す処理は、ソースコード生成装置２０１の備えるＣＰＵ２０２が、メモリ２０３で実行するプログラムによって実現される。そしてこのプログラムは、以下に説明される各種の動作を行うためのコードから構成されている。
【０１２９】  ＣＰＵ２０２は、コード等価性証明部１１６を実行することによって、入力されたFlattenedコードの未処理の行のうち、先頭行を取得する（ステップ２００１）。
【０１３０】  コード等価性証明部１１６は、ステップ２００１で取得した取得行の種類によって、以下手順を実行する。上記取得行が、if文コードの場合、ステップ２００４を実行する。上記取得行が、代入文コードの場合、ステップ２００３を実行する（ステップ２００２）。
【０１３１】  コード等価性証明部１１６は、代入文コードからなる上記取得行を、そのまま代入文コードとして記述する（ステップ２００３）。
【０１３２】  コード等価性証明部１１６は、上記Flattenedコードの中に、取得したif文コードへとジャンプするgoto文コードが存在するかを確認する。上記のようなgoto文コードが存在する場合は、ステップ２００５を実行する。存在しない場合は、ステップ２００８を実行する（ステップ２００４）。
【０１３３】  コード等価性証明部１１６は、取得したif文コードの分岐条件から、否定を除去した条件をループ条件として持つ、while文コードを作成する（ステップ２００５）。図１０を例にとると、if文コード１００３から、図１１のwhile文コード１１０４を作成する。
【０１３４】  コード等価性証明部１１６は、上記Flattenedコードにおいて、上記取得したif文コードと、そのif文コードへとジャンプするgoto文コードの間にあるコードに、本goto変換処理を再帰適用する（ステップ２００６）。図１０の例では、if文コード１００３から、goto文コード１００６までの間のコードに再帰適用する。
【０１３５】  コード等価性証明部１１６は、上記再帰適用によって作成したコードを、ステップ２００５で作成した上記while文コードの処理として記述する（ステップ２００７）。
【０１３６】  コード等価性証明部１１６は、取得したif文コードの分岐条件から、否定を除去した条件を分岐条件として持つ、if文コードを作成する（ステップ２００８）。図１０の例では、if文コード１００４から、図１１のif文コード１１０３を作成する。
【０１３７】  コード等価性証明部１１６は、上記Flattenedコードにおいて、上記取得したif文コードから、そのif文コードの処理に含まれるgoto文コードによってジャンプする先の行から１を引いた行にあるgoto文コードまでの間にあるコードに対して、本goto変換処理を再帰適用する（ステップ２００９）。図１０の例では、if文コード１００４から、goto文コード１００５までの間のコードに再帰適用する。
【０１３８】  コード等価性証明部１１６は、上記再帰適用によって作成したコードを、ステップ２００８で作成した上記if文コードの処理として記述する（ステップ２０１０）。
【０１３９】  コード等価性証明部１１６は、上記取得したif文コードの処理に含まれるgoto文コードによってジャンプする先の行から１を引いた行にあるgoto文コードを、else文コードとして記述する（ステップ２０１１）。図１０の例では、goto文コード１００５から、図１１のelse文コード１１０７を作成する。
【０１４０】  コード等価性証明部１１６は、ステップ２０１１でelse文コードに変換したgoto文コードについて、上記goto文コードから、上記goto文にてジャンプする先の行までの間にあるコードに対して、本goto変換処理を再帰適用する（ステップ２０１２）。図１０の例では、goto文コード１００５から、コード１００６までの間のコードに再帰適用する。
【０１４１】  コード等価性証明部１１６は、上記再帰適用によって作成したコードを、ステップ２０１１で作成した上記else文コードの処理として記述する（ステップ２０１３）。
【０１４２】  以上、本実施例においては、ソースコード生成装置と、ソースコード証明装置を別個の装置としたが、それぞれの機能を一つの装置にて実現してもよい。
【０１４３】  このように、本実施形態におけるソースコード生成装置によれば、ソフトウェア仕様の正しさを形式的に証明した形式モデルから、ソースコードを生成する際において、制御構造を含む形式モデルであるScheduledモデルと、if分岐やdoループの代わりにgoto文を使用したソースコードであるFlattenedコードを生成する。上記Scheduledモデルと上記Flattenedコードは、上記Restrictedモデルと上記Targetコードとの制御構造の有無に関する差異や、言語上の差異を橋渡しする役割を担う。つまり、上記生成元の形式モデルと上記Scheduledモデルの詳細化関係、上記Scheduledモデルと上記Flattenedコードの等価性、および上記Flattenedコードと上記生成ソースコードの等価性を証明することで、その結果、生成したソースコードが、生成元の形式モデルが表す仕様を詳細化した結果であることを証明できるようになる。よって、生成したソースコードに誤りがある場合は、そのことを検出できるようになる。以上より、ソフトウェア不具合の削減を達成することができる。
【符号の説明】
【０１４４】  １０１    モデル編集部  １０２    Developedモデル保持部  １０３    モデル変換部  １０４    Restrictedモデル保持部  １０５    コード生成部  １０６    Scheduledモデル保持部  １０７    Flattenedコード保持部  １０８    Targetコード保持部  １０９    モデル詳細化証明部  １１０    詳細化証明結果保持部  １１１    スケジューラ保持部  １１２    スケジューラ編集部  １１３    スケジューラ検査部  １１４    中間物等価性証明部  １１５    中間物証明結果保持部  １１６    コード等価性証明部  １１７    コード証明結果保持部  １１８    中間物生成部。
【図１】
2015087409.tif 000003
【図２】
2015087409.tif 000004
【図３】
2015087409.tif 000005
【図４Ａ】
2015087409.tif 000006
【図４Ｂ】
2015087409.tif 000007
【図５】
2015087409.tif 000008
【図６Ａ】
2015087409.tif 000009
【図６Ｂ】
2015087409.tif 000010
【図７】
2015087409.tif 000011
【図８】
2015087409.tif 000012
【図９Ａ】
2015087409.tif 000013
【図９Ｂ】
2015087409.tif 000014
【図９Ｃ】
2015087409.tif 000015
【図１０】
2015087409.tif 000016
【図１１】
2015087409.tif 000017
【図１２】
2015087409.tif 000018
【図１３Ａ】
2015087409.tif 000019
【図１３Ｂ】
2015087409.tif 000020
【図１３Ｃ】
2015087409.tif 000021
【図１４Ａ】
2015087409.tif 000022
【図１４Ｂ】
2015087409.tif 000023
【図１４Ｃ】
2015087409.tif 000024
【図１５】
2015087409.tif 000025
【図１６Ａ】
2015087409.tif 000026
【図１６Ｂ】
2015087409.tif 000027
【図１７】
2015087409.tif 000028
【図１８Ａ】
2015087409.tif 000029
【図１８Ｂ】
2015087409.tif 000030
【図１９】
2015087409.tif 000031
【図２０Ａ】
2015087409.tif 000032
【図２０Ｂ】
2015087409.tif 000033
【国際調査報告】
2015087409.tif 000034
2015087409.tif 000035
2015087409.tif 000036