UML モデルのシミュレーション実行

4章で説明した通り、OCLの事前/事後条件より振舞いに関する情報を取得する。これ はクラスのメソッドの事前/事後条件を振舞仕様における操作演算に関する等式として反 映させることである。これらの等式を左辺から右辺への書換え規則とみなせば仕様は項書 換えシステムとして捉えることができ、操作演算を繰り返し適用した項をリダクションす ることによって実行に相応することを行う。この際、CafeOBJの処理系を利用すれば計 算機による自動的な実行を行うことができる。CafeOBJの処理系を用いてリダクション を行うには、redコマンドを使用する。

先にも説明した通り、クラス図におけるスナップショットはクラス図から生成すること のできる、ある状態である。クラスに対応する隠蔽ソートはそのクラスの状態空間を現 すソートであり、ある時点でのスナップショットを項として表現することができる。ある Classに対してメソッドoperation1、operation2を順に適用した時点でのスナップショット は次の項によって表現することができる。

operation2(operation1(C : Class)) -- hidden sort of Class

では、例を用いてクラス図+OCLのシミュレーション実行について説明する。まず第4 章で説明した例題(2)を用いて説明する。

UML

expense-sheet

price : Integer = 0 card? : Boolean = false

setPrice(I : Integer)

customer

pocket : Integer = 0 setPocket(I : Integer)

order

1 1

図 4.3: クラス図: シミュレーション実行例(1)

図4.3のクラス図において、まず客の所持金が5000円で明細書の額が3000円である場 合のスナップショットを考え、このスナップショットをsnapshot1と名づける。snapshot1 は、次の項によって表現できる。

setPrice(3000,setPocket(5000,init-order)) -- snapshot1

この際、このスナップショットにおける各クラスの属性値をリダクションを行うことで次 のように取り出すことができる。

CafeOBJ> open ORDER

-- opening module ORDER.. done.

%ORDER> red card?(setPrice(3000,setPocket(5000, init-order))) . false : Bool

次に、snapshot1から明細書の額が7000円に更新された場合のスナップショットを考え る。このスナップショットをsnapshot2と名づける。snapshot2は次の項によって表現で きる。

setPrice(7000,setPrice(3000,setPocket(5000,init-order))) -- snapshot2

同様にしてリダクションによりクラスの属性値を次のように取り出す。

%ORDER> red card?(setPrice(7000,setPrice(5000,setPocket(5000,init-order)))) . false : Bool

%ORDER> red price(setPrice(7000,setPrice(5000,setPocket(5000,init-order)))) . 7000 : NzNat

次に、snapshot2から所持金が10000円に増えた場合のスナップショットを考え、これ をsnapshot3と名づける。snapshot3は次の項によって表現される。

setPocket(10000,setPrice(7000,setPrice(3000,setPocket(5000,init-order)))) -- snapshot3 同様にしてリダクションによりクラスの属性値を次のように取り出す。

%ORDER> red card?(setPocket(10000,setPrice(7000,setPrice(3000, setPocket(5000,init-order))))) . false : Bool

%ORDER> red pocket(setPocket(10000,setPrice(7000,setPrice(3000, setPocket(5000,init-order))))) . 10000 : NzNat

以上のようにシミュレーション実行を行う。

e1 :: Expense-sheet card? = false price = 3000

c1 :: Customer pocket = 5000

snapshot1

: setPrice(3000,setPocket(5000,init-order))

e1 :: Expense-sheet card? = true price = 7000

c1 :: Customer pocket = 5000 snapshot2

: setPrice(7000,setPrice(3000, setPocket(5000,init-order))

e1 :: Expense-sheet card? = false price = 7000

c1 :: Customer pocket = 10000 snapshot3

: setPocket(10000,setPrice(7000,setPrice(3000, setPocket(5000,init-order))

図 4.4: シミュレーション実行例(1)

OCLの事前/事後条件は等式として記述したが、これらの制約が正しいかどうかは以上 のようにシミュレーション実行してみることで調べることができる。