状態遷移図の段階的構築のための論理的基盤

Vol.0 No.0 情報処理学会論文誌 ¹⁹⁵⁹

状態遷移図の段階的構築のための論理的基盤

青 木 利 晃

^y;yy

片 山 卓 也

^y

本稿では，証明された正しい事実から，正しい状態遷移図を段階的に構築する手法と，それを扱う ための論理的基盤を提案する．また，簡単な例をもとに，その利点と問題点について議論する．

Foundations for Stepwise Construction of State Transition Mo dels

Toshiaki Aoki y;yy

and Takuya Katayama y

Inthispap er,weprop osefoundationstostepwiseconstructcorrectstatetransitionmo d-

elsfrompre-provedfacts. Then, wediscusstheiradvantagesandproblemsbasedonsimple

examples.

1. は じ め に

オブジェクト指向分析モデルは，属性やメソッド な どの概念を含んでいるため，本質的に，無限の状態を 含んでいる．その検証アプローチとしては，大きく分 けて，²種類ある．¹つ目は，対象となるモデルを抽 象化などにより有限空間に押えて，モデル検査等の自 動検証を適用するものである．²つ目は，無限状態を 述語論理を用いて直接的に記述し，定理証明システム を用いて対話的に検証を行う．

我々は，後者のアプローチにより，オブジェクト指 向分析モデルの検証法^8),14)，および，定理証明システ ム^HOL4)を用いた検証支援法^12),13)を提案してきた．

このアプローチの問題点の¹つは，その検証コストが 大きいことである．対話的な検証では，述語論理の推 論規則を，自然数やリストといったデータ型に関する 定理や定義に適用することにより，目的の事実を導く．

そのため，どの推論規則をどの定理^/定義に適用すれ ば良いか迷うことが多く，また，対話的な操作による 時間的コストも大きい．

この問題を解決するため，我々は，ADA(Assertion

Driven Approach) とい う手法を提案している．

ADAは²つの活動，⁽¹⁾領域ライブラリの構築，⁽²⁾ 正しいモデルの段階的構築，により構成される．

(1)領域ライブラリの構築^: 同一の領域に属するシス

y北陸先端科学技術大学院大学

JapanAdvancedInstituteofScienceandTechnology

yy科学技術振興事業団 さきがけ研究²¹

PRESTO,JapanScienceandTechnologyCorp oration

テムの開発では，用いる語彙が同じ場合が多い．オブ ジェクト指向分析モデルでは，語彙はユーティリティ クラス⁽データ型⁾として表現できる．そこで，対象領 域に出現する語彙や概念をクラス図により整理し，そ れらに関する正しい事実を定理として蓄積する．これ を，本手法では，領域ライブラリと呼ぶことにする．

特定のシステムの分析モデル作成の際，領域ライブラ リに蓄積されたデータ型や定理を用いることにより，

証明を再利用することができる．

(2)正しいモデルの段階的構築^: 検証で行う対話的 推論は，原理的に，モデル構築と同様のものである．

我々が提案した検証手法では，構築したモデルの検証 は，それを構築する際曖昧に考えていたことを，形式 化し証明することに対応していた．^ADAでは，モデ ル構築を行う際，⁽¹⁾で蓄積された事実を用いて，その 正しさを保証しながら構築を行う．これにより，モデ ル構築の早期に誤りを発見^/修正することができ，結 果的に，バックトラックコストを低く押えることが可 能になる．

(1)は，定理証明システムにおける抽象データ型に 関する扱いを拡張することにより扱うことができるこ とがわかった．そこで，本稿では，⁽²⁾について，そ の論理的基盤の提案と考察を行う．本稿の構成は次の とおりである．²節では，状態遷移図と領域ライブラ リを形式的に定義する．³節では，領域ライブラリに 蓄積されている正しい事実から，状態遷移図を段階的 に構築する手法を示す．⁴節では，提案した手法を簡 単な事例に適用して考察を行い，問題点と今後の課題 を明らかにする．

IPSJ SIG Technical Report

2003／7／17

−21−

2. 状態遷移図と領域ライブラリ

我々が対象としているオブジェクト指向分析モデル は，クラスとステートチャート図により構成される．

クラス毎に¹つのステートチャート図が割り当てられ ており，そのクラスから実体化されるオブジェクトの 振舞を記述する．よって，状態遷移図の集合が，この ようなモデルの本質である．以下では，状態遷移図の 集合の段階的構築に焦点を当てる．

2.1 状態遷移図の概要

本研究では，図¹のような状態遷移図を対象とする．

