(57)【要約】【課題】プログラム中で間違った動作をする箇所の発見や原因調査のために、動作の異常を起こす範囲を特定するとともに異常発生の直前状態をデバッガ上で自動的に再現する。【解決手段】あらかじめ形式的に記述しておいた仕様（例えばメソッドの事前条件と事後条件）に従って、プログラムの動作状況を自動的に検証、プログラム内の誤っている箇所の範囲、つまり挙動を確認すべき範囲を自動的に絞り込む。より詳細には、メソッドの表明に関して注釈で事前条件と事後条件を定まった形式で記述しておき、その表明注釈を解析する表明注釈解析部４と、メソッドを表明ごとにシンボリックデバッガ３に実行させる実行制御部５と、実行結果が事前条件又は事後条件を満たすか否かを評価するデバッグ範囲特定部６と、を有する。【選択図】図１
2008210059.tif 000002
【特許請求の範囲】
【請求項１】
各メソッドの事前条件及び事後条件が記述された表明注釈が付与されたプログラムリストのデバッグを支援する情報処理装置であって、
デバッグ対象の表明注釈付きプログラムリストの表明注釈を解析する表明注釈解析手段と、
前記プログラムリストの有する各メソッドの開始時点及び終了時点にブレークポイントを置き、該ブレークポイントにて、プログラムの実行の停止及び再開のいずれか一方をシンボリックデバッガにさせる実行制御手段と、
前記表明注釈解析手段による解析によって得られた各メソッドの事前条件及び事後条件に基づき、前記各メソッドの表明ごとに前記事前条件及び事後条件の真偽値を得るデバッグ範囲特定手段と、を有し、
前記実行制御手段は、前記ブレークポイントにて、前記デバッグ範囲特定手段に、前記各メソッドの表明ごとに前記事前条件及び事後条件の真偽値を評価させ、
前記デバッグ範囲特定手段は、呼出メソッドから呼び出されたメソッドの、ある表明の事前条件の評価結果が偽であれば、デバッグ範囲を、前記呼出メソッドの開始時点から前記表明にて前記呼び出されたメソッドを呼び出す時点までに特定し、
呼出メソッドから呼び出されたメソッドの、ある表明の事後条件の評価結果が偽であれば、デバッグ範囲を、前記表明にて前記呼び出されたメソッドの開始時点から終了時点までに特定することを特徴とする情報処理装置。
【請求項２】
前記実行制御手段は、
制御の開始時点から、実行制御の履歴を保持し、
前記デバッグ範囲特定手段により前記各メソッドのある表明にて前記事前条件及び事後条件のいずれか一方の真偽値の評価結果が偽であると評価されたときに、前記実行制御の履歴を参照して、評価結果が偽であると評価された前記表明にてメソッドを開始する時点の状態を再現することを特徴とする請求項１記載の情報処理装置。
【請求項３】
各メソッドの事前条件及び事後条件が記述された表明注釈が付与されたプログラムリストのデバッグを支援するデバッグ支援方法であって、
デバッグ対象の表明注釈付きプログラムリストの表明注釈を解析する表明注釈解析手順と、
前記プログラムリストの有する各メソッドの開始時点及び終了時点にブレークポイントを置くブレークポイント設定手順と、
あるメソッドの開始時点の前記ブレークポイントから前記メソッドのある表明にてプログラムの実行コードをシンボリックデバッガに実行させ、終了時点の前記ブレークポイントで停止させる実行制御手順と、
該実行制御手順によりプログラムの実行を停止させたタイミングで前記メソッドの表明の評価を行う表明評価手順と、
該表明評価手順による、前記表明の事前条件の評価結果が偽であれば、前記メソッドの呼出メソッドの開始時点から前記表明にて前記メソッドを呼び出す時点まで、
前記表明評価手段による、前記表明の事後条件の評価結果が偽であれば、前記表明にて呼び出された前記メソッドの開始時点から終了時点まで、にデバッグ範囲を特定するデバッグ範囲特定手順と、
を有することを特徴とするデバッグ支援方法。
【請求項４】
前記実行制御手順の実行の後に、実行制御の履歴を記憶する記憶手順を行い、
前記表明評価手順により、ある表明の事前条件又は事後条件のいずれか一方の評価結果が偽であると評価されたときに、前記記憶手順により記憶された前記実行制御の履歴を参照して評価が偽であると評価された前記表明にてメソッドを開始する時点の状態を再現する再現手順を行うことを特徴とする請求項３記載のデバッグ支援方法。
【請求項５】
各メソッドの事前条件及び事後条件が記述された表明注釈が付与されたプログラムリストのデバッグを支援する情報処理装置を、
デバッグ対象の表明注釈付きプログラムリストの表明注釈を解析する表明注釈解析手段と、
前記プログラムリストの有する各メソッドの開始時点及び終了時点にブレークポイントを置き、該ブレークポイントにて、プログラムの実行の停止及び再開のいずれか一方をシンボリックデバッガにさせる実行制御手段と、
前記表明注釈解析手段による解析によって得られた各メソッドの事前条件及び事後条件に基づき、前記各メソッドの表明ごとに前記事前条件及び事後条件の真偽値を得るデバッグ範囲特定手段と、として機能させ、
前記実行制御手段は、前記ブレークポイントにて、前記デバッグ範囲特定手段に、前記各メソッドの表明ごとに前記事前条件及び事後条件の真偽値を評価させ、
前記デバッグ範囲特定手段は、呼出メソッドから呼び出されたメソッドの、ある表明の事前条件の評価結果が偽であれば、デバッグ範囲を、前記呼出メソッドの開始時点から前記表明にて前記呼び出されたメソッドを呼び出す時点までに特定し、
呼出メソッドから呼び出されたメソッドの、ある表明の事後条件の評価結果が偽であれば、デバッグ範囲を、前記表明にて前記呼び出されたメソッドの開始時点から終了時点までに特定することを特徴とするプログラム。
【請求項６】
前記実行制御手段は、
制御の開始時点から、実行制御の履歴を保持し、
前記デバッグ範囲特定手段により前記各メソッドのある表明にて前記事前条件及び事後条件のいずれか一方の真偽値の評価結果が偽であると評価されたときに、前記実行制御の履歴を参照して、評価結果が偽であると評価された前記表明にてメソッドを開始する時点の状態を再現することを特徴とする請求項５記載のプログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、情報処理装置、デバッグ支援方法及びプログラムに関する。
【背景技術】
【０００２】
プログラムをデバッグする場合、何らかの障害が報告されたことに対して、同じ現象をデバッガ上で再現してプログラムの挙動を解析することで原因を調査し、対処法を考えていくのが通常のやり方であった。
【０００３】
例えば、特許文献１（特に段落００２７−００３０等）を参照すると、所定の内部イベント後にその成立条件とデバッガの操作が記述されたカスタムハンドラとを登録したイベントテーブルを持ち、イベントテーブルの各内部イベント成立条件とデバッガの状態変数とを監視し、内部イベント成立条件が成立しているかを調べ、内部イベント成立条件が成立したときに、該内部イベントに対応してイベントテーブルに登録されているカスタムハンドラを起動するデバッガに関する技術が開示されている。
【０００４】
また、例えば、特許文献２を参照すると、ユーザが指定した制御の流れ及び変数値と、デバッガで実行した制御の流れ及び変数値とを比較して、プログラム情報の検証を行う技術が開示されている。
【０００５】
しかし、報告された現象の原因をデバッガで調べるためには、障害発生の少し前の時点でデバッガを停止状態にする必要があるが、それは容易ではない。
【０００６】
なぜならば、デバッガ上ではいったん実行時エラーが発生してしまったプログラムを、エラー発生の前の状態に逆戻りさせることができないからである。
【０００７】
実行時エラーが発生する主要な原因は、そのエラーが発生したメソッド呼出の初期状態や、そのメソッド内で既に実行されたステートメントの作用が想定外となっていることである。この場合、Ｐｒｏｇｒａｍｍｉｎｇ  Ｂｙ  Ｃｏｎｔｒａｃｔの考え方（例えば、非特許文献１参照）を応用し、エラー発生に関与するメソッドの事前条件や事後条件を明確化することで、想定外の事態を引き起こすようなメソッドの使い方を予防することができる。
【０００８】
実行時エラーを標的にデバッグする代わりに、事前条件や事後条件へ違反する状況を標的にしてデバッグする場合、標的の直前でデバッガを自動停止させることは、不可能ではなくなる。それを実現したのが本発明である。
【特許文献１】特開平１１−３０６０４２号公報
【特許文献２】特開平０２−３１０６３７号公報
【非特許文献１】Ｂｅｒｔｒａｎｄ  Ｍｙｅｒ著、二木厚吉監訳『オブジェクト指向入門』アスキー出版局、１９９０年１１月２１日、ｐｐ．１５３−１６８
【発明の開示】
【発明が解決しようとする課題】
【０００９】
上記従来技術は、デバッグを効率化するという点で、本発明と目的とする方向が一致するものではあるが、次のような問題点があった。
【００１０】
プログラムのデバッグ時に、誤った動作をしている箇所を見つけ出すにはステップ実行によってプログラムの挙動を逐一確認するという手間のかかる作業が必要だった。
【００１１】
そこで本発明は、上記従来技術の問題点に鑑み、プログラム中で間違った動作をする箇所の発見や原因調査のために、動作の異常を起こす範囲を特定するとともに異常発生の直前状態をデバッガ上で自動的に再現することを可能にすることを目的とする。
【課題を解決するための手段】
【００１２】
上記目的を達成するための請求項１記載の発明は、各メソッドの事前条件及び事後条件が記述された表明注釈が付与されたプログラムリストのデバッグを支援する情報処理装置であって、デバッグ対象の表明注釈付きプログラムリストの表明注釈を解析する表明注釈解析手段と、前記プログラムリストの有する各メソッドの開始時点及び終了時点にブレークポイントを置き、該ブレークポイントにて、プログラムの実行の停止及び再開のいずれか一方をシンボリックデバッガにさせる実行制御手段と、前記表明注釈解析手段による解析によって得られた各メソッドの事前条件及び事後条件に基づき、前記各メソッドの表明ごとに前記事前条件及び事後条件の真偽値を得るデバッグ範囲特定手段と、を有し、前記実行制御手段は、前記ブレークポイントにて、前記デバッグ範囲特定手段に、前記各メソッドの表明ごとに前記事前条件及び事後条件の真偽値を評価させ、前記デバッグ範囲特定手段は、呼出メソッドから呼び出されたメソッドの、ある表明の事前条件の評価結果が偽であれば、デバッグ範囲を、前記呼出メソッドの開始時点から前記表明にて前記呼び出されたメソッドを呼び出す時点までに特定し、呼出メソッドから呼び出されたメソッドの、ある表明の事後条件の評価結果が偽であれば、デバッグ範囲を、前記表明にて前記呼び出されたメソッドの開始時点から終了時点までに特定することを特徴とする情報処理装置である。
【００１３】
請求項２記載の発明は、請求項１記載の情報処理装置において、前記実行制御手段は、制御の開始時点から、実行制御の履歴を保持し、前記デバッグ範囲特定手段により前記各メソッドのある表明にて前記事前条件及び事後条件のいずれか一方の真偽値の評価結果が偽であると評価されたときに、前記実行制御の履歴を参照して、評価結果が偽であると評価された前記表明にてメソッドを開始する時点の状態を再現することを特徴とする。
【００１４】
請求項３記載の発明は、各メソッドの事前条件及び事後条件が記述された表明注釈が付与されたプログラムリストのデバッグを支援するデバッグ支援方法であって、デバッグ対象の表明注釈付きプログラムリストの表明注釈を解析する表明注釈解析手順と、前記プログラムリストの有する各メソッドの開始時点及び終了時点にブレークポイントを置くブレークポイント設定手順と、あるメソッドの開始時点の前記ブレークポイントから前記メソッドのある表明にてプログラムの実行コードをシンボリックデバッガに実行させ、終了時点の前記ブレークポイントで停止させる実行制御手順と、該実行制御手順によりプログラムの実行を停止させたタイミングで前記メソッドの表明の評価を行う表明評価手順と、該表明評価手順による、前記表明の事前条件の評価結果が偽であれば、前記メソッドの呼出メソッドの開始時点から前記表明にて前記メソッドを呼び出す時点まで、前記表明評価手段による、前記表明の事後条件の評価結果が偽であれば、前記表明にて呼び出された前記メソッドの開始時点から終了時点まで、にデバッグ範囲を特定するデバッグ範囲特定手順と、を有することを特徴とするデバッグ支援方法である。
【００１５】
請求項４記載の発明は、請求項３記載のデバッグ支援方法において、前記実行制御手順の実行の後に、実行制御の履歴を記憶する記憶手順を行い、前記表明評価手順により、ある表明の事前条件又は事後条件のいずれか一方の評価結果が偽であると評価されたときに、前記記憶手順により記憶された前記実行制御の履歴を参照して評価が偽であると評価された前記表明にてメソッドを開始する時点の状態を再現する再現手順を行うことを特徴とする。
【００１６】
請求項５記載の発明は、各メソッドの事前条件及び事後条件が記述された表明注釈が付与されたプログラムリストのデバッグを支援する情報処理装置を、デバッグ対象の表明注釈付きプログラムリストの表明注釈を解析する表明注釈解析手段と、前記プログラムリストの有する各メソッドの開始時点及び終了時点にブレークポイントを置き、該ブレークポイントにて、プログラムの実行の停止及び再開のいずれか一方をシンボリックデバッガにさせる実行制御手段と、前記表明注釈解析手段による解析によって得られた各メソッドの事前条件及び事後条件に基づき、前記各メソッドの表明ごとに前記事前条件及び事後条件の真偽値を得るデバッグ範囲特定手段と、として機能させ、前記実行制御手段は、前記ブレークポイントにて、前記デバッグ範囲特定手段に、前記各メソッドの表明ごとに前記事前条件及び事後条件の真偽値を評価させ、前記デバッグ範囲特定手段は、呼出メソッドから呼び出されたメソッドの、ある表明の事前条件の評価結果が偽であれば、デバッグ範囲を、前記呼出メソッドの開始時点から前記表明にて前記呼び出されたメソッドを呼び出す時点までに特定し、呼出メソッドから呼び出されたメソッドの、ある表明の事後条件の評価結果が偽であれば、デバッグ範囲を、前記表明にて前記呼び出されたメソッドの開始時点から終了時点までに特定することを特徴とするプログラムである。
【００１７】
請求項６記載の発明は、請求項５記載のプログラムにおいて、前記実行制御手段は、制御の開始時点から、実行制御の履歴を保持し、前記デバッグ範囲特定手段により前記各メソッドのある表明にて前記事前条件及び事後条件のいずれか一方の真偽値の評価結果が偽であると評価されたときに、前記実行制御の履歴を参照して、評価結果が偽であると評価された前記表明にてメソッドを開始する時点の状態を再現することを特徴とする。
【発明の効果】
【００１８】
本発明によれば、プログラム中で間違った動作をする箇所の発見や原因調査のために、動作の異常を起こす範囲を特定するとともに異常発生の直前状態をデバッガ上で自動的に再現することが可能になる。
【発明を実施するための最良の形態】
【００１９】
以下、本発明の好適な実施の形態について、図面を参照して説明する。なお、以下では、例として、Ｊａｖａ（登録商標）プログラムのデバッグを行う場合について説明するが、言うまでもなく、本発明は、本例に限定されるものではない。
【００２０】
まず、本実施形態の構成について説明する。図１を参照すると、本実施形態の機能構成が示されている。本実施形態に該当する情報処理装置１は、実行コードコンパイラ２と、シンボリックデバッガ３と、表明注釈解析部４と、実行制御部５と、デバッグ範囲特定部６と、を有する構成である。以下、これらの各構成要素について説明する。
【００２１】
実行コードコンパイラ２は、Ｊａｖａ（登録商標）のコンパイラである。一般的に、Ｃ言語やＪａｖａ（登録商標）言語などのプログラミングに通常使用されているコンパイラである。
【００２２】
シンボリックデバッガ３は、Ｊａｖａ（登録商標）のシンボリックデバッガである。一般的に、Ｃ言語やＪａｖａ（登録商標）言語などのプログラミングに通常使用されているシンボリックデバッガである。
【００２３】
表明注釈解析部４は、ソースコード内の関数に付与された表明に関する注釈を解析し、デバッガ上で評価可能な式を生成する。
【００２４】
実行制御部５は、シンボリックデバッガ３を制御し、事前条件と事後条件をチェックすべきステップで停止して、デバッグ範囲特定部６に解析処理を指示する。
【００２５】
デバッグ範囲特定部６は、事前条件と事後条件の成立状況に基づいてバグの存在する範囲を特定する。
【００２６】
次に、上記の構成を有する本実施形態の動作について説明する。
【００２７】
本実施形態においてデバッグ対象とするＪａｖａ（登録商標）プログラムのソースコードには、各々の関数（メソッド）についての表明（事前条件、事後条件）が注釈として記述されているものとする。
【００２８】
なお、事前条件、事後条件の記述には、ＪＭＬ（Ｊａｖａ（登録商標）  Ｍｏｄｅｌｉｎｇ  Ｌａｎｇｕａｇｅ）等の表明記述言語を用いる。ＪＭＬは、アイオワ州立大学を中心として制定された言語であり、事前条件と事後条件だけでなく、プログラムの振る舞い・仕様を記述するための様々な記法が提供されている。ＪＭＬに関しては、次のＵＲＬから情報を得ることができる。
ＵＲＬ：  http://www.cs.iastate.edu/~leavens/JML/
【００２９】
以下、図１を参照して説明する。まず、実行コードコンパイラ２（Ｊａｖａ（登録商標）コンパイラ）は、デバッグ対象のプログラムの、表明注釈付きソースコード１０をバイトコードにコンパイルする。
【００３０】
次に、シンボリックデバッガ３は、デバッグ対象のプログラムのバイトコードである、実行コード１１を読み込み、そのプログラムを実行待機状態におく。
【００３１】
一方で、表明注釈解析部４は、表明注釈付きソースコード１０を解析し、各メソッドの表明注釈を抽出し、事前条件や事後条件の式をデバッガ上で評価可能な形式（各メソッドの事前条件と事後条件１３）に変換してデバッグ範囲特定部６へ渡す。図２は、本動作の一例を示す図である。図２において、本動作は、上段のプログラムリストから、下段の条件式等に変換するものである。
【００３２】
また、一方で、表明注釈解析部４は、実行制御部５に、検証対象とする関数名１２を渡して、検証させる。
【００３３】
具体的には、実行制御部５は、シンボリックデバッガ３に対して表明注釈の付与された関数の開始時点、終了時点にブレークポイントを設定して、プログラムの実行を開始させる。
【００３４】
また、実行制御部５は、関数の開始時点のブレークポイントでプログラムが停止した際に、デバッグ範囲特定部６にメソッド呼出のコンテクストを解析させた後、シンボリックデバッガ３にプログラムの実行を再開させる。
【００３５】
また、実行制御部５は、関数の終了時点のブレークポイントでプログラムが停止した際に、デバッグ範囲特定部６にメソッド呼出のコンテクストを解析させた後、シンボリックデバッガ３にプログラムの実行を再開させる。
【００３６】
また、実行制御部５は、任意の停止時点の状態を再現することができるように、開始時点からの実行制御の履歴を保存する。
【００３７】
なお、上記の実行制御部５の動作は、さらに詳細には、プログラムの実行を停止させたタイミングで表明の評価をデバッグ範囲特定部６に指示し、また、シンボリックデバッガ３に指示して次に検証すべき行までプログラムの実行を進めて停止させるものである。
【００３８】
デバッグ範囲特定部６は、個々のメソッド実行のコンテクストにおいて、メソッドの呼出時における事前条件、終了時における事後条件を評価し、条件への違反があった場合には、当該コンテクストを図３の手順で解析し、条件違反の原因として疑うべき範囲をソースコード中で特定し、その範囲にマーカーを付与する。デバッグ範囲特定部６の出力は、デバッグ範囲マーカー１４となる。
【００３９】
図３は、メソッド実行のコンテクストを解析する手順を示すフローチャート図である。まず、あるメソッド（ｍ）呼出の事前条件の評価結果の真偽値を調べる（ステップＳ３１）。偽なら、処理を行わない。
【００４０】
真ならば、メソッドｍ内で次の（初めて実行する場合は、最初の）ステートメント（Ｓ）を実行する（ステップＳ３２）。
【００４１】
ステートメントＳの事前条件の評価結果の真偽値を調べる（ステップＳ３３）。偽であれば、デバッグ対象は、メソッドｍ内のステートメントＳより前の範囲、又は、ステートメントＳの呼出先メソッドの仕様である（ステップＳ３４）。デバッグ範囲特定部６は、これらの範囲にマーカーを付与する。
【００４２】
ステートメントＳの事前条件の評価結果が、真であれば、次に、ステートメントＳの事後条件の評価結果の真偽値を調べる（ステップＳ３５）。真であれば、ステップＳ３２へ戻り、次のステートメントを実行する。偽であれば、デバッグ対象は、ステートメントＳの呼出先メソッドである（ステップＳ３６）。デバッグ範囲特定部６は、この範囲にマーカーを付与する。
【００４３】
上記、図３を参照して説明したメソッド実行のコンテクストを解析する手順の説明において明らかになったように、条件違反のパターンとしては、図４及び図５に示す２種類の状況が起こりうる。
【００４４】
あるメソッド呼出において、事前条件が成立しない場合は、そのメソッドの想定外の使い方をしているわけであり、呼出側に誤りがあると考えられる。図４は、この場合を概念的に示す図である。デバッグ範囲特定部６は、呼出メソッドの開始時点にデバッグ開始のポイントを置き、メソッド実行にエラーがあった事前条件のところまでにマーカーを付与する。
【００４５】
また、あるメソッド呼出の事前条件が成立していて、事後条件が成立しない場合、想定内の使い方であるのに期待通りの処理結果が得られていないわけであるから、そのメソッドに誤りがあると考えられる。図５は、この場合を概念的に示す図である。デバッグ範囲特定部６は、ある事前条件で呼び出されたメソッドの開始時点にデバッグ開始のポイントを置き、呼出メソッドに返値を返すところまでにマーカーを付与する。
【００４６】
さて、デバッグ範囲特定部６にて条件違反が検出された場合、実行制御部５は、プログラムを中断／再実行し、前回の実行履歴を利用して、条件違反の検出されるコンテクストの開始時点まで実行を進めて停止し、ユーザにデバッグ作業を委ねる。
【００４７】
以上で、本実施形態の説明を終え、次に、本実施形態の効果について述べる。
【００４８】
本実施形態によれば、想定していた仕様（事前条件、事後条件）に反する間違った動作が自動的に検出され、その現象の発生する直前の状態がデバッガ上で自動的に再現されることにより、ユーザはプログラムを効率良くデバッグできる。
【００４９】
なお、本発明は、下記のようにしても実施可能である。
【００５０】
すなわち、上記実施形態では、デバッグ範囲特定部６にて条件違反が検出された場合に、条件違反を最初に見つけた時点で実行を中断してしまうが、上記実施形態において、プログラム実行を中断せずに実行を継続し、実行制御部５によるシンボリックデバッガ３に対する、表明注釈の付与された関数の開始時点と終了時点にブレークポイントを設定してプログラムの実行を開始又は再開させる処理と、デバッグ範囲特定部６による個々のメソッド実行のコンテクストにおいてメソッドの呼出時における事前条件と終了時における事後条件の評価処理と、を繰り返して行う。このように構成することによって、可能な限り多くのデバッグ対象候補を収集することができる。
【００５１】
また、さらに、上記実施形態では、デバッグ範囲特定部６にて条件違反が検出された場合に再実行する、再起動処理においては、最初に見つけたデバッグ対象箇所を再現するが、他のデバッグ対象範囲にもそれぞれブレークポイントを設定するようにする。このように構成することによって、さらに細かくデバッグ範囲の特定が可能になる。
【産業上の利用可能性】
【００５２】
メソッドや関数を持つプログラミング言語によるプログラム開発であれば、事前条件と事後条件によるＰｒｏｇｒａｍｍｉｎｇ  Ｂｙ  Ｃｏｎｔｒａｃｔを導入できるため、本発明の構成が適用できる。
【図面の簡単な説明】
【００５３】
【図１】本発明による実施形態の機能構成を示すブロック図である。
【図２】本発明による実施形態の表明注釈解釈部４の作用を説明するための図である。
【図３】本発明による実施形態の、メソッド実行のコンテクストを解析する手順を示す図である。
【図４】本発明による実施形態の、条件違反の類型を説明するための図（その１）である。
【図５】本発明による実施形態の、条件違反の類型を説明するための図（その２）である。
【符号の説明】
【００５４】
１    情報処理装置
２    実行コードコンパイラ
３    シンボリックデバッガ
４    表明注釈解析部
５    実行制御部
６    デバッグ範囲特定部
１０    表明注釈付きソースコード
１１    実行コード
１２    検証対象とする関数名
１３    各メソッドの事前条件と事後条件
１４    デバッグ範囲マーカー
【図１】
2008210059.tif 000003
【図２】
2008210059.tif 000004
【図３】
2008210059.tif 000005
【図４】
2008210059.tif 000006
【図５】
2008210059.tif 000007