(57)【要約】【課題】デバッグ作業においてメモリ値を適正に設定し最適なデバッグを行うことができるデバッグ装置、デバッグ方法、及びデバッグプログラムを提供すること。【解決手段】デバッグ装置１は、プログラムの実行を一時停止させる停止手段２と、停止手段２により一時停止されたプログラムにおいて、所定のメモリ値を変更する変更手段３と、変更手段３により変更されたメモリ値が他のメモリ値の関係で適正であるか否かをモデル検査するモデル検査手段４と、を備えている。【選択図】図１
2013210736.tif 000002
【特許請求の範囲】
【請求項１】
プログラムの実行を一時停止させる停止手段と、
前記停止手段により一時停止されたプログラムにおいて、所定のメモリ値を変更する変更手段と、
前記変更手段により変更されたメモリ値が他のメモリ値の関係で適正であるか否かをモデル検査するモデル検査手段と、
を備える、ことを特徴とするデバッグ装置。
【請求項２】
請求項１記載のデバッグ装置において、
前記モデル検査手段は、前記プログラムの状態遷移図において、初期状態から任意状態への到達可能性を検査することで、前記変更手段により変更されたメモリ値が他のメモリ値の関係で適正であるか否かをモデル検査する、ことを特徴とするデバッグ装置。
【請求項３】
請求項１又は２記載のデバッグ装置であって、
前記モデル検査手段による検査結果を表示する表示手段を更に備える、ことを特徴とするデバッグ装置。
【請求項４】
請求項１乃至３のうちいずれか１項記載のデバッグ装置であって、
前記モデル検査手段は、前記変更手段により変更されたメモリ値が不適正であると判断したとき、適正なメモリ値を算出し提示する、ことを特徴とするデバッグ装置。
【請求項５】
プログラムの実行を一時停止させるステップと、
前記一時停止されたプログラムにおいて、所定のメモリ値を変更するステップと、
前記変更されたメモリ値が他のメモリ値の関係で適正であるか否かをモデル検査するステップと、
を含む、ことを特徴とするデバッグ方法。
【請求項６】
請求項５記載のデバッグ方法において、
前記プログラムの状態遷移図において、初期状態から任意状態への到達可能性を検査することで、前記変更されたメモリ値が他のメモリ値の関係で適正であるか否かをモデル検査する、ことを特徴とするデバッグ方法。
【請求項７】
請求項５又は６記載のデバッグ方法であって、
前記モデル検査による検査結果を表示するステップを更に含む、ことを特徴とするデバッグ方法。
【請求項８】
請求項５乃至７のうちいずれか１項記載のデバッグ方法であって、
前記変更されたメモリ値が不適正であると判断したとき、適正なメモリ値を算出し提示するステップを更に含む、ことを特徴とするデバッグ方法。
【請求項９】
プログラムの実行を一時停止させる処理と、
前記一時停止されたプログラムにおいて、所定のメモリ値を変更する処理と、
前記変更されたメモリ値が他のメモリ値の関係で適正であるか否かをモデル検査する処理と、
をコンピュータに実行させる、ことを特徴とするデバッグプログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、プログラムのデバッグを最適に実行できるデバッグ装置、デバッグ方法、及びデバッグプログラムに関するものである。
【背景技術】
【０００２】
プログラムの開発過程において、そのプログラムが設計者の意図通りに作られているか否か、また、誤っている場合にどの様に修正すべきかを調査する、いわゆるデバッグ作業が行われており、現代のプログラム開発に欠かせない作業となっている。また、そのデバッグ作業を行うためのツールとして、適正に行う様々なプログラムデバッガが知られている（例えば、特許文献１参照）。このプログラムデバッガは、プログラムを実行しつつ、プログラムを任意の時点で一時停止させ、メモリ値を確認・変更することで、上記デバッグを行っている。
【０００３】
ところで、プログラムデバッガを使用したデバッグ作業においては、一般に、誤りが生じそうな時点でプログラムを一時停止させ、誤りを引き起こしそうなメモリ値に変更し、プログラムを再開させるといった確認作業が行われる。
【先行技術文献】
【特許文献】
【０００４】
【特許文献１】特開平０４−３３３９３３号公報
【発明の概要】
【発明が解決しようとする課題】
【０００５】
このとき、その変更するメモリ値については、例えば、デバッグ作業を行う作業者の裁量などによって決められており、メモリ値が適正に設定されていない場合、そのデバッグ作業自体が不適正なものとなる虞がある。
【０００６】
本発明は、このような問題点を解決するためになされたものであり、デバッグ作業においてメモリ値を適正に設定し最適なデバッグを行うことができるデバッグ装置、デバッグ方法、及びデバッグプログラムを提供することを主たる目的とする。
【課題を解決するための手段】
【０００７】
上記目的を達成するための本発明の一態様は、プログラムの実行を一時停止させる停止手段と、前記停止手段により一時停止されたプログラムにおいて、所定のメモリ値を変更する変更手段と、前記変更手段により変更されたメモリ値が他のメモリ値の関係で適正であるか否かをモデル検査するモデル検査手段と、を備える、ことを特徴とするデバッグ装置である。
他方、上記目的を達成するための本発明の一態様は、プログラムの実行を一時停止させるステップと、前記一時停止されたプログラムにおいて、所定のメモリ値を変更するステップと、前記変更されたメモリ値が他のメモリ値の関係で適正であるか否かをモデル検査するステップと、を含む、ことを特徴とするデバッグ方法であってもよい。
また、上記目的を達成するための本発明の一態様は、プログラムの実行を一時停止させる処理と、前記一時停止されたプログラムにおいて、所定のメモリ値を変更する処理と、前記変更されたメモリ値が他のメモリ値の関係で適正であるか否かをモデル検査する処理と、をコンピュータに実行させる、ことを特徴とするデバッグプログラムであってもよい。
【発明の効果】
【０００８】
本発明によれば、デバッグ作業においてメモリ値を適正に設定し最適なデバッグを行うことができるデバッグ装置、デバッグ方法、及びデバッグプログラムを提供することができる。
【図面の簡単な説明】
【０００９】
【図１】本発明の一実施の形態に係るデバッグ装置の機能ブロック図である。
【図２】本発明の一実施の形態に係るデバッグ装置の概略的なシステム構成を示すブロック図である。
【図３】プログラムの一例を示す図である。
【図４】本発明の一実施の形態に係るデバッグ装置の処理フローを示すフローチャートである。
【発明を実施するための形態】
【００１０】
図１は、本発明の一実施の形態に係るデバッグ装置の機能ブロック図である。本実施の形態に係るデバッグ装置１は、プログラムの実行を一時停止させる停止手段２と、停止手段２により一時停止されたプログラムにおいて、所定のメモリ値を変更する変更手段３と、変更手段３により変更されたメモリ値が他のメモリ値の関係で適正であるか否かをモデル検査するモデル検査手段４と、を備えている。これにより、ユーザは、変更されたメモリ値が他のメモリ値の関係で適正であるか否かを判断できる。したがって、デバッグ作業においてメモリ値を適正に設定し最適なデバッグを行うことができる。
【００１１】
図２は、本発明の一実施の形態に係るデバッグ装置の概略的なシステム構成を示すブロック図である。本実施の形態に係るデバッグ装置１は、再生停止部１１と、変更部１２と、モデル検査部１３と、表示部１４と、を備えている。
【００１２】
再生停止部１１は、停止手段の一具体例であり、プログラムの実行を一時停止させ、あるいはプログラムを再生させる。再生停止部１１は、例えば、デバッグ作業において、誤りが生じそうな時点でプログラムを停止させる。また、再生停止部１１は、変更部１２により所定のメモリ値が変更された後、再度、プログラムを再生する。なお、再生停止部１１は、例えば、ユーザによる一時停止指示及び再生指示に応じて、上記プログラムを一時停止及び再生を行ってもよく、誤りが生じそうな時点で自動的に上記プログラムを一時停止及び再生を行ってもよい。
【００１３】
変更部１２は、変更手段の一具体例であり、再生停止部１１により一時停止されたプログラムにおいて所定のメモリ値を変更する。変更部１２は、例えば、ユーザの入力指示に基づいて再生停止部１１により一時停止されたプログラムにおいて所定のメモリ値を変更する。なお、ユーザは、例えば、キーボード、マウス、などの任意の入力装置１５を用いて、変更値を変更部１２に入力することができる。
【００１４】
表示部１４は、表示手段の一具体例であり、モデル検査部１３による検査結果を表示する。表示部１４は、例えば、液晶ディスプレイ装置や有機或いは無機ＥＬディスプレイ装置などにより構成され、文字、図形、グラフ、画像などの任意の情報を表示することができる。
【００１５】
なお、デバッグ装置１は、例えば、制御処理、演算処理等と行うＣＰＵ（Central Processing Unit）、ＣＰＵによって実行される制御プログラム、演算プログラム等が記憶されたＲＯＭ（Read Only Memory）、処理データ等を一時的に記憶するＲＡＭ（Random Access Memory）等からなるマイクロコンピュータを、中心にしてハードウェア構成されている。ＣＰＵ、ＲＯＭ、及びＲＡＭは、データバスなどを介して相互に接続されている。
【００１６】
ところで、従来、デバッグ作業において、プログラムを一時停止した状態でメモリ値を変更する場合、メモリ値を実際には起こり得ない値に変更してしまい、そのデバッグ作業自体が不適正なものとなる虞があった。
【００１７】
例えば、図３に示すように、あるメモリ値を指す変数ｘとｙを有するプログラムにおいて、６行目の時点でプログラムを一時停止させたとき、ｘ値が１、ｙ値が１である場合を想定する。ここで、デバッグ作業を行うためにｙ値を０に変更したとする。
【００１８】
このとき、合わせてｘ値をｘ≦０となる適当な値に変更しなければ、ｘとｙの組み合わせが実際には起こり得ない不適正なものになる。なぜならば、この時点でｙ値が０になるのは４行目のｙ＝０を通るときであり、４行目を通るには１行目のｘ＞０の判定で偽となる、すなわちｘ値がｘ≦０という条件が満たされなければならないからである。このことに気付かないまま、ｙ値だけを変更したデバッグ作業を行っても、そのような状況は実際には起こり得ないため、そのデバッグ作業は不適正なものとなる。
【００１９】
そこで、本実施の形態に係るデバッグ装置１において、モデル検査部１３は、変更部１２により変更された所定のメモリ値が他のメモリ値の関係で適正であるか否かをモデル検査する。これにより、ユーザは、上記検査結果を用いて、変更されたメモリ値が適正であるか否かを容易に判断できる。したがって、デバッグ作業においてメモリ値を適正に設定し最適なデバッグを行うことができる。
【００２０】
モデル検査部１３は、モデル検査手段の一具体例であり、モデル検査部１３は、例えば、プログラムの状態遷移図において、初期状態から任意状態への到達可能性を検査することで、変更部１２により変更されたメモリ値が他のメモリ値の関係で適正であるか否かをモデル検査する。モデル検査部１３は、プログラムを状態遷移図に見立て、モデル検査を実施することによって、プログラムの任意の時点における任意のメモリ値への到達可能性を検査することができる。
【００２１】
なお、モデル検査の詳細については、例えば、参考文献１（"Automatic verification of finite state concurrent systems using temporal logic", E.M. Clarke, E.A. Emerson, and A.P. Sistla, ACM Trans. on Programming Languages and Systems (TOPLAS), Volume 8 Issue 2, April 1986.）や、参考文献２（"形式手法によるC言語検証ツール「VARVEL」", 橋本 祐介, 徳岡 宏樹, 宮崎 義昭, NEC技報, Vol.60 No.2, 2007,）などに詳細な内容が開示されており、これを援用することができる。
【００２２】
モデル検査部１３は、変更部１２により変更されたメモリ値が不適正であると判断されたとき、適正なメモリ値を算出し、ユーザに提示する。モデル検査部１３は、例えば、変更部１２により変更されたメモリ値が適正であるか否かの検査結果や上記変更部１２により変更されたメモリ値が不適正であると判断されたときに適正なメモリ値を、表示部１４に表示させる。これにより、ユーザは、表示部１４の検査結果及び適正なメモリ値を参照してデバッグ作業を容易かつ適正に行うことができる。
【００２３】
モデル検査部１３は、変更部１２により変更されたメモリ値と他のメモリ値との組み合わせが実際に起こり得ず、適正でないと判断したとき、変更するメモリ値をプロパティとしたモデル検査を実行し、変更しないその他のメモリ値がどのような値であれば良いかを、モデル検査の結果として得られる反例により提示する。
【００２４】
モデル検査部１３は、これらのモデル検査により反例がないと判断した場合、いかなる条件下においてもこれらの条件を満たす組み合わせがない、すなわち、デバッグ作業を行う者が変更しようとしたメモリ値は、いかなる場合も実際には起こり得ない旨を提示する。
【００２５】
モデル検査部１３は、例えば、ＶＡＲＶＥＬやＣＢＭＣなどを用いて、Ｃ言語で書かれたプログラムを対象にモデル検査を実施する。なお、ＶＡＲＶＥＬやＣＢＭＣにおいては、プロパティの否定であるａｓｓｅｒｔをモデル検査により検証することができる。このため、プロパティの否定をａｓｓｅｒｔにすることで、プロパティの否定の否定、すなわちプロパティを検証することができる。メモリ値を変更する時点において、変更するメモリ値のプロパティを表す、変更するメモリ値の否定をａｓｓｅｒｔにする。また、変更するメモリ値と変更しないその他のメモリ値のプロパティを表す、変更するメモリ値と変更しないその他のメモリ値の否定をａｓｓｅｒｔにし、ＶＡＲＶＥＬやＣＢＭＣを実施する。
【００２６】
例えば、図３のようなプログラムにおいて、再生停止部１１が６行目の時点でプログラムを一時停止させたとき、ｘ値が１、ｙ値が１であったとする。ここで、ユーザが入力装置１５を介してｙ値に０を入力し、変更部１２がｙ値（メモリ値）を０に変更した場合に、モデル検査部１３は、変更部１２により変更されたそのメモリ値が他のメモリ値の関係で適正であるか否かをモデル検査する。
【００２７】
モデル検査部１３は、例えば、変更するメモリ値のプロパティを表す！（ｙ＝＝０）と、変更しないその他のメモリ値のプロパティを表す！（ｘ＝＝１＆＆ｙ＝＝０）と、を合わせて、ａｓｓｅｒｔ（！（ｙ＝＝０）＆＆！（ｘ＝＝１＆＆ｙ＝＝０））とする。そして、モデル検査部１３は、上記のようにしたａｓｓｅｒｔを、メモリ値を変更する時点である６行目に加えて検証を行う。
【００２８】
モデル検査部１３は、例えば、ＶＡＲＶＥＬを用いた場合、上記検証により反例として、ｘ値が−２となる対案を算出し提示する。すなわち、ｙ値を０に変更するのと同時に、 ｘ値を、例えば−２にすれば、実際に起こり得る状況になるため、その変更したメモリ値が適正である旨を提示する。
【００２９】
次に本実施の形態に係るデバッグ装置によるデバッグ方法について詳細に説明する。
図４は、本実施の形態に係るデバッグ装置の処理フローを示すフローチャートである。
【００３０】
まず、再生停止部１１がプログラムを一時停止させ（ステップＳ１０１）、ユーザが入力装置１５を介して変更値を入力する（ステップＳ１０２）。変更部１２は、入力装置１５に入力された変更値に基づいて、再生停止部１１により一時停止されたプログラムにおいて所定のメモリ値を変更する。
【００３１】
次に、モデル検査部１３は、変更部１２により変更された所定のメモリ値が他のメモリ値の関係で適正であるか否かをモデル検査する（ステップＳ１０３）。
【００３２】
モデル検査部１３は、変更部１２により変更された所定のメモリ値が他のメモリ値の関係で適正であると判断したとき（ステップＳ１０４のＹＥＳ）、そのメモリ値が適正である旨を表示部１４に表示させる（ステップＳ１０５）。一方、モデル検査部１３は、変更部１２により変更された所定のメモリ値が他のメモリ値の関係で不適正であると判断したとき（ステップＳ１０４のＮＯ）、メモリ値が適正となる対案があるか否かを判断する（ステップＳ１０６）。
【００３３】
モデル検査部１３は、メモリ値が適正となる対案があると判断したとき（ステップＳ１０６のＹＥＳ）、その対案のメモリ値を表示部１４に表示させ（ステップＳ１０７）、上記（ステップＳ１０２）の処理に戻る。一方、モデル検査部１３は、メモリ値が適正となる対案がないと判断したとき（ステップＳ１０６のＮＯ）、そのメモリ値の変更が常に不適正である旨を表示部１４に表示させ（ステップＳ１０８）、上記（ステップＳ１０２）の処理に戻る。
【００３４】
以上、本実施の形態に係るデバッグ装置１において、変更部１２は再生停止部１１により一時停止されたプログラムにおいて、所定のメモリ値を変更し、モデル検査部１３は、変更部１２により変更されたメモリ値が他のメモリ値の関係で適正であるか否かをモデル検査する。これにより、ユーザは、上記検査結果を用いて変更されたメモリ値が適正であるか否かを容易に判断できる。したがって、デバッグ作業においてメモリ値を適正に設定し最適なデバッグを行うことができる。
【００３５】
なお、本発明は上記実施の形態に限られたものではなく、趣旨を逸脱しない範囲で適宜変更することが可能である。例えば、上記実施の形態において、Ｃ言語のプログラムに適用されているが、これに限らず、任意のプログラムに適用可能である。
【００３６】
また、本発明は、図４に示す処理を、ＣＰＵにコンピュータプログラムを実行させることにより実現することも可能である。
【００３７】
プログラムは、様々なタイプの非一時的なコンピュータ可読媒体（non-transitory computer readable medium）を用いて格納され、コンピュータに供給することができる。非一時的なコンピュータ可読媒体は、様々なタイプの実体のある記録媒体（tangible storage medium）を含む。非一時的なコンピュータ可読媒体の例は、磁気記録媒体（例えばフレキシブルディスク、磁気テープ、ハードディスクドライブ）、光磁気記録媒体（例えば光磁気ディスク）、ＣＤ−ＲＯＭ（Read Only Memory）、ＣＤ−Ｒ、ＣＤ−Ｒ／Ｗ、半導体メモリ（例えば、マスクＲＯＭ、ＰＲＯＭ（Programmable ROM）、ＥＰＲＯＭ（Erasable PROM）、フラッシュＲＯＭ、ＲＡＭ（random access memory））を含む。
【００３８】
また、プログラムは、様々なタイプの一時的なコンピュータ可読媒体（transitory computer readable medium）によってコンピュータに供給されてもよい。一時的なコンピュータ可読媒体の例は、電気信号、光信号、及び電磁波を含む。一時的なコンピュータ可読媒体は、電線及び光ファイバ等の有線通信路、又は無線通信路を介して、プログラムをコンピュータに供給できる。
【００３９】
上記実施の形態の一部又は全部は、以下の付記のようにも記載されうるが、以下には限られない。
【００４０】
（付記１）
プログラムの実行を一時停止させる停止手段と、
前記停止手段により一時停止されたプログラムにおいて、所定のメモリ値を変更する変更手段と、
前記変更手段により変更されたメモリ値が他のメモリ値の関係で適正であるか否かをモデル検査するモデル検査手段と、
を備える、ことを特徴とするデバッグ装置。
（付記２）
（付記１）記載のデバッグ装置において、
前記モデル検査手段は、前記プログラムの状態遷移図において、初期状態から任意状態への到達可能性を検査することで、前記変更手段により変更されたメモリ値が他のメモリ値の関係で適正であるか否かをモデル検査する、ことを特徴とするデバッグ装置。
（付記３）
（付記１）又は（付記２）記載のデバッグ装置であって、
前記モデル検査手段による検査結果を表示する表示手段を更に備える、ことを特徴とするデバッグ装置。
（付記４）
（付記１）乃至（付記３）のうちいずれか記載のデバッグ装置であって、
前記モデル検査手段は、前記変更手段により変更されたメモリ値が不適正であると判断したとき、適正なメモリ値を算出し提示する、ことを特徴とするデバッグ装置。
（付記５）
プログラムの実行を一時停止させるステップと、
前記一時停止されたプログラムにおいて、所定のメモリ値を変更するステップと、
前記変更されたメモリ値が他のメモリ値の関係で適正であるか否かをモデル検査するステップと、
を含む、ことを特徴とするデバッグ方法。
（付記６）
（付記５）記載のデバッグ方法において、
前記プログラムの状態遷移図において、初期状態から任意状態への到達可能性を検査することで、前記変更されたメモリ値が他のメモリ値の関係で適正であるか否かをモデル検査する、ことを特徴とするデバッグ方法。
（付記７）
（付記５）又は（付記６）記載のデバッグ方法であって、
前記モデル検査による検査結果を表示するステップを更に含む、ことを特徴とするデバッグ方法。
（付記８）
（付記５）乃至（付記７）のうちいずれか記載のデバッグ方法であって、
前記変更されたメモリ値が不適正であると判断したとき、適正なメモリ値を算出し提示するステップを更に含む、ことを特徴とするデバッグ方法。
（付記９）
プログラムの実行を一時停止させる処理と、
前記一時停止されたプログラムにおいて、所定のメモリ値を変更する処理と、
前記変更されたメモリ値が他のメモリ値の関係で適正であるか否かをモデル検査する処理と、
をコンピュータに実行させる、ことを特徴とするデバッグプログラム。
【産業上の利用可能性】
【００４１】
本発明は、プログラムのデバッグを行うデバッグ装置に適用可能である。
【符号の説明】
【００４２】
１    デバッグ装置
２    停止手段
３    変更手段
４    モデル検査手段
１１    再生停止部
１２    変更部
１３    モデル検査部
１４    表示部
１５    入力装置
【図１】
2013210736.tif 000003
【図２】
2013210736.tif 000004
【図３】
2013210736.tif 000005
【図４】
2013210736.tif 000006