この図では，²つの状態遷移図が定義されており，イ ベントを用いて協調動作している．

個々の状態遷移は，ラベル^{e[cond]=e0action}を持つ．

ここで，^eは入力イベント，^e0は出力イベント，^cond は遷移条件，^actionはアクションを表現している．遷 移の前状態において，イベント^eを受け取り，^condが 成立しているならば，^actionを実行して，イベント^e0 を出力することを意味する．アクションは属性評価と 属性への代入を表現する式，遷移条件は真偽値を返す 属性評価と論理演算子により構成される式である．そ れぞれ，アクション式，遷移条件式と呼ぶことにする．

状態とイベントは属性に関する表明を持つ．状態の 表明は，その状態で，イベントの表明は，そのイベン トが発生する時に，成立する性質を表現している．図

1では，状態^S1は表明^0n<100を持っている．こ れは，その状態では，常に，属性ⁿの値は⁰以上¹⁰⁰ 未満であるべきということを表現している．また，イ ベント^{l og}は表明^{0 l og :v 100}を持つ．これは，

イベント^logの属性^vは，常に，⁰以上¹⁰⁰未満であ るべきということを表現している．

以上の表明は，成立すべき性質を書き留めておくも のである．属性の計算法や状態遷移図により規定され た振舞により，それが成立しない場合もありうる．状 態とイベントの表明が，任意の状態遷移図の振舞で，

常に，成立する時，その状態遷移図は正しい，と呼ぶ ことにする．

2.2 状態遷移図の意味論

以上で説明した状態遷移図とその意味を形式的に定 義する．

定義^2.1 システム

複数の状態遷移図から構成されるシステムを，以下の

Sy stemにより定義する．

$ H>Q @ORJY Q QORJY Q

UHVHWORJY Q ORJY H>Q@ORJY

Q QORJY Q

$ Q

Q +ÿ ≤Q

$ ORJY OLVW ORJY OLVW

∀[∈OLVW≤[≤

OLVW >@

fa®z ¨k

ORJ

≤ORJY≤

図¹ 状態遷移図

System=(Atr;STS;E;AssnE)

whereAtr:属性識別子の集合，

STS :状態遷移図の集合，

E:イベント識別子の集合，

AssnE:E!Pr ed(Atr )

ここで，^{Pr ed(Atr )}は^Atrの属性を自由変数とする述 語論理式である

^☆

．また，入力^/出力イベントが無いこ とを表現する特別なイベントをで表現し，^2Eで あるものとする．

STSの要素である状態遷移図は，以下で定義される．

定義^2.2 状態遷移図

(Atr;S;C ;A;T;t0;s0;s01;a0;Assn)

where

Atr:属性識別子の集合，^S:状態識別子の集合，

C:遷移条件式の集合，^A:アクション式の集合，

T S2E2E2C2A2S，

t02T;s02S;s012S;a02A;

Assn:S!Pr ed(Atr );Assn(s01)=Tr ue;

t

0

=(s

01

;;;Tr ue;a

0

;s

0 );

以上の定義で，^s0は初期状態を表現している．初期 状態では，属性に初期値が設定されているものとする．

初期設定はアクション^a0で行われる．また，その他 の状態遷移によるアクションと初期設定のためのアク ションを同様に扱うため，初期化前の状態を表現する

s01と，初期設定アクションを実行する状態遷移^t0を 導入した．

次に，属性が持つ値を表現するために，属性の環境 を定義する．

定義^2.3 属性環境

システムの属性が持つ値は，以下の領域と値域を持つ 関数により表現する．

:Atr

1

81118Atr

n

8Atr!Value

☆

述語論理式なので，属性を表現する自由変数の他に，述語変数 も使うことができる

ここで，^{Atr1;111;Atrn}は^STSの要素である状態遷 移図の属性集合であり，^Atrは^{Sy stem}の属性集合で

ある．^{Val ue}は，属性が持つことができる値の集合で

ある．

個々の状態遷移と表明の関係を表現 するために ， 表明付き状態遷移という概念を導入する．一般形は

fAge=e 0

fBgfPg[c]afQgである．^e;e0;c;aは，それ ぞれ，入力イベント，出力イベント，遷移条件，アク ションである．^{A;B;P ;Q}は表明である．遷移前に，

入力イベントに関して^A，状態において^Pが成立して いた時，この状態遷移が発火すると，遷移後に出力イ ベントに関して^B，状態に関して^Qが成立すること を表現している．

表明付き状態遷移が正しいことは，状態遷移に関す る最弱事前条件^(weakest pre-conditions)

1)を用 いて定義する．個々の状態遷移は，遷移条件が成立す れば，アクション，すなわち，属性評価と属性への代 入，を行うので，基本的に，ループ無しの手続き型言 語と等価である．手続き型言語の最弱事前条件は，す でに，良く知られているため，本稿では，それらにつ いては証明しない．

定理^2.1 状態遷移の最弱事前条件

状態遷移^{e[c]=e0 a}の イベント^e0に関する事後条件

B，状 態 に 関 する 事後 条 件 ^Q の 最 弱事 前 条 件 を

w p(e[c]=e 0

a;B;Q)と書く．アクション^aが，^a1 :=

t1;111;an:=tnである時，^{w p(e[c]=e0a;B;Q)}は以下 である．ただし，^t1

;111;t

nは属性へのメソッド 適用を 行う式である．

w p(e[c]=e 0

a;B;Q)=

c)((B^Q)[t

1

=a

1 ]111[t

n

=a

n ])

