8.4 MSSS の適用例
8.4.4 変数名統一
8.4.3項のマッチングでは図8.15で示したレンタカーシステムの細分化モデルRentC6
に対してそれぞれ図8.14の部品CG5がマッチした．この節では6.2.3項で示した変数名 統一手順に沿って部品CG5 の実装依存モデルと細分化実装の変数名をRentC6の変数名
第8章 手法適用例 118
RentC5の事前条件より GroupC3の事前条件が厳しい limit : NAT1
maxCar : 1..10000 maxUser : 1..10000
rent : POW(0..maxCar * 0..maxUser) dom(rent) : POW(0..maxCar) dom(rent~) : POW(0..maxUser) (rent~;rent):POW(id(0..maxUser))
!(user).(user : dom(rent~) =>
card(rent~[{user}]) <= limit) car : 0..maxCar
user : 0..maxUser
card(rent~[{user}]) + 1 <= limit not(car : dom(rent))
not(user = rent(car)) rent := rent <+ {car |-> user}
パラメタ制約
不変条件
事前条件
代入
limit : NAT1 &
maxPerson : 1..10000 &
maxGroup : 1..10000
belong : POW((0..maxPerson) * (0..maxGroup)) dom(belong) : POW(0..maxPerson)
dom(belong~) : POW(0..maxGroup) (belong~;belong):POW(id(0..maxGroup))
!(group).(group:dom(belong~) =>
card(belong~[{group}]) <= limit) person : 0..maxPerson &
group : 0..maxGroup &
max(dom(belong))+1 <= maxPerson &
card(belong~[{group}]) + 1 <= limit &
not(person : dom(belong)) &
not(group = belong(person))
belong := belong <+ {person |-> group}
パラメタ制約
不変条件
事前条件
代入
図 8.17: 細分化モデルRentC5と細分化モデルGroupC3間のマッチング に置換する．図8.18に部品CG5と部品CG5に変数名置換を適用した結果を示す．
モデル実装間変数対応付けとして部品CG5は (belong, belong i.value) を持つ．まず，
部品CG5の細分化モデルGroupC5の変数名を置換する．これは細分化モデルGroupC5 の変数名を登場順に細分化モデルRentC6に書き換えることで行う．これにより，limit, maxPerson, maxGroup, belong, userがそれぞれlimit, maxCar, maxUser, rent, car に置 換される．次に実装依存モデルGroupC5 dの変数名を置換する．実装依存モデルの変数 名置換は細分化モデルの変数名置換と同様に置換を行った上で，細分化モデルに存在し ない変数名に対して部品名をプレフィックスとすることで部品毎に固有の変数名を与え る．GroupC5 d では変数fileOpen がGroupC5に存在しない変数であるため，fileOpen
を GroupC5 fileOpen に置換する．また，細分化実装に現れるモデル変数に対しても実
装依存モデルの変数名置換を適用する．次に細分化実装の変数名を置換する．細分化実装 の変数名は‘輸入で生じる変数’，‘細分化実装のCONCRETE VARIABLESで宣言される 変数’，‘局所変数’ に分類される．‘輸入で生じる変数’ には belong i.val が該当する．部 品CG5はモデル実装間変数対応付けとして (belong, belong i.value)を持ち，モデル変数 belong は rent に置換されるため，モジュールの別名belong i をrent i に置換する．こ れにより，belong i.valは rent i.val になる．部品CG5は局所変数を持たないため，局所 変数名の置換は生じない．以上により部品CG5の実装依存モデルと細分化実装は図8.18 の部品CG50 のようになる．
同様に細分化モデルRentC7にマッチする図8.14の部品CB5に変数名置換を適用する と図8.18の部品CB50 のようになる．
第8章 手法適用例 119
IMPLEMENTATION RentC7_i(maxUser, maxPoint) REFINES RentC7_d
IMPORTS
points_i.PFunc((0..maxUser), (0..maxPoint)) INVARIANT
points = points_i.value &
((BankC5_fileOpen = TRUE) =>
(points_i.fileOpen = TRUE))
OPERATIONS returnCar(user, point) = VAR bal, arg1, arg2 IN /*REF*/
MACHINE Rent_C7_d(maxUser, maxPoint) ...
CONCRETE_VARIABLES BankC5_fileOpen INVARIANT
points : 0..maxUser +-> 0..maxPoint &
dom(points) <: 0..maxUser &
ran(points) <: 0..maxPoint &
BankC5_fileOpen : BOOL OPERATIONS returnCar(user, point) = PRE
user : 0..maxUser &
point : NAT &
points(user) + point <= maxPoint &
BankC5_fileOpen = TRUE THEN
RentC7と同じ END
実装依存モデルRentC7_d 細分化実装RentC7_i 部品C’B5
IMPLEMENTATION RentC6_i(limit, maxCar, maxUser) REFINES RentC6_d
IMPORTS
rent_i.PFunc((0..maxCar), (0..maxUser)) INVARIANT
rent_i.value = rent &
((GroupC5_fileOpen=TRUE) =>
(belong_i.fileOpen=TRUE)) MACHINE RentC6_d(...)
CONCRETE_VARIABLES GroupC5_fileOpen INVARIANT
rent : 0..maxCar +-> 0..maxUser &
!(user).(user : ran(rent)) => ...) &
dom(rent) <: 0..maxCar &
ran(rent) <: 0..maxUser &
GroupC5_fileOpen : BOOL OPERATIONS returnCar(car) = PRE car : 0..maxCar &
car : dom(rent) &
GroupC5_fileOpen = TRUE THEN
細分化モデルと同じ END
細分化実装RentC6_i 実装依存モデルRentC6_d
部品CG5
OPERATIONS returnCar(car) = /*DEF*/
rent_i.delVal(car)
END Zx
bal <-- points_i.getVal(user);
arg1 := user;
arg2 := bal + point;
/*DEF*/
points_i.setVal(arg1, arg2) END
END
Wy
Zy
図 8.18: 部品CG5, CB5 の変数名置換結果
第8章 手法適用例 120
MACHINE DbBankC1_d(maxUser, maxBalance) CONSTRAINTS
maxUser : 1..10000 &
maxBalance : 1..10000000 ...
CONCRETE_VARIABLES transaction INVARIANT ... & transaction : BOOL OPERATIONS
res_newUser <-- registUser(name, addr) = PRE ... & transaction = TRUE
THEN 細分化モデルの代入文と同じ
実装依存モデルDbBankC1_d
細分化実装DbBankC1_i 部品C’B1
IMPLEMENTATION DbBankC1_i(maxUser, maxBalance) REFINES Bank_registUserAnyDefP1_DB_d IMPORTS
table.DbTable(0..maxUser, 1, 0..maxBalance, 2) INVARIANT
users = table.keys &
userName = table.strFields(1) &
userAddr = table.strFields(2) &
((transaction = TRUE) => table.transaction = TRUE)
OPERATIONS
res_newUser <-- registUser(name, addr) = VAR corFlag, pp, xxres IN
/*REF*/
corFlag <-- table.existsWithStr(1, name, 2, addr);
pp := corFlag;
IF corFlag = FALSE THEN
xxres <-- table.nextKey END;
/*DEF*/
IF corFlag = FALSE THEN
res_newUser := xxres END
END END
図 8.19: 細分化モデルBankC1のデータベースによる実装