(57)【要約】【課題】定理証明技術に基づく仕様検証装置を用いて、動作記述言語によって記述された仕様に対して匿名性が保証されていることを検証するための匿名性検査装置を提供する。【解決手段】動作記述言語による記述５が匿名性を保証していることを検証するための装置であって、「動作記述言語による記述」５、「匿名性保証の条件の性質記述言語による記述」７及び「匿名であることを確認したい全ての動作のリスト」６に基づいて、性質記述言語によって記述され、帰納法によって検証される各項目を含む検証命題８を生成するプリプロセッサ２と、検証命題８と、「動作記述言語による記述」５を性質記述言語に変換した記述とを入力として、検証命題に対する検証を行う仕様検証装置４とを備えている。【選択図】    図１
2006293633.tif 000002
【特許請求の範囲】
【請求項１】
動作記述言語による記述が匿名性を保証していることを検証するための匿名性検査装置であって、
「動作記述言語による記述」、「匿名性保証の条件の性質記述言語による記述」及び「匿名であることを確認したい全ての動作のリスト」を入力とし、性質記述言語によって記述された、帰納法によって検証される項目を含む検証命題を生成するプリプロセッサと、
前記プリプロセッサが生成した検証命題と、「動作記述言語による記述」を性質記述言語に変換した記述とを入力として、検証命題に対する検証を行う仕様検証装置と
を備えることを特徴とする匿名性検査装置。
【請求項２】
前記仕様検証装置が定理証明器からなることを特徴とする請求項１に記載の匿名性検査装置。
【請求項３】
前記プリプロセッサが、「動作記述言語による記述」の初期状態に関する検査項目を表現する文字列と、インターナル型の遷移に関する検査項目を表現する文字列と、「匿名であることを確認したい全ての動作のリスト」に指定がある場合アウトプット型の遷移に関する検査項目を表現する文字列と、「匿名であることを確認したい全ての動作のリスト」に指定がない場合アウトプット型の遷移に関する検査項目を表現する文字列とを生成し、それらを組み合わせて検査項目全体に関する検査開始命令を表す文字列を生成する
ことを特徴とする請求項１または２に記載の匿名性検査装置。
【請求項４】
動作記述言語による記述が匿名性を保証していることを検証するための匿名性検査方法であって、
「動作記述言語による記述」、「匿名性保証の条件の性質記述言語による記述」及び「匿名であることを確認したい全ての動作のリスト」を入力とし、性質記述言語によって記述された、帰納法によって検証される項目を含む検証命題を生成するステップと、
生成された検証命題と、「動作記述言語による記述」を性質記述言語に変換した記述とを入力として、仕様検証装置によって検証命題に対する検証を行うステップと、
を有することを特徴とする匿名性検査方法。
【請求項５】
動作記述言語による記述が匿名性を保証していることを検証するための方法をコンピュータに実行させる匿名性検査プログラムであって、
「動作記述言語による記述」、「匿名性保証の条件の性質記述言語による記述」及び「匿名であることを確認したい全ての動作のリスト」を入力とし、性質記述言語によって記述された、帰納法によって検証される項目を含む検証命題を生成するステップと、
生成された検証命題と、「動作記述言語による記述」を性質記述言語に変換した記述とを入力として、仕様検証装置によって検証命題に対する検証を行うステップと、
をコンピュータに実行させる匿名性検査プログラム。
【請求項６】
請求項５に記載の匿名性検査プログラムを記録したコンピュータ読み取り可能な記録媒体。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、分散システムの仕様を検証する技術に係わり、特に分散システムを使用するユーザの匿名性を検証する際に用いて好適な匿名性検査装置、方法、プログラム及び記録媒体に関する。
【背景技術】
【０００２】
ソフトウェア工学の分野では、プログラムや仕様を論理式や数式で記述し、その正しさを計算機を使って検証する方法が知られている。このような方法は、形式的手法と呼ばれる。形式的手法では、分散システムの動作を動作記述言語で記述し、一方、分散システムが満たすべき性質を性質記述言語で記述する。動作記述言語としては、 I/O−オートマトン（Input/Output -Automata）（非特許文献１）、 CSP（非特許文献２）、 π−計算（非特許文献３）などが知られている。また、性質記述言語としては、一階述語論理などが知られている。
【０００３】
形式的手法では、一般に、動作記述言語の記述が性質記述言語に変換され、分散システムが満たすべき性質の記述とともに、仕様検証装置に入力され、検証が行われる。このような変換を行う装置としては、 IOA-Toolkit（非特許文献４）などが知られている。 IOA-Toolkitでは、I/O−オートマトンで記述された分散システムの動作記述が、一階述語論理の論理式に変換される。
【０００４】
仕様検証装置としては、モデル検査技術に基づく方式と、定理証明技術に基づく方式が知られている。モデル検査技術に基づく方式は、全自動検証が可能であるが、小規模な問題に限られると言う問題がある。モデル検査技術としては、FDR（非特許文献５）、SMV (非特許文献６）、SPIN （非特許文献７）などが知られている。
【０００５】
一方、定理証明技術は、全自動の検証ができないが、大規模システムに対する検証に対応可能という長所がある。定理証明技術としては、Larch Prover（非特許文献８）、Isabelle（非特許文献９）などが知られている。たとえばLarch Proverでは、一階述語論理の論理式に対する真偽の検証が可能である。
【０００６】
なお、モデル検査技術に基づく匿名性の検証は、例えば、以下のように行われる。まず、構成図を図１０に示す。モデル検査技術を用いる方法では、まず、検証装置20への入力として、動作記述言語による記述(図１０中の「仕様Ａ21」)と匿名であることを確認したい全ての動作のリスト(図１０中の「匿名動作のリスト22」)を用意する。仕様Ｂ23は、仕様Ａ21と匿名確認動作のリスト22をもとに、図１０中の「仕様生成装置24」によって、構成される。仕様生成装置24は、以下の処理を行う。
【０００７】
（A1）仕様Ａ21に現れる、
匿名動作のリスト22の各エントリである動作名ａ1，ａ2，…，ａnをすべてある定数ｃに置き換える（置き換えた結果を、暫定仕様０と呼ぶ）。
【０００８】
（A2）次に、
・暫定仕様０に現れるｃをａlに置き換えたもの(暫定仕様１と呼ぶ)、
・暫定仕様０に現れるｃをａ2に置き換えたもの(暫定仕様２と呼ぶ)、
………
及び
・暫定仕様０に現れるｃをａnに置き換えたもの(暫定仕様ｎと呼ぶ)
を作る。
【０００９】
（A3）暫定仕様１〜暫定仕様ｎの記述を連結して仕様Ｂ23とする。
【００１０】
上記手順によって仕様Ａ21と匿名動作のリスト22から得られた仕様Ｂ23が、匿名性の検証を行うための正当な中間形式であることは、(非特許文献１０）で示されている。さて、モデル検査技術を用いる方法では、入力された二つの仕様（仕様Ａ21と仕様Ｂ23）それぞれに対して、とりうるすべての動作系列を計算部25と計算部26で計算する。その結果が図１０中のαとβである。すなわち、初期状態から始まる、すべての可能な実行系列をしらみつぶしに計算し尽くす。その後、比較部27によって、それぞれの仕様に関する実行系列集合を比較し、一致するかどうかを検査する。一致する場合は、匿名性が保証され、そうでない場合は保証されない。
【００１１】
このように、モデル検査技術では、分散システムがとりうるすべての状態に関する展開処理を必要とする。したがって、とりうる状態の数が無限の場合、あるいは有限でも非常に大きい場合は、メモリ容量不足などの理由から、実行系列に関する計算を完了できない場合がある。実行系列集合が計算できない場合、匿名性の最終検査（すなわち、実行系列集合の比較）ができないことになる。ここに、モデル検査技術を用いた場合の、大規模システムに対する匿名性検証の困難さがある。
【００１２】
なお、本願においては次の各用語が以下の意味を有するものとして用いている。
【００１３】
「動作記述言語」：分散システムがどのように動作するかに関する設計図を数学的に記述するための言語。非特許文献１、非特許文献２、非特許文献３等に説明されている。
【００１４】
「性質記述言語」：分散システムが持つべき性質を数学的に記述するための言語。一階述語論理などが知られている。
【００１５】
「仕様検証装置」：性質記述言語で記述された性質が成り立つか否かを検証するための計算機プログラム。
【００１６】
「匿名性」：分散システム中のあるエージェントによる行為を他のどのエージェントも行いうる、という性質。インターネット上のシステムにおいてユーザのプライバシを保証する上で成り立つべき性質のひとつである。
【非特許文献１】ナンシー・リンチ（Nancy A. Lynch）著、「ディストリビューテッドアルゴリズム（Distributed Algorithms）」、（米国）、モーガン・カウフマン出版社（Morgan Kaufmann Publishers）、1996年、ｐ．217−220
【非特許文献２】ホーア著、吉田信博訳、「ホーアＣＳＰモデルの理論」、丸善株式会社、 1992年
【非特許文献３】ミルナー（R. Milner）著、「コミュニケーティング・アンド・モバイルシステム  パイ計算（Communicating and mobile systems: the π-calculus）」、（米国）、ケンブリッジ大学出版局（Cambridge Univ. Press）、 2000年
【非特許文献４】ソーガード・アンダーソン外４名（J. F. Soegaard-Andersen, S.J. Garland, J.V.Guttag, N.A.Lynch and A. Pogosyants ）著、「コンピュータアシスト・シミュレーションプルーフ（“Computer-Assisted Simulation Proofs,” In Computer-Aided Verification, 5th International Conference, CAV'93）」、シュプリンガー出版（Springer-Verlag）、1993年、LNCS  687（Lecture Notes in Computer Science 697）、ｐ．305−319
【非特許文献５】「モデルチェッカーFDR2（Model-Checker FDR2）」、［online］、ベリファイド・システム・インターナショナル社（Verified Systems International GmbH）、［平成17年3月28日検索］、インターネット＜URL: http://www.verified.de/fdr.html＞
【非特許文献６】「ＳＭＶ（a symbolic model checker for CTL）システム（The SMV System）」、［online］、カーネギーメロン大学モデルチェッキンググループ（Model Checking Group, Specification and Verification Center, Carnegie Mellon University）、［平成17年3月28日検索］、インターネット＜URL: http://www-2.cs.cmu.edu/~modelcheck/smv.html＞
【非特許文献７】ジェラード・ホルツマン（Gerard J. Holzmann ）著、「スピンモデル・チェッカー（The SPIN Model-checker）」、アディソン−ウェズリー社（Addison Wesley Pub）、2003年
【非特許文献８】ガーランド外２名（S. J. Garland, J. V. Guttag and J. J. Horning）著、「オーバービュー・オブ・ラーチ（“An overview of Larch,” in Functional Programming, Concurrency, Simulation and Automated Reasoning, ）」、シュプリンガー出版（Springer-Verlag）、1993年、LNCS 693（Lecture Notes in Computer Science 693）、ｐ．329−348
【非特許文献９】ポールソン（L. C. Paulson）著、「イサベル（“Isabelle: The next seven hundred theorem provers,” in Proceedings of the 9th Conference on Automated Deduction）」、シュプリンガー出版（Springer-Verlag）、1989年、LNCS 310（Lecture Notes in Computer Science 310）、ｐ．772−773
【非特許文献１０】シュナイダー外１名（S. Schneider and A. Sidiropoulos）著、「ＣＳＰ・アンド・アノニミティ（“CSP and anonymity,” in ESORICS '96 ）」、シュプリンガー出版（Springer-Verlag）、1996年、LNCS 1146（Lecture Notes in Computer Science 1146）、ｐ．198−218
【発明の開示】
【発明が解決しようとする課題】
【００１７】
近年、インターネットに基づく電子投票システムなどのコンピュータシステムが出現しつつある。このようなコンピュータシステムに対しては、システム動作によってユーザの匿名性が侵されないことをあらかじめ検査しておく必要がある。たとえば、電子投票システムに対して、投票者がどの候補者に投票したかが第三者に知られないことを検査する必要がある。
【００１８】
しかし、従来、形式的手法で検証可能な仕様の性質としては、安全性(想定していないメモリ領域へのアクセスをしない、など)や活性(プログラムの実行を続けていればいつか停止可能になる、など)が主であり、匿名性に対してどのように検証を行えばよいのかは明らかではなかった。
【００１９】
とくに、コンピュータシステムが持つべき匿名性を、計算機を用いて検証する手法は、モデル検査技術に基づく方法は知られているが、定理証明技術に基づく手法は知られていなかった。すなわち、現状では、小規模システムに対する匿名性の検証は可能でも、大規模システムに対する匿名性の検証は困難である。
【００２０】
本発明は、これに鑑みてなされたもので、その目的とするところは、定理証明技術に基づく仕様検証装置を用いて、動作記述言語によって記述された仕様に対して匿名性が保証されていることを検証するための匿名性検査装置、方法、プログラム及び記録媒体を提供することにある。
【課題を解決するための手段】
【００２１】
上記課題を解決するため、本発明は、動作記述言語による記述が匿名性を保証していることを検証するための匿名性検査装置であって、「動作記述言語による記述」、「匿名性保証の条件の性質記述言語による記述」及び「匿名であることを確認したい全ての動作のリスト」を入力とし、性質記述言語によって記述された、帰納法によって検証される項目を含む検証命題を生成するプリプロセッサと、前記プリプロセッサが生成した検証命題と、「動作記述言語による記述」を性質記述言語に変換した記述とを入力として、検証命題に対する検証を行う仕様検証装置とを備えることを特徴とする匿名性検査装置である。
【００２２】
本発明は、上記に記載の発明において、前記仕様検証装置が定理証明器からなることを特徴とする。
【００２３】
本発明は、上記に記載の発明において、前記プリプロセッサが、「動作記述言語による記述」の初期状態に関する検査項目を表現する文字列と、インターナル型の遷移に関する検査項目を表現する文字列と、「匿名であることを確認したい全ての動作のリスト」に指定がある場合アウトプット型の遷移に関する検査項目を表現する文字列と、「匿名であることを確認したい全ての動作のリスト」に指定がない場合アウトプット型の遷移に関する検査項目を表現する文字列とを生成し、それらを組み合わせて検査項目全体に関する検査開始命令を表す文字列を生成することを特徴とする。
【００２４】
本発明は、動作記述言語による記述が匿名性を保証していることを検証するための匿名性検査方法であって、「動作記述言語による記述」、「匿名性保証の条件の性質記述言語による記述」及び「匿名であることを確認したい全ての動作のリスト」を入力とし、性質記述言語によって記述された、帰納法によって検証される項目を含む検証命題を生成するステップと、生成された検証命題と、「動作記述言語による記述」を性質記述言語に変換した記述とを入力として、仕様検証装置によって検証命題に対する検証を行うステップと、を有することを特徴とする匿名性検査方法である。
【００２５】
本発明は、動作記述言語による記述が匿名性を保証していることを検証するための方法をコンピュータに実行させる匿名性検査プログラムであって、「動作記述言語による記述」、「匿名性保証の条件の性質記述言語による記述」及び「匿名であることを確認したい全ての動作のリスト」を入力とし、性質記述言語によって記述された、帰納法によって検証される項目を含む検証命題を生成するステップと、生成された検証命題と、「動作記述言語による記述」を性質記述言語に変換した記述とを入力として、仕様検証装置によって検証命題に対する検証を行うステップと、をコンピュータに実行させる匿名性検査プログラムである。
【００２６】
本発明は、上記に記載の匿名性検査プログラムを記録したコンピュータ読み取り可能な記録媒体。
【発明の効果】
【００２７】
本発明においては、「動作記述言語による記述」、「匿名性保証の条件の性質記述言語による記述」及び「匿名であることを確認したい全ての動作のリスト」に基づいて、性質記述言語によって記述され、帰納法によって検証される各項目を含む検証命題を生成するための手段を設けたので、定理証明技術に基づく仕様検証装置を用いて、動作記述言語によって記述された仕様に対して匿名性が保証されていることを検証することができる。
【発明を実施するための最良の形態】
【００２８】
以下、図面を参照して本発明による匿名性検査装置の実施の形態について説明する。図１は、本発明による匿名性検査装置の実施の形態の構成例を示すブロック図である。図１に示す匿名性検査装置1は、コンピュータ及びその周辺装置を用いて実行される計算機プログラムによって構成されている。図１において匿名性検査装置1は、プリプロセッサ2、動作記述言語による記述から性質記述言語による記述への変換装置3、および仕様検査装置4から構成されている。
【００２９】
プリプロセッサ2は、動作記述言語による仕様の記述5、匿名であることを確認したい全ての動作のリスト（以下、匿名動作のリスト）6及び性質記述言語による匿名性保証条件の記述7を処理し、性質記述言語で記述された検証命題8を生成する。この検証命題8は、ファイル9に記録される。
【００３０】
動作記述言語による記述から性質記述言語による記述への変換装置3は、入力された動作記述言語による記述を処理し、性質記述言語による記述を出力する。動作記述言語による記述から性質記述言語による記述への変換装置3から出力された性質記述言語による記述はファイル10に記録される。
【００３１】
仕様検証装置4は、Larch Prover等の定理証明器から構成されている。仕様検証装置4は、プリプロセッサ2と動作記述言語による記述から性質記述言語による記述への変換装置3とのそれぞれが出力する性質記述言語による記述を受け取って入力し、ユーザ11からの命令入力等の操作に基づき性質記述言語による記述に対する式変形処理を行って真または偽を出力する。
【００３２】
図１において本発明が主要な特徴とする部分はプリプロセッサ2である。「動作記述言語による記述から性質記述言語による記述への変換装置」3と「仕様検証装置」4は、既知の技術を用いればよい。以下の説明では便宜上、動作記述言語による記述から性質記述言語による記述への変換装置3としてIOA-Toolkit（I/Oオートマトン・ツールキット）（非特許文献４）を、仕様検証装置4としてLarch Prover（ラーチ定理証明器）（非特許文献８）を用いて説明する。
【００３３】
以下、具体的な記述例を示しながら図１の匿名性検査装置1の構成及び動作について説明する。本実施の形態における動作記述言語と性質記述言語の構文の定義は図２である。図２中、「｛Ａ｝＊」は記号列｛Ａ｝の０個以上の並びを表す。
【００３４】
［準備］
図３は、図１の動作記述言語による記述5の例（記述例D101）を示す。なお、以下の各記述には、可読性を確保するため必要に応じて改行を挿入し、また説明のため必要に応じて行番号を付ける。
【００３５】
図３において、1003行〜1008行が型宣言部である。1010行〜1012行がグローバル変数の宣言と初期値の設定を行っている部分である。そして、1014行〜1038行が動作記述本体部である。
【００３６】
図３の動作記述言語による記述5の記述例D101は、全体として、コンピュータ制御によるジュークボックスの動作を記述したものである。ジュークボックスに１または複数枚のコインが投入され、ボタンAが押されればコインの枚数分ジャズを演奏し、ボタンBが押されればコインの枚数分ロックを演奏するという動作を記述したものである。グローバル変数「pc」がジュークボックスの動作状態（例えば「start」が初期状態、「button」がボタンを押すことが可能な状態等）を表し、グローバル変数「quarter」がジュークボックスに投入されたコインの残り枚数を表す。以下、各行の記述内容について説明する。
【００３７】
例えば1015行の「internal」はアクションの型（インターナル型；内部型）、「insertCoins」はアクション名、「q」はアクションの引数である。1015行のアクション「internal insertCoins(q)」は、1016行の「pre」以下の条件文と、1017行の「eff」以下のその条件成立時の実行文とから構成されている。すなわち、1015行のアクション「internal insertCoins(q)」は、変数「pc」の値が「satrt」ならば、変数「pc」の値を「button」に更新するとともに、変数「quarter」の値を引数「q」の値に更新するという処理を行うものである。ここで、演算子「=」は等号を、「pc := button」の演算子「:=」は代入を表し、符号「;」は文の継続を表している。
【００３８】
1020行〜1026行の「output」型（アウトプット型；外部型；出力型）のアクション「output pressButton(id)」は、定理証明器（仕様検証装置4）内でアクション「pressButton(A)」、「pressButton(B)」などとして呼び出され、アクションの仮引数「id」には値「A」、「B」などが代入される。このアクション「output pressButton(id)」は、変数「pc」の値が「button」に一致した場合（1021行）、引数「id」が「A」ならば変数「pc」の値を「jazz」に更新し（1023行）、引数「id」が「A」でないならば変数「pc」の値を「rock」に更新する（1025行）。一方、変数「pc」の値が「button」に一致しない場合には処理は行われない。
【００３９】
なお、1029行等の演算子「∨」は論理和（OR）、「∧」は論理積（AND）を表している。
【００４０】
操作者によってジュークボックスにコインが投入された場合に相当するアクション「internal insertCoins(q)」（1015行〜1018行）が呼び出されると、ジュークボックスが起動中の場合、ジュークボックスがボタン押下可能状態（受付可能状態）にされるとともに、投入されたコインの枚数が変数「quarter」に代入される。ジュークボックスのボタンAまたはボタンBが押された場合に相当するアクション「output pressButton(id)」（1020行〜1026行）が呼び出されると、ジュークボックスがボタン押下可能状態の場合、押下されたボタンが「A」のときジャズの演奏状態となり、「A」でないとき（すなわち「B」のとき）ロックを演奏状態となる。
【００４１】
また、演奏が行われた際には、1028行〜1030行のアクション「output playMusic」、1032行〜1034行のアクション「 output playJazz」、及び1036行〜1039行の「output playRock」が呼び出されて、コインの枚数を減らす処理や、演奏を終了する処理が行われる。アクション「output playMusic」では、ジャズを演奏中（「pc = jazz」）またはロックを演奏中（「pc = rock」）で、かつ、コインの残り枚数が１枚でない（「quarter ~= 1」）場合、コインの枚数が１枚減らされる（「quarter := quarter - 1」）。
【００４２】
アクション「output playJazz」では、ジャズを演奏中で、かつ、コインの残り枚数が１枚の場合（「pc = jazz ∧ quarter = 1」）、演奏が停止状態（停止準備状態）とされる（「pc :=stop」）。  アクション「output playRock」では、ロックを演奏中で、かつ、コインの残り枚数が１枚の場合（「pc = rock ∧ quarter = 1」）、演奏が停止状態（停止準備状態）とされる（「pc :=stop」）。
【００４３】
図４は、図１の性質記述言語による記述7等の性質記述言語の一般例(記述例D102)を示す。記述例D102における「start(s:States[Jukebox]) => as(s:States[Jukebox], s:States[Jukebox])」は、状態「s」が初期状態「start」ならば「as(s:States[Jukebox], s:States[Jukebox])」（as(s, s)）が成立することを表している。
【００４４】
上述した図３の記述例D101をIOA-Toolkitからなる変換装置3で変換すると、図５の性質記述言語による記述（記述D103）が得られる。記述D103のうち、「start」、「internal」、「output」、「enabled」および「effect」は、Larch Proverの述語名で、その定義はIOA-Toolkitによって出力される。他の類似技術（たとえば、Isabelle（非特許文献９））でも、Larch Proverを使う場合と全く同様にして、述語名の定義を出力するプログラムは構成できる。例えば、図５の記述D103の1202行では、「s:States[Jukebox].pc」が状態「s」での変数「pc」の値、「s:States[Jukebox].quarter」が状態「s」での変数「quarter」の値を表している。
【００４５】
図６は、図１の匿名動作のリスト6の例(記述例D104)を示す。「("pressButton(A)", "pressButton(B)")」は、「A」が押されたのか、「B」が押されたのかが匿名となっているか（隠されているか）ということが、確認したい動作であることを示している。
【００４６】
図７は、図１の性質記述言語による匿名性保証の条件の記述7の例(記述例D105)を示す。
【００４７】
図１のプリプロセッサ2に投入される「匿名性保証の条件の性質記述言語による記述」7は、次の制限を満たすように記述されるとする。
・変数s:States[システム名]を持つ。
・変数s':States[システム名]を持つ。
・上記以外の変数は現れない。
【００４８】
［プリプロセッサの実現方法］
以下では、プリプロセッサ2の実現方法を説明する。
【００４９】
プリプロセッサ2は、内部変数として、以下を持つ。
・ioa(文字列)：動作記述言語による記述5を格納するメモリ領域。
・anonym(文字列のリスト)：匿名動作のリスト6を格納するメモリ領域。
・as(文字列)：匿名性保証の条件の性質記述言語による記述7を格納するメモリ領域。
・sys(文字列)：システム名を格納するメモリ領域。
・lsl(文字列)：出力となる性質記述言語による記述を格納するメモリ領域。
・stmp(文字列)：文字列の一時格納用。
・stmp2 (文字列)：文字列の一時格納用。
・ltmp(文字列のリスト)：文字列のリストの一時格納用。
【００５０】
また、ライブラリ関数として、以下が定義されている。
【００５１】
・関数append：引数として、二つの文字列str1と文字列str2をとり、str1にstr2を連結した結果得られる文字列を返す。
−  実行例：関数呼出しappend("abc", "de")を実行すると、結果"abcde"が返される。
【００５２】
・関数replace：引数として、三つの文字列str1、str2およびstr3をとり、文字列str1に現れる全ての部分文字列str2をstr3に置き換えた結果得られる文字列を返す。
−  実行例：関数呼出しreplace ("abcdefgdefg", "de", "ZZZZ")を実行すると、結果"abcZZZZfgZZZZfg"が返される。
【００５３】
・関数car：引数として、リストlstをとり、第一要素を返す。
−  実行例：関数呼出しcar(("a", "b", "c"))を実行すると、結果"a"が返される。
【００５４】
・関数cdr：引数として、リストlstをとり、第二要素以降を返す。
−  実行例：関数呼出しcdr(("a", "b", "c"))を実行すると、結果("b", "c")が返される。
【００５５】
・関数write：引数として、文字列strと文字列filenameをとり、filenameをファイルネームとみなして新規ファイルを作成し、さらに文字列strを内容として書き込む。返値は、ファイルの書き込みに成功した場合はt、失敗した場合はnilである。
−  実行例：関数呼出しwrite("c", "tmpFile")を実行すると、ファイル"tmpFile"が作成され、ファイルの内容として"c"が書き込まれる。
【００５６】
・関数read-from-string：引数として、文字列strをとり、空白および改行を区切りとして文字列strを複数の単語に切り分けた結果をリスト形式で返す。
−  実行例：内部変数ioaに文字列
"automaton Jukebox 
signature
internal insertCoins(q:NonZeroNat)"
が格納されているとする。このとき、関数呼出しread-from-string(ioa)を実行すると、結果
("automaton", "Jukebox", "signature", "internal", "insertCoins(q:NonZeroNat)")
が返される。
【００５７】
次に、図８を参照してプリプロセッサ2による処理について説明する。
【００５８】
まず、各変数に対する初期値の設定が、処理例（B1）のようにして行われる（図８のステップS11）。
【００５９】
（B1）「動作記述言語による記述5」「匿名動作のリスト6」および「匿名性保証の条件の性質記述言語による記述7」を引数として受け取り、それぞれを内部変数ioa,  anonymおよびasに格納する。また、変数sys, lsl, stmp, stmp2の値をすべて""(空文字列)に設定する。
【００６０】
次に、動作記述5（内部変数ioa）を読み込み、処理例（B2）のようにして仕様名が抽出される（ステップS12）。
【００６１】
（B2）関数呼出しread-from-string(ioa)を実行し、結果を内部変数ltmpに格納する。次に、関数呼出しcdr(ltmp)を実行し、結果を内部変数ltmpに格納する。さらに、関数呼出しcar(ltmp)を実行し、結果を内部変数sysに格納する。さらに、変数ltmpの値をnil (空リスト)に設定する。ただし、内部変数ioaには（動作記述言語の識別子（"automaton"），システム名（"Jukebox"），…）の位置に変数sysに格納すべきシステム名が格納されていることとする。
【００６２】
次に、処理例（B3）のようにして初期状態に関する検査項目(conj1)の定義を表現する文字列が生成される（ステップS13）。
【００６３】
（B3）文字列
"assert
conj1 <=>
start(s:States[システム名]) => as(s:States[システム名], s:States[システム名])
.."
を変数lslに格納する。
【００６４】
次に、処理例（B4）のようにしてinternal型の遷移に関する検査項目(conj2)を表現する文字列が生成される（ステップS14）。
【００６５】
（B4）文字列
"assert
conj2 <=> 
(as(s:States[システム名], s':States[システム名])
∧      enabled(s:States[システム名], a:Actions[システム名])
∧      internal(a:Actions[システム名]))
=> (＼E a':Actions[システム名]
(enabled(s':States[システム名], a':Actions[システム名])
∧ internal(a':Actions[システム名])
∧ as(effect(s:States[システム名], a:Actions[システム名]),
effect(s':States[システム名], a':Actions[システム名]))))
.."
を変数stmpに格納する。さらに、関数呼出しappend(lsl, stmp)を実行し、結果を内部変数lslに格納する。
【００６６】
次に、処理例（B5）〜（B11）のようにしてoutput型（匿名動作のリスト6に指定がある場合）の遷移に関する検査項目(conj3)を表現する文字列が生成される（ステップS15）。ここでは図７に示すような匿名動作（匿名性の保証条件7）に関する検査項目の生成が行われる。その際、検査項目(conj3)は、「X=>Y」（XならばY）の形式で生成される。下記処理例（B5）〜（B11）では、「X」に該当する部分が、処理例（B5）の「(as(s:States[システム名], s':States[システム名])」（「<=>」の後）から処理例（B8）の「 "false ))」（「=>」の前）までである。そして、「Y」に該当する部分が、処理例（B8）の「(true "」（「=>」の後）から処理例11の文字列までである。
【００６７】
（B5）文字列
"assert
conj3 <=> 
(as(s:States[システム名], s':States[システム名])
∧ enabled(s:States[システム名], a:Actions[システム名])
∧ ("
を変数stmpに格納する。次に、関数呼出しappend(lsl, stmp)を実行し、結果を内部変数lslに格納する。さらに、変数anonymの内容を変数ltmpに格納する。
【００６８】
（B6）変数ltmpの内容がnil(空リスト)かを比較する。比較結果が真（nilである）ならば処理例（B8）にジャンプする。偽ならば、処理例（B7）に移る。
【００６９】
（B7）文字列
"(a:Actions[システム名] = "
を変数stmpに格納する。次に、関数呼出しappend(lsl, stmp)を実行し、結果を内部変数lslに格納する。さらに、関数呼出しcar(ltmp)を評価し、結果を変数stmpに格納する。さらに、関数呼出しappend(lsl, stmp)を実行し、結果を内部変数lslに格納する。さらに、関数呼出しcdr(ltmp)を評価し、結果を変数ltmpに格納する。さらに、文字列
") ∨"
を変数stmpに格納する。さらに、関数呼出しappend(lsl, stmp)を実行し、結果を内部変数lslに格納する。さらに、処理例（B6）にジャンプする。
【００７０】
（B8）文字列
"false ))
=> (true "
を変数stmpに格納する。次に、関数呼出しappend(lsl, stmp)を実行し、結果を内部変数lslに格納する。さらに、変数anonymの内容を変数ltmpに格納する。
【００７１】
（B9）変数ltmpの内容がnil(空リスト)かを比較する。比較結果が真（nilである）ならば処理例（B11）にジャンプする。偽ならば、処理例（B10）に移る。
【００７２】
（B10）文字列
"∧ (enabled(s':States[システム名],アクション名)
∧ as(effect(s:States[システム名], a:Actions[システム名]),
effect(s':States[システム名], アクション名)))"
を変数stmpに格納する。さらに、関数呼出しcar(ltmp)を評価し、結果を変数stmp2に格納する。さらに、関数呼出しcdr(ltmp)を評価し、結果を変数ltmpに格納する。さらに、関数呼出しreplace(stmp, "アクション名", stmp2)を実行し、結果を内部変数stmpに格納する。さらに、関数呼出しappend(lsl, stmp)を実行し、結果を内部変数lslに格納する。さらに、処理例（B9）に戻る。
【００７３】
（B11）文字列
")
.."
を変数stmpに格納する。さらに、関数呼出しappend(lsl, stmp)を実行し、結果を内部変数lslに格納する。
【００７４】
次に、処理例（B12）〜（B15）のようにしてoutput型（匿名動作のリスト6に指定がない場合)の遷移に関する検査項目(conj4)を表現する文字列が生成される（ステップS16）。検査項目(conj4)は、匿名動作以外でoutput型を持つアクションに関する検査項目である。例えば、処理例（B15）に示す「output(a: Actions[システム名])」が検査項目となる。
【００７５】
（B12）文字列
"assert
conj4 <=>
(as(s:States[システム名], s':States[システム名])
∧ enabled(s:States[システム名], a:Actions[システム名])"
を変数stmpに格納する。次に、関数呼出しappend(lsl, stmp)を実行し、結果を内部変数lslに格納する。さらに、変数anonymの内容を変数ltmpに格納する。
【００７６】
（B13）変数ltmpの内容がnil (空リスト)かを比較する。比較結果が真（nilである）ならば処理例（B15）にジャンプする。偽ならば、処理例（B14）に移る。
【００７７】
（B14）文字列
"∧ ~(a:Actions[システム名] = "
を変数stmpに格納する。次に、関数呼出しappend(lsl, stmp)を実行し、結果を内部変数lslに格納する。さらに、関数呼出しcar (ltmp)を評価し、結果を変数stmpに格納する。さらに、関数呼出しcdr(lrmp)を評価し、結果を変数ltmpに格納する。さらに、関数呼出しappend(lsl, stmp)を実行し、結果を内部変数lslに格納する。さらに、関数呼出しappend(lsl,  ")")を実行し、結果を内部変数lslに格納する。さらに、処理例（B13）に戻る。
【００７８】
（B15）文字列
"∧ output(a:Actions[システム名]))
=> (enabled(s':States[システム名], a:Actions[システム名])
∧ as(effect(s:States[システム名], a:Actions[システム名]),
effect(s':States[システム名], a:Actions[システム名])))
.."
を変数stmpに格納する。さらに、関数呼出しappend(lsl, stmp)を実行し、結果を内部変数lslに格納する。
【００７９】
次に、処理例（B16）のようにして「as」の定義部分を表す文字列が生成される（ステップS17）。ここで、生成される文字列の一部(記述例D105に相当)はユーザによってステップS11でプリプロセッサ2に与えられたものである。
【００８０】
（B16）文字列
"assert
as(s:States[システム名], s':States[システム名])
<=> ("
を変数stmpに格納する。次に、関数呼出しappend(lsl, stmp)を実行し、結果を内部変数lslに格納する。さらに、関数呼出しappend(lsl, as)を実行し、結果を内部変数lslに格納する。さらに、文字列
")
.."
を変数stmpに格納する。さらに、関数呼出しappend(lsl, stmp)を実行し、結果を内部変数lslに格納する。
【００８１】
次に、処理例（B17）のようにして検査項目全体(conj1〜conj4)に関する検査開始命令を表す文字列(prove...)が生成される（ステップS18）。すなわち、conj1〜conj4を組み合わせて検査項目（トップレベル）が生成される。
【００８２】
（B17）文字列
"prove
conj1 ∧ conj2 ∧ conj3 ∧ conj4
.."
を変数stmpに格納する。さらに、関数呼出しappend(lsl, stmp)を実行し、結果を内部変数lslに格納する。
【００８３】
次に、ステップS19で、処理例（B18）〜（B19）のようにして文字列「システム名」をステップS12で抽出した仕様名に置き換え、定理証明器の入力言語として扱うことができる文字列に変換し、さらに、結果をファイル「tmpFile」に書き込む処理が行われる。これは、上記で生成した文字列に文字列「システム名」が含まれるため、直接、仕様検証装置（定理証明器）4の入力には使えないためである。
【００８４】
（B18）関数呼出しreplace(lsl, "システム名", sys)を実行し、結果を内部変数lslに格納する。
【００８５】
（B19）関数呼出しwrite(lsl, "tmpFile")を実行し、新規ファイル"tmpFile"を作成して、内部変数lslに格納された文字列を書き込む。
【００８６】
以上の処理によって図１のプリプロセッサ2は、仕様の動作記述言語による記述5、匿名動作のリスト6、及び性質記述言語による匿名性保証条件の記述7を読み込み、記述5の初期状態に関する検査項目(conj1)、記述5のinternal型の遷移に関する検査項目(conj2)、記述5のoutput型(匿名動作のリスト6に指定がある場合)の遷移に関する検査項目(conj3)、記述5のoutput型(匿名動作のリスト6に指定がない場合)の遷移に関する検査項目(conj4)をそれぞれ表現する文字列を記述7に応じて生成し、それらを組み合わせて検査項目全体(conj1〜conj4)に関する検査開始命令を表す文字列(prove...)を生成する。そして、各検査項目を表す文字列(conj1〜conj4)、記述7に基づく文字列、及び検査開始命令を表す文字列(prove...)からなる性質記述言語によって記述された検証命題8（図９）をファイル9に記録する。
【００８７】
ここで、検証命題8に含まれる各検査項目（conj1〜conj4）は、仕様証明装置4において帰納法（数学的帰納法）によって検証される各項目を表している。すなわち、検査項目（conj1）はある検証命題がシステム初期状態で成立すべき項目として表されている。そして、他の検査項目 conj2〜4は、全て A=>Bという記述がされており、Aに相当する項目は、命令aを実行する前のシステム状態s および s' で成立すべき項目であり、Bに相当する項目は、命令a の実行後のシステム状態 effect(s, a)および effect(s', b)（但し、命令bは、命令a または他の命令a' ）に成立すべき項目であり、全体としてA=>Bはシステム状態 s およびs' で命題Aが真ならば、命令実行後のシステム状態effect(s, a)およびeffect(s', b)で命題Bが真であるということを検証するための項目として表されている。すなわち、検査によりconj1が真であり、更に conj2〜4のそれぞれが真であれば、全ての実行ステップにおいて検査項目が真であるということが証明されることになる。従来のモデル検査技術では全ての実行ステップについて総当たりで検査項目の検査を行っていたのに対して、本発明は、帰納法により証明を行うため、メモリ不足などの問題が発生せず、実用的な時間での検査を行うことが可能となる。
【００８８】
［実施例：プリプロセッサ2］
次に、上述したプリプロセッサ2の処理内容の詳細を処理例（C1）〜処理例（C28）として具体的に説明する。
【００８９】
プリプロセッサ2の実行の詳細を述べる。以下では、動作記述言語による記述5として記述例D101（図３）を、匿名動作のリスト6として記述例D104（図４）を、匿名性保証の条件の性質記述言語による記述7として記述例D105（図７）を、プリプロセッサ2に与えたときの実行を示す。
【００９０】
（C1）「動作記述言語による記述5（記述例D101）」「匿名動作のリスト6（記述例D104）」および「匿名性保証の条件の性質記述言語による記述7（記述例D105）」を引数として受け取り、それぞれ、内部変数ioa, anonymおよびasに格納する。
【００９１】
すなわち、変数ioaの値は、
"automaton Jukebox
signature
internal insertCoins(q:NonZeroNat),
output pressButton(id:AorB),
output playMusic,
output   playJazz，
output   playRock
【００９２】
states
pc:      PC         := start,
quarter:  NonZeroNat := 1
【００９３】
transitions
internal insertCoins(q)
pre pc = start
eff pc := button;
quarter := q
【００９４】
output pressButton(id)
pre pc = button
eff if id = A then
pc := jazz
else
pc：= rock
fi
output playMusic
pre (pc = jazz ∨ pc = rock) ∧ quarter ~= 1
eff quarter := quarter - 1
output playJazz
pre pc = jazz ∧ quarter = 1
eff pc := stop
output playRock
pre pc = rock ∧ quarter = 1
eff pc := stop"
【００９５】
変数anonymの値は、
("pressButton(A)", "pressButton(B)")
【００９６】
変数asの値は、
"((s:States[システム名].quarter = s':States[システム名].quarter)
∧ ((s:States[システム名].pc = s':States[システム名].pc)
∨ (s:States[システム名].pc = jazz ∧ s':States[システム名].pc = rock)
∨ (s:States[システム名].pc = rock ∧ s':States[システム名].pc = jazz)))"
である。
【００９７】
また、変数sys, lsl, stmp, stmp2の値をすべて""(空文字列)に設定する。
【００９８】
（C2）関数呼出しread-from-string(ioa)を実行し、結果
("automaton", "Jukebox", "signature",…… , "eff", "pc", ":=", "stop")
を内部変数ltmpに格納する。
【００９９】
次に、関数呼出しcdr(ltmp)を実行し、結果
("Jukebox", "signature", ……, "eff", "pc", ":=", "stop")
を内部変数ltmpに格納する。
【０１００】
さらに、関数呼出しcar(ltmp)を実行し、結果
"Jukebox"
を内部変数sysに格納する。さらに、変数ltmpの値をnil(空リスト)に設定する。
【０１０１】
（C3）文字列
"assert
conj1 <=>
start(s:States[システム名]) => as(s:States[システム名], s:States[システム名])
.."
を変数lslに格納する。
【０１０２】
（C4）文字列
"assert
conj2 <=>
(as(s:States[システム名], s':States[システム名])
∧      enabled(s:States[システム名], a:Actions[システム名])
∧      internal(a:Actions[システム名]))
=> (＼E a':Actions[システム名]
(enabled(s':States[システム名], a':Actions[システム名])
∧ internal(a':Actions[システム名])
∧ as(effect(s:States[システム名], a:Actions[システム名]),
effect(s':States[システム名], a':Actions[システム名]))))
.."
を変数stmpに格納する。
【０１０３】
さらに、関数呼出しappend(lsl, stmp)を実行し、結果
"assert
conj1 <=> 
start(s:States[システム名]) => as(s:States[システム名], s:States[システム名])
..
【０１０４】
assert
conj2 <=> 
(as(s:States[システム名], s':States[システム名])
∧ enabled(s:States[システム名], a:Actions[システム名])
∧ internal(a:Actions[システム名]))
=> (＼E a':Actions[システム名]
(enabled(s':States[システム名], a':Actions[システム名])
∧ internal(a':Actions[システム名])
∧ as(effect(s:States[システム名], a:Actions[システム名]),
effect(s':States[システム名], a':Actions[システム名]))))
.."
を内部変数lslに格納する。
【０１０５】
（C5）文字列
"assert
conj3 <=> 
(as(s:States[システム名], s':States[システム名])
∧ enabled(s:States[システム名], a:Actions[システム名])
∧ ("
を変数stmpに格納する。
【０１０６】
次に、関数呼出しappend(lsl, stmp)を実行し、結果
"assert
conj1 <=> 
start(s:States[システム名]) => as(s:States[システム名], s:States[システム名])
..
【０１０７】
assert
conj2 <=> 
(as(s:States[システム名], s':States[システム名])
∧ enabled(s:States[システム名], a:Actions[システム名])
∧ internal(a:Actions[システム名])
=> (＼E a':Actions[システム名]
(enabled(s':States[システム名], a':Actions[システム名])
∧ internal(a':Actions[システム名])
∧ as(effect(s:States[システム名], a:Actions[システム名]),
effect(s':States[システム名], a':Actions[システム名]))))
..
【０１０８】
assert
conj3 <=>
(as(s:States[システム名], s':States[システム名])
∧ enabled(s:States[システム名], a:Actions[システム名])
∧ ("
を内部変数lslに格納する。
【０１０９】
さらに、変数anonymの内容
("pressButton(A)", "pressButton(B)")
を変数ltmpに格納する。
【０１１０】
（C6）変数ltmpの内容
("pressButton(A)", "pressButton(B)")
がnil (空リスト)かを比較する。比較結果が偽（nilでない）なので、処理例（C7）に移る。
【０１１１】
（C7）文字列
"(a:Actions[システム名] ="
を変数stmpに格納する。次に、関数呼出しappend(lsl, stmp)を実行し、結果
"assert
conj1 <=>
start(s:States[システム名]) => as(s:States[システム名], s:States[システム名])
..
【０１１２】
assert
conj2 <=>
(as(s:States[システム名], s':States[システム名])
∧ enabled(s:States[システム名], a:Actions[システム名])
∧ internal(a:Actions[システム名]))
=> (＼E a':Actions[システム名]
(enabled(s':States[システム名], a':Actions[システム名])
∧ internal(a':Actions[システム名])
∧ as(effect(s:States[システム名], a:Actions[システム名]),
effect(s':States[システム名], a':Actions[システム名]))))
..
【０１１３】
assert
conj3 <=> 
(as(s:States[システム名], s':States[システム名])
∧ enabled(s:States[システム名], a:Actions[システム名])
∧ ((a:Actions[システム名] = "
を内部変数lslに格納する。
【０１１４】
さらに、関数呼出しcar(ltmp)を評価し、結果
"pressButton(A)"
を変数stmpに格納する。
【０１１５】
さらに、関数呼出しappend(lsl, stmp)を実行し、結果
"assert
conj1 <=> 
start(s:States[システム名]) => as(s:States[システム名], s:States[システム名])
..
【０１１６】
assert
conj2 <=>
(as(s:States[システム名], s':States[システム名])
∧ enabled(s:States[システム名], a:Actions[システム名])
∧ internal(a:Actions[システム名])
=> (＼E a':Actions[システム名]
(enabled(s':States[システム名], a':Actions[システム名])
∧ internal(a':Actions[システム名])
∧ as(effect(s:States[システム名], a:Actions[システム名],
effect(s':States[システム名], a':Actions[システム名]))))
..
【０１１７】
assert
conj3 <=>
(as(s:States[システム名], s':States[システム名])
∧ enabled(s:States[システム名], a:Actions[システム名])
∧ ((a:Actions[システム名] = pressButton(A)"
を内部変数lslに格納する。
【０１１８】
さらに、関数呼出しcdr(ltmp)を評価し、結果
("pressButton(B)")
を変数ltmpに格納する。
【０１１９】
さらに、文字列
") ∨"
を変数stmpに格納する。
【０１２０】
さらに、関数呼出しappend(lsl, stmp)を実行し、結果
"assert
conj1 <=> 
start(s:States[システム名]) => as(s:States[システム名], s:States[システム名])
..
【０１２１】
assert
conj2 <=>
(as(s:States[システム名], s':States[システム名])
∧ enabled(s:States[システム名], a:Actions[システム名])
∧ internal(a:Actions[システム名]))
=> (＼E a':Actions[システム名]
(enabled(s':States[システム名], a':Actions[システム名])
∧ internal(a':Actions[システム名])
∧ as(effect(s:States[システム名], a:Actions[システム名]),
effect(s':States[システム名], a':Actions[システム名]))))
..
【０１２２】
assert
conj3 <=>
(as(s:States[システム名], s':States[システム名])
∧ enabled(s:States[システム名], a:Actions[システム名])
∧ ((a:Actions[システム名] = pressButton(A)) ∨ "
を内部変数lslに格納する。さらに、処理例（C8）に移る。
【０１２３】
（C8）変数ltmpの内容
("pressButton(B)")
がnil (空リスト)かを比較する。比較結果が偽（nilでない）なので、処理例（C9）に移る。
【０１２４】
（C9）文字列
"(a:Actions[システム名] = "
を変数stmpに格納し、関数呼出しappend(lsl, stmp)を実行して結果を内部変数lslに格納し、関数呼出しcar(ltmp)を評価して結果を変数stmpに格納し、関数呼出しappend(lsl, stmp)を実行して結果を内部変数lslに格納し、関数呼出しcdr(ltmp)を評価して結果を変数ltmpに格納する。
【０１２５】
さらに、文字列
") ∨"
を変数stmpに格納する。
【０１２６】
さらに、関数呼出しappend(lsl, stmp)を実行して結果を内部変数lslに格納する。この結果、変数lslの内容は
"assert
conj1 <=>
start(s:States[システム名]) => as(s:States[システム名], s:States[システム名])
..
【０１２７】
assert
conj 2 <=> 
(as(s:States[システム名], s':States[システム名])
∧ enabled(s:States[システム名], a:Actions[システム名])
∧ internal(a:Actions[システム名])
=> (＼E a':Actions[システム名]
(enabled(s':States[システム名], a':Actions[システム名])
∧ internal(a':Actions[システム名])
∧ as(effect(s:States[システム名], a:Actions[システム名]),
effect(s':States[システム名], a':Actions[システム名])))
..
【０１２８】
assert
conj3 <=> 
(as(s:States[システム名], s':States[システム名])
∧ enabled(s:States[システム名], a:Actions[システム名])
∧ ((a:Actions[システム名] = pressButton(A)) ∨ (a:Actions[システム名] = pressButton(B)) ∨ "
であり、変数ltmpの内容はnilである。さらに、処理例（C10）に移る。
【０１２９】
（C10）変数ltmpの内容がnil(空リスト)かを比較する。比較結果が真（nilである）なので、処理例（C11）に移る。
【０１３０】
（C11）文字列
"false ))
=> (true "
を変数stmpに格納する。
【０１３１】
次に、関数呼出しappend(lsl, stmp)を実行し、結果
"assert
conj1 <=>
start(s:States[システム名]) => as(s:States[システム名], s:States[システム名])
..
【０１３２】
assert
conj2 <=>
(as(s:States[システム名], s':States[システム名])
∧ enabled(s:States[システム名], a:Actions[システム名])
∧ internal(a:Actions[システム名])
=> (＼E a':Actions[システム名]
(enabled(s':States[システム名], a':Actions[システム名])
∧ internal(a':Actions[システム名])
∧ as(effect(s:States[システム名], a:Actions[システム名]),
effect(s':States[システム名], a':Actions[システム名]))))
..
【０１３３】
assert
conj3 <=>
(as(s:States[システム名], s':States[システム名])
∧ enabled(s:States[システム名], a:Actions[システム名])
∧ ((a:Actions[システム名] = PressButton(A)) ∨ (a:Actions[システム名] = pressButton(B)) ∨ false))
=> (true"
を内部変数lslに格納する。
【０１３４】
さらに、変数anonymの内容
("pressButton(A)", "pressButton(B)")
を変数ltmpに格納する。
【０１３５】
（C12）変数ltmpの内容
("pressButton(A)", "pressButton(B)")
がnil(空リスト)かを比較する。比較結果が偽（nilでない）なので、処理例（C13）に移る。
【０１３６】
（C13）文字列
"∧ (enabled(s':States[システム名], アクション名)
∧ as(effect(s:States[システム名], a:Actions[システム名]),
effect(s':States[システム名], アクション名)))"
を変数stmpに格納する。
【０１３７】
次に、関数呼出しcar(ltmp)を評価し、結果
"pressButton(A)"
を変数stmp2に格納する。
【０１３８】
さらに、関数呼出しcdr(ltmp)を評価し、結果
("pressButton(B)")
を変数ltmpに格納する。
【０１３９】
さらに、関数呼出しreplace(stmp, "アクション名", stmp2)を実行し、結果
"∧ (enabled(s':States[システム名], pressButton(A))
∧ as(effect(s:States[システム名], a:Actions[システム名]),
effect(s':States[システム名], pressButton(A))))"
を内部変数stmpに格納する。
【０１４０】
さらに、関数呼出しappend(lsl, stmp)を実行し、結果
"assert
conj1 <=> 
start(s:States[システム名]) => as(s:States[システム名], s:States[システム名])
..
【０１４１】
assert
conj2 <=> 
(as(s:States[システム名], s':States[システム名])
∧ enabled(s:States[システム名], a:Actions[システム名])
∧ internal(a:Actions[システム名])
=> (＼E a':Actions[システム名]
(enabled(s':States[システム名], a':Actions[システム名])
∧ internal(a':Actions[システム名])
∧ as(effect(s:States[システム名], a:Actions[システム名]),
effect(s':States[システム名], a':Actions[システム名]))))
..
【０１４２】
assert
conj3 <=> 
(as(s:States[システム名], s':States[システム名])
∧ enabled(s:States[システム名], a:Actions[システム名])
∧ ((a:Actions[システム名] = pressButton(A)) ∨ (a:Actions[システム名] = pressButton(B)) ∨false))
=> (true ∧ (enabled(s':States[システム名], pressButton(A))
∧ as(effect(s:States[システム名], a:Actions[システム名]),
effect (s':States[システム名], pressButton(A))))"
を内部変数lslに格納する。さらに、処理例（C14）に移る。
【０１４３】
（C14）変数ltmpの内容
("pressButton(B)")
がnil (空リスト)かを比較する。比較結果が偽（nilでない）なので、処理例（C15）に移る。
【０１４４】
（C15）文字列
"∧ (enabled(s':States[システム名], アクション名)
∧ as(effect(s:States[システム名], a:Actions[システム名]),
effect(s':States[システム名], アクション名)))"
を変数stmpに格納し、関数呼出しcar(ltmp)を評価して結果を変数stmp2に格納し、関数呼出しcdr(ltmp)を評価して結果を変数ltmpに格納し、関数呼出しreplace(stmp, "アクション名", stmp2)を実行して結果を内部変数stmpに格納し、関数呼出しappend(lsl, stmp)を実行して結果を内部変数lslに格納する。
【０１４５】
この結果、変数lslの内容は
"assert
conj1 <=> 
start(s:States[システム名]) => as(s:States[システム名], s:States[システム名])
..
【０１４６】
assert
conj2 <=> 
(as(s:States[システム名], s':States[システム名])
∧ enabled(s:States[システム名], a:Actions[システム名])
∧ internal(a:Actions[システム名])
=> (＼E a':Actions[システム名]
(enabled(s':States[システム名], a':Actions[システム名])
∧ internal(a':Actions[システム名])
∧ as(effect(s:States[システム名], a:Actions[システム名]),
effect(s':States[システム名], a':Actions[システム名]))))
..
【０１４７】
assert
conj3 <=> 
(as(s:States[システム名], s':States[システム名])
∧ enabled(s:States[システム名], a:Actions[システム名])
∧ ((a:Actions[システム名] = pressButton(A)) ∨ (a:Actions[システム名] = pressButton(B)) ∨ false))
=> (true ∧ (enabled(s':States[システム名], pressButton(A))
∧ as(effect(s:States[システム名], a:Actions[システム名]),
effect(s':States[システム名], pressButton(A))))
∧ (enabled(s':States[システム名], pressButton(B))
∧ as(effect(s:States[システム名], a:Actions[システム名]),
effect(s':States[システム名], pressButton(B))))"
であり、変数ltmpの内容はnilである。さらに、処理例（C16）に移る。
【０１４８】
（C16）変数ltmpの内容がnil (空リスト)かを比較する。比較結果が真（nilである）なので、処理例（C17）に移る。
【０１４９】
（C17）文字列
")
.."
を変数stmpに格納する。
【０１５０】
さらに、関数呼出しappend(lsl, stmp)を実行し、結果
"assert
conj1 <=>
start (s:States[システム名]) => as(s:States[システム名], s:States[システム名])
..
【０１５１】
assert
conj2 <=> 
(as(s:States[システム名], s':States[システム名])
∧ enabled(s:States[システム名], a:Actions[システム名])
∧ internal(a:Actions[システム名]))
=> (＼E a':Actions[システム名]
(enabled(s':States[システム名], a':Actions[システム名])
∧ internal(a':Actions[システム名])
∧ as(effect(s:States[システム名], a:Actions[システム名]),
effect(s':States[システム名], a':Actions[システム名]))))
..
【０１５２】
assert
conj3 <=> 
(as(s:States[システム名], s':States[システム名])
∧ enabled(s:States[システム名], a:Actions[システム名])
∧ ((a:Actions[システム名] = pressButton(A)) ∨ (a:Actions[システム名] = pressButton(B)) ∨ false))
=> (true ∧ (enabled(s':States[システム名], pressButton(A))
∧ as(effect(s:States[システム名], a:Actions[システム名]),
effect(s':States[システム名], pressButton(A))))
∧ (enabled(s'States[システム名], pressButton(B))
∧ as(effect(s:States[システム名], a:Actions[システム名]),
effect(s':States[システム名], pressButton(B)))))
.."
を内部変数lslに格納する。
【０１５３】
（C18）文字列
"assert
conj4 <=> 
(as(s:States[システム名], s':States[システム名])
∧ enabled(s:States[システム名], a:Actions[システム名])"
を変数stmpに格納する。さらに、関数呼出しappend(lsl, stmp)を実行し、結果
"assert
conj1 <=> 
start(s:States[システム名]) => as(s:States[システム名], s:States[システム名])
..
【０１５４】
assert
conj2 <=> 
(as(s:States[システム名], s':States[システム名])
∧ enabled(s:States[システム名], a:Actions[システム名])
∧ internal(a:Actions[システム名])
=> (＼E a':Actions[システム名]
(enabled(s':States[システム名], a':Actions[システム名])
∧ internal(a':Actions[システム名])
∧ as(effect(s:States[システム名], a:Actions[システム名]),
effect(s':States[システム名], a':Actions[システム名])))
..
【０１５５】
assert
conj3 <=> 
(as(s:States[システム名], s':States[システム名])
∧ enabled(s:States[システム名], a:Actions[システム名])
∧ ((a:Actions[システム名] = pressButton(A)) ∨ (a:Actions[システム名] = pressButton(B)) ∨ false))
=> (true ∧ (enabled(s':States[システム名], pressButton(A))
∧ as(effect(s:States[システム名], a:Actions[システム名]),
effect(s':States[システム名], pressButton(A))))
∧ (enabled(s':States[システム名], pressButton(B))
∧ as(effect(s:States[システム名], a:Actions[システム名]),
effect(s':States[システム名], pressButton(B)))))
..
【０１５６】
assert
conj4 <=> 
(as(s:States[システム名], s':States[システム名])
∧ enabled(s:States[システム名], a:Actions[システム名])"
を内部変数lslに格納する。さらに、変数anonymの内容
("pressButton(A)", "pressButton(B)")
を変数ltmpに格納する。
【０１５７】
（C19）変数ltmpの内容
("pressButton(A)", "pressButton(B)")
がnil (空リスト)かを比較する。比較結果が偽（nilでない）なので、処理例（C20）に移る。
【０１５８】
（C20）文字列
"∧ ~(a:Actions[システム名] = "
を変数stmpに格納する。次に、関数呼出しappend(lsl, stmp)を実行し、結果
"assert
conj1 <=> 
start(s:States[システム名]) => as(s:States[システム名], s:States[システム名])
..
【０１５９】
assert
conj2 <=>
(as(s:States[システム名], s':States[システム名])
∧ enabled(s:States[システム名], a:Actions[システム名])
∧ internal(a:Actions[システム名]))
=> (＼E a':Actions[システム名]
(enabled(s':States[システム名], a':Actions[システム名])
∧ internal(a':Actions[システム名])
∧ as(effect(s:States[システム名], a:Actions[システム名]),
effect(s':States[システム名], a':Actions[システム名]))))
..
【０１６０】
assert
conj3 <=> 
(as(s:States[システム名], s':States[システム名])
∧ enabled(s:States[システム名], a:Actions[システム名])
∧ ((a:Actions[システム名] = pressButton(A)) ∨ (a:Actions[システム名] = pressButton(B)) ∨ false))
=> (true ∧ (enabled(s':States[システム名], pressButton(A))
∧ as(effect(s:States[システム名], a:Actions[システム名]),
effect(s':States[システム名], pressButton(A))))
∧ (enabled(s':States[システム名], pressButton(B))
∧ as(effect(s:States[システム名], a:Actions[システム名]),
effect(s':States[システム名], pressButton(B)))))
..
【０１６１】
assert
conj4 <=> 
(as(s:States[システム名], s':States[システム名])
∧ enabled(s:States[システム名], a:Actions[システム名])
∧ ~(a:Actions[システム名] = "
を内部変数lslに格納する。
【０１６２】
さらに、関数呼出しcar(ltmp)を評価し、結果
"pressButton(A)"
を変数stmpに格納する。
【０１６３】
さらに、関数呼出しcdr(ltmp)を評価し、結果
("pressButton(B)")
を変数ltmpに格納する。
【０１６４】
さらに、関数呼出しappend(lsl, stmp)を実行し、結果
"assert
conj1 <=> 
start(s:States[システム名]) => as(s:States[システム名], s:States[システム名])
..
【０１６５】
assert
conj2 <=> 
(as(s:States[システム名], s':States[システム名])
∧ enabled(s:States[システム名], a:Actions[システム名])
∧ internal(a:Actions[システム名])
=> (＼E a':Actions[システム名]
(enabled(s':States[システム名], a':Actions[システム名])
∧ internal(a':Actions[システム名])
∧ as(effect(s:States[システム名], a:Actions[システム名]),
effect(s':States[システム名], a':Actions[システム名]))))
..
【０１６６】
assert
conj3 <=> 
(as(s:States[システム名], s':States[システム名])
∧ enabled(s:States[システム名], a:Actions[システム名])
∧ ((a:Actions[システム名] = pressButton(A)) ∨ (a:Actions[システム名] = pressButton(B)) ∨ false))
=> (true ∧ (enabled(s':States[システム名], pressButton(A))
∧ as(effect(s:States[システム名], a:Actions[システム名]),
effect(s':States[システム名], pressButton(A))))
∧ (enabled(s':States[システム名], pressButton(B))
∧ as(effect(s:States[システム名], a:Actions[システム名]),
effect(s':States[システム名], pressButton(B)))))
..
【０１６７】
assert
conj4 <=> 
(as(s:States[システム名], s':States[システム名])
∧ enabled(s:States[システム名], a:Actions[システム名])
∧ ~(a:Actions[システム名] = pressButton(A)"
を内部変数lslに格納する。
【０１６８】
さらに、関数呼出しappend(lsl, ")")を実行し、結果
"assert
conj1 <=> 
start(s:States[システム名]) => as(s:States[システム名], s:States[システム名])
..
【０１６９】
assert
conj2 <=>
(as(s:States[システム名], s':States[システム名])
∧ enabled(s:States[システム名], a:Actions[システム名])
∧ internal(a:Actions[システム名])
=> (＼E a':Actions[システム名]
(enabled(s':States[システム名], a':Actions[システム名])
∧ internal(a':Actions[システム名])
∧ as(effect(s:States[システム名], a:Actions[システム名]),
effect(s':States[システム名], a':Actions[システム名]))))
..
【０１７０】
assert
conj3 <=> 
(as(s:States[システム名], s':States[システム名])
∧ enabled(s:States[システム名], a:Actions[システム名])
∧ ((a:Actions[システム名] = pressButton(A)) ∨ (a:Actions[システム名] = pressButton(B)) ∨ false))
=> (true ∧ (enabled(s':States[システム名], pressButton(A))
∧ as(effect(s:States[システム名], a:Actions[システム名]),
effect(s':States[システム名], pressButton(A))))
∧ (enabled(s':States[システム名], pressButton(B))
∧ as(effect(s:States[システム名], a:Actions[システム名]),
effect(s':States[システム名], pressButton(B)))))
..
【０１７１】
assert
conj4 <=>
(as(s:States[システム名], s':States[システム名])
∧ enabled(s:States[システム名], a:Actions[システム名])
∧ ~(a:Actions[システム名] = pressButton(A))"
を内部変数lslに格納する。さらに、処理例（C21）に移る。
【０１７２】
（C21）変数ltmpの内容
("pressButton(B)")
がnil (空リスト)かを比較する。比較結果が偽（nilでない）なので、処理例（C22）に移る。
【０１７３】
（C22）文字列
"∧ ~(a:Actions[システム名] = "
を変数stmpに格納し、関数呼出しappend(lsl, stmp)を実行して結果を内部変数lslに格納し、関数呼出しcar(ltmp)を評価して結果を変数stmpに格納し、関数呼出しcdr(ltmp)を評価して結果を変数ltmpに格納し、関数呼出しappend(lsl, stmp)を実行して結果を内部変数lslに格納し、関数呼出しappend(lsl, ")")を実行して結果を内部変数lslに格納する。
【０１７４】
この結果、変数lslの内容は
"assert
conj1 <=> 
start(s:States[システム名]) => as(s:States[システム名], s:States[システム名])
..
【０１７５】
assert
conj2 <=> 
(as(s:States[システム名], s':States[システム名])
∧ enabled(s:States[システム名], a:Actions[システム名])
∧ internal(a:Actions[システム名]))
=> (＼E a':Actions[システム名]
(enabled(s':States[システム名], a':Actions[システム名])
∧ internal(a':Actions[システム名])
∧ as(effect(s:States[システム名], a:Actions[システム名]),
effect(s':States[システム名], a':Actions[システム名]))))
..
【０１７６】
assert
conj3 <=> 
(as(s:States[システム名], s':States[システム名])
∧ enabled(s:States[システム名], a:Actions[システム名])
∧ ((a:Actions[システム名] = pressButton(A)) ∨ (a:Actions[システム名] = pressButton(B)) ∨ false))
=> (true ∧ (enabled(s':States[システム名], pressButton(A))
∧ as(effect(s:States[システム名], a:Actions[システム名]),
effect(s':States[システム名], pressButton(A))))
∧ (enabled(s':States[システム名], pressButton(B))
∧ as(effect(s:States[システム名], a:Actions[システム名]),
effect(s':States[システム名], pressButton(B)))))
..
【０１７７】
assert
conj4 <=> 
(as(s:States[システム名], s':States[システム名])
∧ enabled(s:States[システム名], a:Actions[システム名])
∧ ~(a:Actions[システム名] = pressButton(A))
∧ ~(a:Actions[システム名] = pressButton(B))"
であり、変数ltmpの内容はnilである。さらに、処理例（C23）に移る。
【０１７８】
（C23）変数ltmpの内容がnil(空リスト)かを比較する。比較結果が真（nilである）なので、処理例（C24）に移る。
【０１７９】
（C24）文字列
"∧ output(a:Actions[システム名]))
=> (enabled(s':States[システム名], a:Actions[システム名])
∧ as(effect(s:States[システム名], a:Actions[システム名]),
effect(s':States[システム名], a:Actions[システム名])))
.."
を変数stmpに格納する。
【０１８０】
さらに、関数呼出しappend(lsl, stmp)を実行し、結果
"assert
conj1 <=> 
start(s:States[システム名]) => as(s:States[システム名], s:States[システム名])
..
【０１８１】
assert
conj2 <=> 
(as(s:States[システム名], s':States[システム名])
∧ enabled(s:States[システム名], a:Actions[システム名])
∧ internal(a:Actions[システム名]))
=> (＼E a':Actions[システム名]
(enabled(s':States[システム名], a':Actions[システム名])
∧ internal(a':Actions[システム名])
∧ as(effect(s:States[システム名], a:Actions[システム名]),
effect(s':States[システム名], a':Actions[システム名]))))
..
【０１８２】
assert
conj3 <=> 
(as(s:States[システム名], s':States[システム名])
∧ enabled(s:States[システム名], a:Actions[システム名])
∧ ((a:Actions[システム名] = pressButton(A)) ∨ (a:Actions[システム名] = pressButton(B)) ∨ false))
=> (true ∧ (enabled(s':States[システム名], pressButton(A))
∧ as(effect(s:States[システム名], a:Actions[システム名]),
effect(s':States[システム名], pressButton(A))))
∧ (enabled(s':States[システム名], pressButton(B))
∧ as(effect(s:States[システム名], a:Actions[システム名]),
effect(s':States[システム名], pressButton(B)))))
..
【０１８３】
assert
conj4 <=> 
(as(s:States[システム名], s':States[システム名])
∧ enabled(s:States[システム名], a:Actions[システム名])
∧ ~(a:Actions[システム名] = pressButton(A))
∧ ~(a:Actions[システム名] = pressButton(B))
∧ output(a:Actions[システム名])
=> (enabled(s':States[システム名], a:Actions[システム名])
∧ as(effect(s:States[システム名], a:Actions[システム名]),
effect(s':States[システム名], a:Actions[システム名])))
.."
を内部変数lslに格納する。
【０１８４】
（C25）文字列
"assert
as(s:States[システム名], s':States[システム名])
<=> ("
を変数stmpに格納する。
【０１８５】
次に、関数呼出しappend(lsl, stmp)を実行し、結果
"assert
conj1 <=> 
start(s:States[システム名]) => as(s:States[システム名], s:States[システム名])
..
【０１８６】
assert
conj2 <=> 
(as(s:States[システム名], s':States[システム名])
∧ enabled(s:States[システム名], a:Actions[システム名])
∧ internal(a:Actions[システム名]))
=> (＼E a':Actions[システム名]
(enabled(s':States[システム名], a':Actions[システム名])
∧ internal(a':Actions[システム名])
∧ as(effect(s:States[システム名], a:Actions[システム名]),
effect(s':States[システム名], a':Actions[システム名]))))
..
【０１８７】
assert
conj3 <=> 
(as(s:States[システム名], s':States[システム名])
∧ enabled(s:States[システム名], a:Actions[システム名])
∧ ((a:Actions[システム名] = pressButton(A)) ∨ (a:Actions[システム名] = pressButton(B)) ∨ false ))
=> (true ∧ (enabled(s':States[システム名], pressButton(A))
∧ as(effect(s:States[システム名], a:Actions[システム名]),
effect(s':States[システム名], pressButton(A))))
∧ (enabled(s':States[システム名], pressButton(B))
∧ as(effect(s:States[システム名], a:Actions[システム名]),
effect(s':States[システム名], pressButton(B)))))
..
【０１８８】
assert
conj4 <=>
(as(s:States[システム名], s':States[システム名])
∧ enabled(s:States[システム名], a:Actions[システム名])
∧ ~(a:Actions[システム名] = pressButton(A))
∧ ~(a:Actions[システム名] = pressButton(B))
∧ output(a:Actions[システム名]))
=> (enabled(s':States[システム名], a:Actions[システム名])
∧ as(effect(s:States[システム名], a:Actions[システム名],
effect(s':States[システム名], a:Actions[システム名])))
..
【０１８９】
assert
as(s:States[システム名], s':States[システム名])
<=> ("
を内部変数lslに格納する。
【０１９０】
さらに、関数呼出しappend(lsl, as)を実行し、結果
"assert
conj1 <=> 
start(s:States[システム名]) => as(s:States[システム名], s:States[システム名])
..
【０１９１】
assert
conj2 <=> 
(as(s:States[システム名], s':States[システム名])
∧ enabled(s:States[システム名], a:Actions[システム名])
∧ internal(a:Actions[システム名])
=> (＼E a':Actions[システム名]
(enabled(s':States[システム名], a':Actions[システム名])
∧ internal(a':Actions[システム名])
∧ as(effect(s:States[システム名], a:Actions[システム名]),
effect(s':States[システム名], a':Actions[システム名]))))
..
【０１９２】
assert
conj3 <=> 
(as(s:States[システム名], s':States[システム名])
∧ enabled(s:States[システム名], a:Actions[システム名])
∧ ((a:Actions[システム名] = pressButton(A)) ∨ (a:Actions[システム名] = pressButton(B)) ∨ false ))
=> (true ∧ (enabled(s':States[システム名], pressButton(A))
∧ as(effect(s:States[システム名], a:Actions[システム名]),
effect(s':States[システム名], pressButton(A))))
∧ (enabled(s':States[システム名], pressButton(B))
∧ as(effect(s:States[システム名], a:Actions[システム名]),
effect, (s':States[システム名],  pressButton(B)))))
..
【０１９３】
assert
conj4 <=> 
(as(s:States[システム名], s':States[システム名])
∧ enabled(s:States[システム名], a:Actions[システム名])
∧ ~(a:Actions[システム名] = pressButton(A))
∧ ~(a:Actions[システム名] = pressButton(B))
∧ output(a:Actions[システム名]))
=> (enabled(s':States[システム名], a:Actions[システム名])
∧ as(effect(s:States[システム名], a:Actions[システム名]),
effect(s':States[システム名], a:Actions[システム名])))
..
【０１９４】
assert
as(s:States[システム名], s':States[システム名])
<=> (((s:States[システム名].quarter = s':States[システム名].quarter)
∧ ((s:States[システム名].pc = s':States[システム名].pc)
∨ (s:States[システム名].pc = jazz ∧ s':States[システム名].pc = rock)
∨ (s:States[システム名].pc = rock ∧ s':States[システム名].pc = jazz)))"
を内部変数lslに格納する。
【０１９５】
さらに、文字列
")
.."
を変数stmpに格納する。
【０１９６】
さらに、関数呼出しappend(lsl, stmp)を実行し、結果
"assert
conj1 <=> 
start (s:States[システム名]) => as(s:States[システム名], s:States[システム名])
..
【０１９７】
assert
conj2 <=> 
(as(s:States[システム名], s':States[システム名])
∧ enabled(s:States[システム名], a:Actions[システム名])
∧ internal(a.-Actions[システム名]))
=> (＼E a':Actions[システム名]
(enabled(s':States[システム名], a':Actions[システム名])
∧ internal(a':Actions[システム名])
∧ as(effect(s:States[システム名], a:Actions[システム名]),
effect(s':States[システム名], a':Actions[システム名]))))
..
【０１９８】
assert
conj3<=> 
(as(s:States[システム名], s':States[システム名])
∧ enabled(s:States[システム名], a:Actions〔システム名])
∧ ((a:Actions[システム名] = pressButton(A)) ∨ (a:Actions[システム名] = pressButton(B)) ∨ false ))
=> (true ∧ (enabled(s':States[システム名], pressButton(A))
∧ as(effect(s:States[システム名], a:Actions[システム名]),
effect(s':States[システム名], pressButton(A))))
∧ (enabled(s':States[システム名], pressButton(B))
∧ as(effect(s:States[システム名], a:Actions[システム名]),
effect(s':States[システム名], pressButton(B)))))
..
【０１９９】
assert
conj4 <=> 
(as(s:States[システム名], s':States[システム名])
∧ enabled(s:States[システム名], a:Actions[システム名])
∧ ~(a:Actions[システム名] = pressButton(A))
∧ ~(a:Actions[システム名] = pressButton(B))
∧ output(a:Actions[システム名]))
=> (enabled(s':States[システム名], a:Actions[システム名])
∧ as(effect(s:States[システム名], a:Actions[システム名]),
effect(s':States[システム名], a:Actions[システム名])))
..
【０２００】
assert
as(s:States[システム名], s':States[システム名])
<=> (((s:States[システム名].quarter = s':States[システム名].quarter)
∧ ((s:States[システム名].pc = s':States[システム名].pc)
∨ (s:States[システム名].pc = jazz ∧ s':States[システム名].pc = rock)
∨ (s:States[システム名].pc = rock ∧ s':States[システム名].pc = jazz))))
.."
を内部変数lslに格納する。
【０２０１】
（C26）文字列
"prove
conj1 ∧ conj2 ∧ conj3 ∧ conj4
.."
を変数stmpに格納する。
【０２０２】
さらに、関数呼出しappend(lsl, stmp)を実行し、結果
"assert
conj1 <=> 
start(s:States[システム名]) => as(s:States[システム名], s:States[システム名])
..
【０２０３】
assert
conj2 <=> 
(as(s:States[システム名], s':States[システム名])
∧ enabled(s:States[システム名], a:Actions[システム名])
∧ internal(a:Actions[システム名]))
=> (＼E a':Actions[システム名]
(enabled(s':States[システム名], a':Actions[システム名])
∧ internal(a':Actions[システム名])
∧ as(effect(s:States[システム名], a:Actions[システム名]),
effect(s':States[システム名], a':Actions[システム名]))))
..
【０２０４】
assert
conj3 <=> 
(as(s:States[システム名], s':States[システム名])
∧ enabled (s:States[システム名], a:Actions[システム名])
∧ ((a:Actions[システム名] = pressButton(A)) ∨ (a:Actions[システム名] = pressButton(B) ∨ false))
=> (true ∧ (enabled(s':States[システム名], pressButton(A))
∧ as(effect(s:States[システム名], a:Actions[システム名]),
effect(s':States[システム名], pressButton(A))))
∧ (enabled(s':States[システム名], pressButton(B))
∧ as(effect(s:States[システム名], a:Actions[システム名]),
effect(s':States[システム名], pressButton(B)))))
..
【０２０５】
assert
conj4 <=> 
(as(s:States[システム名], s':States[システム名])
∧ enabled(s:States[システム名], a:Actions[システム名])
∧ ~(a:Actions[システム名] = pressButton(A))
∧ ~(a:Actions[システム名] = pressButton(B))
∧ output(a:Actions[システム名])
=> (enabled(s':States[システム名], a:Actions[システム名])
∧ as(effect(s:States[システム名], a:Actions[システム名]),
effect(s':States[システム名], a:Actions[システム名])))
..
【０２０６】
assert
as(s:States[システム名], s':States[システム名])
<=> (((s:States[システム名].quarter = s':States[システム名].quarter)
∧ ((s:States[システム名].pc = s':States[システム名].pc)
∨ (s:States[システム名].pc = jazz ∧ s':States[システム名].pc = rock)
∨ (s:States[システム名].pc = rock ∧ s':States[システム名].pc = jazz))))
..
【０２０７】
prove
conj1 ∧ conj2 ∧ conj3 ∧ conj4
.."
を内部変数lslに格納する。
【０２０８】
（C27）関数呼出しreplace(lsl, "システム名", sys)を実行し、結果
"assert
conj1 <=> 
start(s:States[Jukebox]) => as(s:States[Jukebox], s:States[Jukebox])
..
【０２０９】
assert
conj2 <=> 
(as(s:States[Jukebox], s':States[Jukebox])
∧ enabled(s:States[Jukebox], a:Actions[Jukebox])
∧ internal(a:Actions[Jukebox]))
=> (＼E a':Actions[Jukebox]
(enabled(s':States[Jukebox], a':Actions[Jukebox])
∧ internal(a':Actions[Jukebox])
∧ as(effect(s:States[Jukebox], a:Actions[Jukebox]),
effect(s':States[Jukebox], a':Actions[Jukebox]))))
..
【０２１０】
assert
conj3<=> 
(as(s:States[Jukebox], s':States[Jukebox])
∧ enabled(s:States[Jukebox], a:Actions[Jukebox])
∧ ((a:Actions[Jukebox] = pressButton(A)) ∨ (a:Actions[Jukebox] = pressButton(B)) ∨ false ))
=> (true ∧ (enabled(s':States[Jukebox], pressButton(A))
∧ as(effect(s:States[Jukebox], a:Actions[Jukebox]),
effect(s':States[Jukebox], pressButton(A))))
∧ (enabled(s':States[Jukebox], pressButton(B))
∧ as(effect(s:States[Jukebox], a:Actions[Jukebox]),
effect(s':States[Jukebox], pressButton(B)))))
..
【０２１１】
assert
conj4 <=> 
(as(s:States[Jukebox], s':States[Jukebox])
∧ enabled(s:States[Jukebox], a:Actions[Jukebox])
∧ ~(a:Actions[Jukebox] = pressButton(A))
∧ ~(a:Actions[Jukebox] = pressButton(B))
∧ output(a:Actions[Jukebox]))
=> (enabled(s':States[Jukebox], a:Actions[Jukebox])
∧ as(effect(s:States[Jukebox], a:Actions[Jukebox]),
effect(s':States[Jukebox], a:Actions[Jukebox])))
..
【０２１２】
assert
as(s:States[Jukebox], s':States[Jukebox])
<=> (((s:States[Jukebox].quarter = s':States[Jukebox].quarter)
∧ ((s:States[Jukebox].pc = s':States[Jukebox].pc)
∨ (s:States[Jukebox].pc = jazz ∧ s':States[Jukebox].pc = rock)
∨ (s:States[Jukebox].pc = rock ∧ s':States[Jukebox].pc = jazz))))
..
【０２１３】
prove
conj1 ∧ conj2 ∧ conj3 ∧ conj4
.."
を内部変数lslに格納する。
【０２１４】
（C28）関数呼出しwrite(lsl, "tmpFile")を実行し、新規ファイル"tmpFile"を作成して、内部変数lslに格納された文字列
"assert
conj1 <=> 
start(s:States[Jukebox]) => as(s:States[Jukebox], s:States[Jukebox])
..
【０２１５】
assert
conj2 <=> 
(as(s:States[Jukebox], s':States[Jukebox])
∧ enabled(s:States[Jukebox], a:Actions[Jukebox])
∧ internal(a:Actions[Jukebox]))
=> (＼E a':Actions[Jukebox]
(enabled(s':States[Jukebox], a':Actions[Jukebox])
∧ internal(a':Actions[Jukebox])
∧ as(effect(s:States[Jukebox], a:Actions[Jukebox]),
effect (s':States[Jukebox], a':Actions[Jukebox]))))
を書き込む。
【０２１６】
［実施例：匿名性検査装置1全体］
次に、図１の匿名性検査装置1の処理内容の詳細を処理例（E1）〜（E4）として具体的に説明する。
【０２１７】
匿名性検査装置1全体の実行の詳細を述べる。以下では、動作記述言語による記述として記述例D101を、匿名動作のリストとして記述例D104を、匿名性保証の条件の性質記述言語による記述として記述例D105を、匿名性検査装置に与えたときの実行を示す。
【０２１８】
（E1）プリプロセッサによって、「動作記述言語による記述(記述例D101)」「匿名動作のリスト(記述例D104)」および「匿名性保証の条件の性質記述言語による記述(記述例D105)」から、性質記述言語による記述である検証命題8（図９）
"assert
conj1 <=> 
start(s:States[Jukebox]) => as(s:States[Jukebox], s:States[Jukebox])
..
【０２１９】
assert
conj2 <=> 
(as(s:States[Jukebox], s':States[Jukebox])
∧ enabled(s:States[Jukebox], a:Actions[Jukebox])
∧ internal(a:Actions[Jukebox]))
=> (＼E a':Actions[Jukebox]
(enabled(s':States[Jukebox], a':Actions[Jukebox])
∧ internal(a':Actions[Jukebox])
∧ as(effect(s:States[Jukebox], a:Actions[Jukebox]),
effect(s':States[Jukebox], a':Actions[Jukebox]))))
..
【０２２０】
assert
conj3 <=> 
(as(s:States[Jukebox], s':States[Jukebox])
∧ enabled(s:States[Jukebox], a:Actions[Jukebox])
∧ ((a:Actions[Jukebox] = pressButton(A)) ∨ (a:Actions[Jukebox] = pressButton(B)) ∨ false ))
=> (true ∧ (enabled(s':States[Jukebox], pressButton(A))
∧ as(effect(s:States[Jukebox], a:Actions[Jukebox]),
effect(s':States[Jukebox].pressButton(A))))
∧ (enabled(s':States[Jukebox], pressButton(B))
∧ as(effect(s:States[Jukebox], a:Actions[Jukebox]),
effect(s':States[Jukebox], pressButton(B)))))
..
【０２２１】
assert
conj4 <=> 
(as(s:States[Jukebox], s':States[Jukebox])
∧ enabled(s:States[Jukebox], a:Actions[Jukebox])
∧ ~(a:Actions[Jukebox] = pressButton(A))
∧ ~(a:Actions[Jukebox] = pressButton(B))
∧ output(a:Actions[Jukebox]))
=> (enabled(s':States[Jukebox], a:Actions[Jukebx])
∧ as(effect(s:States[Jukebox], a:Actions[Jukebox]),
effect(s':States[Jukebox], a:Actions[Jukebox])))
..
【０２２２】
assert
as(s:States[Jukebox], s':States[Jukebox])
<=> (((s:States[Jukebox].quarter = s':States[Jukebox].quarter)
∧ ((s:States[Jukebox].pc = s':States[Jukebox].pc)
∨ (s:States[Jukebox].pc = jazz ∧ s':States[Jukebox].pc = rock)
∨ (s:States[Jukebox].pc = rock ∧ s':States[Jukebox].pc = jazz))))
..
【０２２３】
prove
conj1 ∧ conj2 ∧ conj3 ∧ conj4
.."
が得られる。これは、一時記憶ファイルtmpFile（ファイル9）に格納される。
【０２２４】
ここで、上記の検証命題8の性質記述言語によって記述される内容において、検査項目(as)の定義はユーザによって予め与えられるものであり、proveは上述したように検査開始命令である。以下、検査項目（conj1〜4）の内容について説明する。
【０２２５】
conj1にはシステム初期状態の場合の検査項目が示されている。
「状態sがシステム初期状態である」
ならば、
「s 自身が検査項目(as)を満たす」
【０２２６】
conj2には内部命令（＝非通信命令）が実行される場合の検査項目が示されている。
「システム状態sで命令aが実行可能(enabled(s,a))で、
命令aが内部命令（internal）で、
システム状態s とs'が検査項目 as を満たす」
ならば、
「システム状態s'である内部命令a'が実行可能で、
s で命令a を実行した直後のシステム状態(effect(s,a))と
s' で命令 a'を実行した直後のシステム状態(effect(s',a'))が
検査項目 as を満たす」
【０２２７】
conj3には通信命令のうち、匿名命令を実行する場合の検査項目が示されている。
「システム状態sで命令aが実行可能（enabled(s,a)）で、
命令a が匿名命令（pressButton(A)またはPressButton(B)）で、
システム状態s とs'が検査項目asを満たす」
ならば、
「システム状態s'では、すべての匿名命令
(pressButton(A)およびpressButton(B))
が実行でき、
s で命令aを実行した直後のシステム状態(effect(s,a))と
s'で命令pressButton(A)を実行した直後のシステム状態
(effect(s', pressButton(A)))が
検査項目asを満たし、
s で命令aを実行した直後のシステム状態(effect(s,a))と
s'で命令pressButton(B)を実行した直後のシステム状態
(effect(s', pressButton(B)))が
検査項目asを満たす」
【０２２８】
conj4には匿名命令以外の通信命令を実行する場合の検査項目が示されている。
「システム状態sで命令aが実行可能（enabled(s,a)）で、
命令a が匿名命令以外の通信命令(output(a))で、
システム状態s とs'が検査項目asを満たす」
ならば、
「システム状態s'で命令aが実行できて、
s で命令aを実行した直後のシステム状態(effect(s,a))と
s'で命令aを実行した直後のシステム状態(effect(s',a))が
検査項目asを満たす」
【０２２９】
（E2）一方、動作記述言語による記述から性質記述言語による記述への変換装置3(本例では、IOA-Toolkitを用いる)によって、「動作記述言語による記述(記述例D101)」から、記述D103
"start(s:States[Jukebox])
<=> (s:States[Jukebox].pc = start ∧ s:States[Jukebox].quarter = 1);
【０２３０】
internal(insertCoins(qt : NonZeroNat ));
enabled(s:States[Jukebox], insertCoins(qt:NonZeroNat))
<=> s:States[Jukebox].pc = start;
effeet(s:States[Jukebox], insertCoins(qt:NonZeroNat)).quarter = qt:NonZeroNat;
effect(s:States[Jukebox], insertCoins(qt:NonZeroNat)).pc = button;
【０２３１】
output(pressButton(id:AorB));
enabled(s:States[Jukebox], pressButtondd:AorB))
<=> s:States[Jukebox].pc = button;
effect(s:States[Jukebox], pressButtondd:AorB)).quarter = s:States[Jukebox].quarter;
effect(s:States[Jukebox], pressButton(id:AorB)).pc
= (if (id:AorB = A)  then jazz else rock);
【０２３２】
output(playMusic);
enabled(s:States[Jukebox], playMusic) <=> 
((s:States[Jukebox].pc = jazz ∨ s:States[Jukebox].pc = rock)
∧ s:States[Jukebox].quarter ~= 1);
effect(s:States[Jukebox], playMusic).quarter = s:States[Jukebox].quarter - 1;
effect(s:States[Jukebox], playMusic).pc = s:States[Jukebox].pc;
【０２３３】
internal(playJazz);
enabled(s:States[Jukebox], playJazz)
<=> (s:States[Jukebox].pc = jazz ∧ s:States[Jukebox].quarter = 1);
effect(s:States[Jukebox], playJazz).quarter = s:States[Jukebox].quarter;
effect(s:States[Jukebox], playJazz).pc = stop;
【０２３４】
internal(playRock);
enabled(s:States[Jukebox], playRock)
<=> (s:States[Jukebox].pc = rock ∧ s:States[Jukebox].quarter = 1);
effect(s:States[Jukebox], playRock).quarter = s:States[Jukebox].quarter;
effect(s:States[Jukebox], playRock).pc = stop;"
【０２３５】
が得られる。これは、IOA-Toolkitによって、一時記憶ファイル（tmpFile2と名付ける)としてファイル10に記憶される。
【０２３６】
（E3）仕様検証装置4(本例では、Larch Proverを用いる)によって、ファイル9及びファイル10に記憶されているファイルtmpFileとtmpFile2の内容が読み込まれ、ユーザ11のコマンド操作によって、匿名性の検証が行われる。
【０２３７】
（E4）上記の結果、記述例D101の仕様が匿名性を満たすならば真が、そうでなければ偽が得られる。
【０２３８】
以上説明したように、本実施の形態によれば、定理証明器からなる仕様検証装置4によって動作記述言語で仕様が記述さえた分散システムに対する匿名性の検証を行うことが可能となる。
【０２３９】
なお、本発明の実施の形態は上記に限られず例えばファイル9及び10等の各構成を分離、統合したり、通信回線を介して分散することなどが適宜可能である。また、本発明を構成する計算機プログラムは計算機読み取り可能な記録媒体や通信回線を介して提供することが可能である。
【図面の簡単な説明】
【０２４０】
【図１】本発明の匿名性検査装置の実施の形態の構成を示すブロック図。
【図２】図１の匿名性検査装置1における動作記述言語と性質記述言語の構文定義を示す図。
【図３】図１の仕様の動作記述言語による記述5の記述例（D101）を示す図。
【図４】図１の匿名性検査装置1で用いられる性質記述言語による記述の記述例（D102）を示す図。
【図５】図３の仕様の動作記述言語による記述5の記述例（D101）を、図１の動作記述言語による記述から性質記述言語による記述への変換装置3によって変換した性質記述言語による記述D103を示す図。
【図６】図１の匿名動作のリスト6の記述例（D104）を示す図。
【図７】図１の匿名性保証の条件の性質記述言語による記述例（D105）を示す図。
【図８】図１のプリプロセッサ2の処理内容を示すフローチャート。
【図９】図１の検証命題8の一例を示す図。
【図１０】背景としたモデル検査技術に基づく匿名性検査装置の構成図。
【符号の説明】
【０２４１】
１  匿名性検査装置
２  プリプロセッサ
３  動作記述言語による記述から性質記述言語による記述への変換装置
４  仕様検査用装置（定理証明器）
５  分散システムの仕様の動作記述言語による記述
６  匿名動作のリスト
７  匿名性の保証条件の性質記述言語による記述
８  検証命題
【図１】
2006293633.tif 000003
【図２】
2006293633.tif 000004
【図３】
2006293633.tif 000005
【図４】
2006293633.tif 000006
【図５】
2006293633.tif 000007
【図６】
2006293633.tif 000008
【図７】
2006293633.tif 000009
【図８】
2006293633.tif 000010
【図９】
2006293633.tif 000011
【図１０】
2006293633.tif 000012