定義^2.4 表明付き状態遷移の正しさ

表明付き状態遷移^{at=fAge=e0fB gfPg[c]afQg}が 正しい^(valid)時，^j=atと書き，以下で定義する．

j=fAge=e 0

fBgfPg[c]afQg,

<j=8:[[A]]^[[B]])[[wp(e[c]=e 0

a;B ;Q)]]

ここで，^[[X]]は，^Xに出現するすべての属性識別子

aを ^(a)に，メソッド をそれが表現する実際の関数 に置き換えた式を表現している．^<は属性が持つ値や メソッド を表現する関数の理論を表現している．この ように，表明付き状態遷移の正しさは，値や関数の世 界を用いて定義される．以下では，表明の記述とその ような世界を区別する必要が無いかいぎり^[[]]を省略 する．

最後に，状態遷移図とシステムの正しさの定義を与

える．

定義^2.5 状態遷移図の正しさ 状態遷移図^{ST =(Atr;S;C;A;T;t}0

;s

0

;s

01

;a

0

;Assn)

が正しい時，^j=STと書き，以下で定義する．

j=ST, 8(s1;e;e 0

;c;a;s2)2T:

j=fAssnE(e)ge=e 0

fAssnE(e 0

)g

fAssn(s1)g[c]afAssn(s2)g

定義^2.6 システムの正しさ

システム^{Sy stem=(Atr;STS;E;AssnE)}が正しい 時，^{j=Sy stem}と書き，以下のように定義する．

j=Sy stem,8ST 2STS:j=ST

2.3 領域ライブラリ

領域ライブラリは，データ型とそれに関する定理の 集合である．図²に，汎用カウンタの領域ライブラリ の例を示す．クラス^Counterがデータ型を表現してい る．メソッド^incと^decにより，カウンタのインクリ メント，および，デクリメントを行い，^<，^>などの メソッド によりカウンタの値の検査を行う．カウンタ の値は属性^numberにより表現されており，内部に隠 蔽されている．このようなクラスのことを，データ型 クラスと呼ぶことにし，スレテオタイプhhD ataty p eii

で表現する．データ型クラスは抽象データ型と見なす ことができ，定理証明システム^HOLにも，それを扱 うためのメカニズムがある．また，オブジェクト指向 特有の，オブジェクトの状態，継承などの概念も，そ のメカニズムを少し拡張すれば取扱可能である．

クラス^{Counter (}データ型⁾から実体化されるオブ ジェクト⁽値⁾の性質は，ステレオタイプhhPr oper ty ii

を持つ²つのクラス^LTE(c)，^GTE(c)により定義さ れている．これらのクラスからはオブジェクトは実体 化されず，成立する性質，すなわち，定理のみを定義 している．このようなクラスを性質クラスと呼ぶこと にする．性質クラスでは，特定の用途に使われる定理 群をまとめる．個々の定理は，データ型の内部属性は 直接は操作しないため，そのインターフェースである メソッド の適用に関して記述することになる．これは，

イベント通信を含まない表明付き状態遷移に対応して いる．性質クラスには，このような表明付き状態遷移 の集合を定義することにする．

定義^2.7 イベント無し表明付き状態遷移 アクション^a，遷移条件^cから構成されるイベント通 信を含まない表明付き状態遷移を，^fPg[c]afQgと記 述する．ここで，^Pは事前条件，^Qは事後条件である．

この表明付き状態遷移が正しい時，^j=fPg[c]afQgと 書き，以下により定義する．

Counter <<Datatype>>

number new inc dec =, <, >, ≤, ≥

âªfa®z c 1fa®zU ÞN"D1oò

c1fa®zU ÞN"D1oò {True}[n=c−1]n:=n.inc(){n=c}

{True}[n<c−1]n:=n.inc(){n<c}

{True}[n<c]n:=n.inc(){n≤c}

{n≤c}n:=n.dec(){n<c}

LTE(c) <<Property>>

n:Counter

{True}[n=c+1]n:=n.dec(){n=c}

{True}[c+1<n]n:=n.dec(){c<n}

{True}[c<n]n:=n.dec(){c≤n}

{c≤n}n:=n.inc() {c<n}

GTE(c) <<Property>>

n:Counter

図² 領域ライブラリ

j=fPg[c]afQg,<j=8:[[P]])[[wp([c]a;Q)]]

最弱事前条件^{w p([c]a;Q)}は，アクション^aが，^a1:=

t

1

;111;a

n :=t

nである時，以下である．

w p([c]a;Q)=c)(Q[t

1

=a

1 ]111[t

n

=a

n ])

領域ライブラリは，正しいイベント無し表明付き状 態遷移の集合により定義する．

定義^2.8 領域ライブラリ

領域ライブラリ^{D O M}を，以下により定義する．

D O MPow (ffPg[c]afQgj

j=fPg[c]afQg;c:条件式^;a:アクション式^;

P ;Q:データ型クラスのオブジェクトに関する述語^g) 図²では，クラス^LTE(c)とクラス^GTE(c)におい て，それぞれ，^c以下のカウンタ，^c以上のカウンタ を実現するための正しいイベント無し表明付き状態遷 移群が書かれている．

3. 状態遷移図の段階的構築

3.1 状態遷移の追加

ADAにおける状態遷移図の段階的構築では，正しい 状態遷移図に，領域ライブラリに蓄積されている正しい 表明付き状態遷移を追加することにより，次の段階の正 しい状態遷移図を作成する．図³にその概要を示す．左 上の^{Sy stem}の状態遷移図^STiの状態^{sr c}から^dstに 正しい表明付き状態遷移^{fEge=ffFgfPg[c]afQg}を追 加する場合である．まず，^{a)E;F ;P ;Q}と^AssnE(e),

AssnE(f),Assn(sr c),Assn(dst)が，それぞれ，同 じになるよう調整する．そして，^{b)sr c}から^dstに状 態遷移を追加する．

a) に お い て 表 明 の 調 整 を 行 う際 ，表 明 を 変 更 し た と し て も ，そ れ ぞ れ の 正 し さ は 保 存 さ れ な け れ ば な ら な い ．す な わ ち ，以 下 条 件 を 満 た す

VUF GVW 67 L

$VVQVUF $VVQGVW

H I

6\VWHP

$VVQ(H $VVQ(I H>F@I D

3 4

VUF GVW 67 L ’

3 ’ 4 ’

H I

6\VWHP’

( ’ ) ’

H>F@I D

3’

4 ’ ( ’ ) ’

H I

67 L ’

3 ’ 4 ’

H I

6\VWHP’

( ’ ) ’ VUF GVW

H>F@I D

, -

( )

H I

図³ 状態遷移図の段階的構築法

表 明 ^E0;F0;P0;Q0を 見 付 け る 必 要 が あ る ．た だ し ，^{Sy stem = (Atr;STS;E;AssnE)}，^STi

=

(Atr

i

;S

i

;C

i

;A

i

;T

i

; t

0i

;s

0i

;;s

01i

;a

0i

;Assn

i ) であ る．

(1) j=fE 0

ge=ffF 0

gfP 0

g[c]afQ 0

g

(2) j=(Atr;STS[ST 0

i

=STi];AssnE 0

)

whereAssnE 0

=AssnE](e;E 0

)](f;F 0

);

ST 0

i

=(Atr

i

;S

i

;C

i

;A

i

;T

i

;t

0i

;s

0i

;s

01i

;a

0i

;Assn 0

i );

Assn 0

i

=Assni](sr c;P 0

)](dst;Q 0

)

A](a;b)は，関数^Aの値域の値^aからの写像を，^a から^bの写像で上書きすることを表現している．

(1)は，表明付き状態遷移の表明を調整したとして も，その正しさは保たれなければならないことを表現 している．⁽²⁾は，状態遷移図において状態遷移を接 続する状態の表明を調整したとしても，状態遷移図の 正しさは保たれなければならないことを表現している．

3.2 正しさの保存

3.2.1 表明付き状態遷移の正しさの保存

表 明 付 き 状 態 遷 移 ^{fEge=ffFgfPg[c]afQg} を ，

fE 0

ge=ffF 0

gfP 0

g[c]afQ 0

gに変更する場合，遷移条 件^cやアクション^aの内容に立ち入るべきではない．

ADAでは，個々の表明付き状態遷移の正しさを領域 ライブラリ作成時に証明する．そして，個々の状態遷 移図作成時において，その証明を再利用することを狙 いとしている．そのため，表明を変更する際，遷移条 件やアクションに関する証明をやり直すことは避ける べきである．

以上の方針から，^{j=fEge=ffFgfPg[c]afQg111(1)} を前提にして，^{j=fE0ge=ffF0gfP0g[c]afQ0g111(2)} であるような^E0;F0;P0;Q0を求めることになる．

(1)と⁽²⁾は，表明付き状態遷移の定義を用いる と，それぞれ，^{E^P )w p(e=f [c]a;F ;Q)111(3)}，

E 0

^F 0

)w p(e=f [c]a;F 0

;Q 0

)111(4)である．遷移 条件やアクションに立ち入らないとすると，⁽³⁾の左 辺と右辺を，それぞれ，強めたり弱めたりすることに より⁽⁴⁾を求めることになる．すなわち，以下の²つ の条件を満たす^E0;F0;P0;Q0ならば⁽²⁾が成立する．

(i) E 0

^P 0

)E^P

(ii) w p(e=f [c]a;F ;Q))w p(e=f [c]a;F 0

;Q 0

)

(ii) は最弱事前条件の性質を用いて，^{F ^Q )}

F 0

^Q 0

111(ii 0

)と簡略化できる．よって，⁽¹⁾から，

(i)と⁽ⁱⁱ⁰⁾を満たすような，^E0;F0;P0;Q0を見付ける ことにより，正しさを保存して⁽²⁾へと変更できる．

3.2.2 状態遷移図の正しさの保存

状態遷移図の表明を，その正しさを保存するように 変更するのは，表明付き状態遷移の場合ほど簡単では ない．図⁴の例を考える．ただし，問題を簡略化する ためイベントは省略してある．この例では，左側の状 態遷移図の状態^s3から状態^s1に，ⁿの値を²減じる 状態遷移を追加する．この遷移を追加するためには，

状態^s3の表明を^{0 n 100}から^{2 n100}に 変更しなければならない．この変更を行 うと，さら に，^s2の表明も変更する必要がある．状態^s2の表明

0 n <100は，^s3への状態遷移後，^s3の変更後の 表明を導くには弱すぎるためである．言い替えると，

0n<100)w p(n:=n+1;2n100)が成立 しないためである．よって，以上のような^s3の表明の 変更は，^s2の表明を^1n<100に変更することを要 求する．^s1の表明に関しては，^s2への状態遷移後，^s2 の新たな表明を導くことができるので変更する必要が 無い．

図⁴の例から分かるように，状態遷移図のある状態 の表明の変更は，他の状態の表明の変更を引き起こす 場合がある．このことを，表明の変更伝搬と呼ぶこと

Q ₁ Q _m

P ₁

P _n

R

...

...

Q ₁ P ₁

P _n

R’

...

[b 1 ]a 1

[b _n ]a _n

[c 1 ]d 1 [c _m ]d _m

...

Q _m [b ₁ ]a ₁ [b _n ]a _n

[c ₁ ]d ₁ [c m ]d m

5

5 3 6 6 ₂ 5

5 ₃ 6 6 ₂

7 7

図⁵ 表明変更の一般形

にする．表明の変更伝搬は，最悪の場合，それまで作 成してきたすべての状態遷移に関して表明の正しさを 再度考え直すことが必要になるため，なるべく避ける べきである．以下では，表明の変更伝搬を発生させな い仕組みについて考察を行う．

図⁵は，状態遷移図のある状態の表明を変更する場 合の一般形である．小文字の記号は状態名を，大文字 の記号はそれぞれに対応する表明を表現している．こ こでも，問題を簡略化するためにイベントを扱わない が，それを含む場合も本質的には同様である．

左の状態遷移図の状態^rの表明^Rを，右の状態遷移 図のとおり^R0に変更する場合を考える．左の状態遷 移図は変更する前のものなので，正しいと仮定する．

よって，以下の²つの事実が成立している．

81in:Pi)w p([bi]ai;R)111(5)

81im:R)w p([ci]di;Qi)111(6)

一方，右側の状態遷移図では，以下の²つの事実が 成立しなければならない．

81in:P

i

)w p([b

i ]a

i

;R 0

)111(7)

81im:R 0

)w p([ci]di;Qi)111(8)

(5)から⁽⁷⁾を導くためには，^R)R0が，⁽⁶⁾から⁽⁸⁾ を導くためには^R0)Rが成立していれば良い．よっ て，^R,R0となり，他の状態の表明を変更せずに^R を変更することができないことになる．

(5)と⁽⁷⁾は状態^rへ入る状態遷移に，⁽⁶⁾と⁽⁸⁾は 状態^rから出て行く状態遷移に関するものである．よっ て，状態^rへ入る状態遷移しか無い場合は，新たな^R0 は^R)R0が，状態^rから出て行く状態遷移だけの場 合は，^R0)Rが成立する^R0に変更可能である．

まとめると，状態遷移図の状態^rの表明^Rを表明の 変更伝搬を発生させずに変更するためには，新たな表 明^R0が以下の条件を満たしていれば良い．

(iii) 状態^rへ入る遷移のみの時，^R)R0

(iv ) 状態^rから出て行く遷移のみの時，^R0)R

0≤n<99 0≤n<100

8 8 8

n:=0 [n<98]

n:=n+1

[n<99]

n:=n+1 n:=n+1 0≤n≤100

n:=n+1 Q Q−

≤Q≤

≤Q

0≤n<99

1≤n<100

8 8 8

n:=0 [n<98]

n:=n+1

[n<99]

n:=n+1 n:=n+1

2≤n≤100 n:=n+1 Q Q−

û÷1A«`Ñ

JN A«` ÂA«`Ñ

図⁴ 表明の変更伝搬

(v ) 状態^rから出る遷移，入る遷移がある時，^R,

R 0

以上では，イベントを含まない状態遷移図について 議論してきたが，イベントに関しても同様である．イ ベント^eの表明^Eを^E0に変更する時，^E0が満たすべ き条件は以下である．

(v i) eが出力 イベントとしてのみ使用されている

時，^E)E0．

(v ii) eが入力イベントとしてのみ使用されている

時，^E0)E．

(v iii) eが入力イベント，及び，出力イベントとし

て使用されている時，^E0)E．

4. 例 と 考 察

4.1 段階的構築の例

図²の領域ライブラリを用いて，イベント^e+でイン クリメント，イベント^e0でデクリメントされ，値が

0以上¹⁰⁰以下になるカウンタの状態遷移図を作成し てみる．また，カウンタの値が変更された時，他の状 態遷移図がその変更を記録ものとする．

4.1.1 表明付き状態遷移の変形

まず，図²の^LTEの^cを¹⁰⁰に，^GTEの^cを⁰に 特化した定理群を用いる．この例では，⁰以上¹⁰⁰以 下のカウンタを作成したいので，これらを合成する必 要がある．

例えば，⁰から¹⁰⁰未満まで インクリメントして くループを作るために，クラス^LTEの^{fTr ueg[n<}

99]n :=n:inc()fn < 100gとクラス^GTEの^f0

ngn:=n:inc()f0<ngを組み合わせる必要がある．

最弱事前条件の性質と表明付き状態遷移の定義を用い れば，以下の手順で組み合わせることができる．

(1)fTr ueg[n<99]n:=n:inc()fn<100g^

f0ngn:=n:inc()f0<ng=

(2)fn<99gn:=n:inc()fn<100g^

f0ngn:=n:inc()f0<ng=

(3)f0n_n<99gn:=n:inc()f0<n<100g)

(4)f0n<99gn:=n:inc()f0<n<100g=

(5)f0ng[n<99]n:=n:inc()f0<n<100g

(1)から⁽²⁾では，遷移条件^{[n < 99]}を事前条件 に移動している．⁽²⁾から⁽³⁾では，最弱事前条件 に関する性質と述語論理の事実を使っている．前者 は，任意のアクション^aと事後条件^{P ;Q}に対して

w p(a;P)^w p(q ;Q)=w p(a;P^Q)が成立する，後 者は，^{(P )R )^(Q )R) =(P _Q)R)}が成 立というものである．⁽³⁾から⁽⁴⁾では，^{(P _Q)}

R ))(P^Q)R )が成立するという事実を使って いる．最後に，⁽⁴⁾から⁽⁵⁾では，事前条件の一部を 遷移条件に移動させている．

また，以上のような合成だけでなく，追加や分解と いった変形も必要である．例えば，ⁿの値を他の状態 遷移図で記録させる場合，⁽⁵⁾で作成した表明付き状 態遷移にイベントを送信するアクションを以下のよう に追加する必要がある．

fTr uege+=ef0<e:a<100g

f0ng[n<99]n:=n:inc();e:a:=nf0<n<100g

領域ライブラリに蓄積されている表明付き状態遷移 群は，対象システムの要件を満たすように変形するこ とになる．これは，分析活動の¹つと見なすべきであ る．以上では，表明付き状態遷移の定義や最弱事前条 件の性質を使って変形を行ったが，これらは分析活動 に沿った変形規則⁽性質合成規則，イベント導入規則，

などのように⁾として定義すべきである．

≤

∀∈ ≤

≤

≤

≤

≤

−

≤

≤

₋ −

!

"

#

$ %

≤ ≤

図⁶ 段階的構築の例

4.1.2 状態遷移の追加

まず，初期アクションとして属性ⁿにデータ型クラ

ス^Counterの新規オブジェクトを代入し，初期状態を

作成する．そして，この初期状態から状態遷移と状態 を段階的に追加する．また，各々の段階で状態に割り 当てる表明は，⁰ⁿ¹⁰⁰を導くようなものでなけ ればならない．常に，⁰以上¹⁰⁰以下であるカウンタ を作りたいからである．

図⁶に，²つの状態遷移図の段階的構築の各ステッ プを示した．

ステップ^1: 初期化アクション^{n:=newCounter ()} と初期状態^s1を導入する．図²には記述していないが，

newメソッド に関して，^{fTr uegn:=newCounter ()}

fn=0gが成立する．よって，^s1ではⁿ⁼⁰が成立し ている．

ステップ^2: 合成した⁽⁵⁾を用いて⁰から¹⁰⁰未満 までインクリメントするループを作る．⁽⁵⁾の前状態 と後状態を状態^s1に接続したいため，以下の³つの 条件を満たす表明^Pと^Bを発見する．^Pは，新たな，

状態^s1の表明と⁽⁵⁾の状態に関する事前^/事後条件に，

Bはイベント^eの表明にするものである．

8

>

<

>

:

P)0n

0<n<100^0<e:a<100)P^B

n=0)P

これらは，^3.2節で示した条件^{(i);(ii0);(iii)}である．

0 n <100は^Pの，^0<e:a<100は^Bの解であ る．そこで，ステップ²の状態^s1の表明とイベント^e

の表明をこれらそれぞれに変更して，状態遷移を追加 する．

ステップ²から⁵においても，同様に，状態遷移を 追加できる．ステップ⁵までで，^e+と^e0から構成さ れ，値が⁰以上¹⁰⁰以下になるような任意のイベント 列を受理する状態遷移図となった．そこで，次に，値 を記録する状態遷移図を作成する．ステップ⁶では，

新たな状態遷移図を追加している．ここでは，データ 記録のためのデータ型に関する領域ライブラリを用い ているが，その詳細は本稿では省略する．

4.2 考 察

以上のようにすれば，状態遷移の接続に関連する表 明を変更しながら，それを追加することにより，表明 の変更伝搬が発生させずに正しい状態遷移図を作成す ることができる．しかしながら，各ステップにおいて 変更する表明によっては，もはや状態遷移を追加でき ない状況に陥る場合がある．例えば，ステップ³にお いて，状態^s2の表明を⁰ⁿ¹⁰⁰とすると，ステッ プ⁴において，状態^s2から状態^s1への状態遷移を追 加できなくなってしまう．^s1のⁿが⁰以上という性質 を，デクリメントのアクション後，この表明から導け ないためである．これは，本質的に，表明の変更伝搬 と同様の問題である．このような問題が発生する原因 は，各状態の表明として，その状態で成立する一番強 い性質ではなく，それより弱いものを割り当てること ができるからである．

図⁵について，再度，考察を行う．^3.2.2節で示した 条件^{(iii);(iv);(v)}は，いずれも，表明^Rを^R0に変更

したとしても状態遷移図の正しさが保存されるための 十分条件である．表明^Rを^R0に変更する際，他の表 明^P1

111P

n

;Q

1

;111;Q

mがどのようなものであっても 構わなくするため，十分条件となっている．しかしな がら，十分条件であるがために，表明^R0がこれらの 条件を満たしていなくても，状態遷移図が正しい場合 がある．つまり，正しさが保存されるのに，状態遷移 が追加できない状況が生じるのである．

次に，^{(iii);(iv );(v )}が必要十分条件になる状況につ いて考える．図⁵の場合，以下の性質が成立していれ ば，これらの条件のいずれも，必要十分条件になる．

(81in:w p([bi]ai;R),Pi)^

(81im:w p([c

i ]d

i

;Q

i ),R )

この状況は，各々の状態に割り当てる表明が，その状 態で成立する最も強いものであることを意味している．

最も強い表明を，各々のステップで発見するのは非常 に難しい．将来どのような遷移を追加するか等も考慮 しなければならないからである．

よって，状態遷移が追加できない状況に陥った場合，

最小限の表明変更の伝搬を行うことが現実的である と考えている．関連する研究として，各状態における 不変表明の自動生成に関する研究がある⁵⁾⁷⁾．これ らの手法の基礎は^ForwardPropagationと^Backward

Propagationと呼ばれるものである．^{ForwardPropa-}

gationでは，最強事後条件^(strongestp ost-condition)

を用いて，偽^(False)から出発し，各状態遷移の最強 事後条件の和^(_)を求めていく．そして，その最小不 動点が，個々の状態で最も強い表明となる．^Backward

Propagationでは，個々の状態の弱い表明から出発し，

それらと各状態遷移の最弱事前条件の積^{(^)}を取るこ とにより，段階的に表明を強くしてく手法である．こ のような手法では，不動点の検査を行うことは一般に 決定不能問題であり，また，近似的に求めるにしても 大規模な状態遷移図ではその計算量が問題である．以 上の文献⁵⁾⁷⁾では，それらの様々な解決策が議論され ている．^BackwardPropagationでは，各状態の弱い 表明を段階的に強くしていくため，同様の手法により 表明の変更伝搬を行うことが有効であると考えており，

現在，検討中である．

5. ま と め

本稿では，正しい状態遷移図を段階的に構築する手 法とその論理的基盤を提案した．本手法では，正しい 状態遷移図に，領域ライブラリに蓄積されている正し い表明付き状態遷移を追加することにより，次の段階

の正しい状態遷移図を作成する．また，簡単な例に適 用して，その問題点を明らかにした．今後の課題は，

第一に，表明付き状態遷移の変形規則の提案，第二に，

適切な表明の変更伝搬手法の提案である．

参 考 文 献

1) E.W.Dijkstra:A Discipline of Programming,

PrenticeHall,1976.

2) C.Morgan:Programming from Specications,

PrenticeHall,1990.

3) R-J.BackandJ.Wright:RenementCalculus

-ASystematicIntroduction,Springer,1998.

4) University of Cambridge Computer Lab ora-

tory: The HOL System Description, revised

edition,1991.

5) A.Tiwari, et.al.: A Technique for Invariant

Generation,ToolsandAlgorithmsfortheCon-

structionandAnalysisofSystems,2001.

6) N.Bjorner, A.Browne and Z.Manna: Auto-

maticGenerationofInvariantsandIntermedi-

ateAssertions,TheoreticalComputerScience,

1997.

7) S.Bensalem,Y.LakhnechandH.Saidi:Power-

ful Techniques for the Automatic Generation

of Invariants, Conference onComputer-Aided

Verication,1996.

8) T.Aoki,T.TateishiandT.Katayama:AnAx-

iomaticFormalizationofUMLMo dels,Practi-

calUML-Based Rigorous Development Meth-

o ds,pp.13-28,2001.

9) T.Aoki and T.Katayama: Prototype Execu-

tion of Indep endently Constructed Object-

Oriented Analysis Mo del, Automating the

Object-OrientedSoftwareDevelopmentMeth-

o ds,pp.25-33,2001.

10) T.Aoki,T.Katayama:UnicationandConsis-

tency Verication of Object-Oriented Analy-

sis Mo dels, Asia-Pacic Software Engineering

Conference'98,pp.296{303,1998

11) 青木利晃^, 片山卓也^: オブジェクト指向方法論 のための形式的モデル^,日本ソフトウェア科学会 学会誌 コンピュータソフトウェア^{Vol.16 No.1,}

pp.12{32,1999.

12) 青木利晃^,立石 孝彰^,片山卓也^:定理証明技術の オブジェクト指向分析への適用，日本ソフトウェア 科学会学会誌 コンピュータソフトウェア^,Vol.18

No.4,pp.18{47,2001.

13) 青木利晃，片山卓也^:オブジェクト指向分析モデ ルの検証支援環境^,第¹⁹回 日本ソフトウェア科 学会 全国大会論文集^{(CD-ROM),2002.}

14) 立石孝彰，青木利晃，片山卓也^:振舞い近似手法 を用いたステートチャートに対する不変性の検証，

情報処理学会論文誌⁴⁴巻⁶号，^2003.