社団法人 電子情報通信学会
THE INSTITUTE OF ELECTRONICS,
INFORMATION AND COMMUNICATION ENGINEERS

信学技報
TECHNICAL REPORT OF IEICE.

異なるスキーマ間に対応する SQL 文の整合性のAlloy Analyzer を用いた一検証手法
藤田 悠矢†

岡野 浩三†

楠本真二†† 大阪大学大学院情報科学研究科，吹田市
E-mail: †{f-yuya,okano,kusumoto}@ist.osaka-u.ac.jp
あらまし

ビジネスアプリケーション等において，データベーススキーマが正しく設計・分割できていること，そのスキーマに対応する SQL 文が正しく記述できていることが保証されているということは非常に重要である．データ
ベーススキーマは慎重に設計を行った場合においても運営上の不具合が生じることや，長期にわたって使用することによりスキーマの構造が時代遅れのものとなることがある．その際， 業務に適した形へスキーマの改良 (スキーマ進化) を行う必要性があり，そのスキーマに対する SQL 文も新しいスキーマに適するものに変換する必要がある．一方，
ソフトウェアの仕様を形式的に記述できる言語に Alloy があり，Alloy の制約記述に対してその制約を満たす例 (インスタンス)，満たさない例 (反例) を有界網羅的に検出する Alloy Analyzer というツールがある．本研究では，スキーマ変更に伴う SQL 文の変換が正しく行われていることの確認を Alloy Analyzer によって行う手法を提案し，その手法の正しさの数学証明を行った．また，ケーススタディとして在庫管理プログラムで用いるデータベーススキーマに対して手法を適用し，その有用性の確認を行った．結果，Alloy Analyzer においてスキーマと SQL 文の整合性を確認することができた．
キーワード

Alloy，SQL，スキーマ変換，在庫管理問題

A Verification Method on Consistency between Diﬀerent SQLStatements and Schemas using Alloy Analyzer
Yuya FUJITA† , Kozo OKANO† , and Shinji KUSUMOTO†† Graduate School of Information Science and Technology, Osaka University, Suita-shi, 565-0871, Japan
E-mail: †{f-yuya,okano,kusumoto}@ist.osaka-u.ac.jp
Abstract In software using database, it is very important that database schema is properly designed to assurethat and also that SQL statements which correspond to the schema are correctly described. Long-term operation
sometimes, however, causes operational defects becuase database shema might not fit to the current deployment
despite that it was carefully designed in the past. In such a case, we have to perform improvement of the schema(Schema evolution) to a form suitable for the work, and also we have to convert the SQL statements into a form
suitable for new schema. Alloy is a language which can formally describe specification of software. Alloy Analyzer
is a tool to find instances that satisfy the constraint described in Alloy or counterexamples that do not satisfy. This
report proposes a method that lets Alloy Analyzer verify if the conversion of SQL statements associated with thegiven schema modification have conformance. It also gives mathematical proof of the correctness of the method.
The method is applied to the database schema used in a warehouse management program as a case study to confirm
its usefulness. The author consequently can verify the conformance of the SQL statements using Alloy Analyzer.
Key words Alloy, SQL, Schema evolution, Warehouse Management Program—1—1. ま え が き

attribure1(Primary Key)

attribure1(Primary Key)
attribute2
attribute3

る SQL 文が正しく記述できていることが保証されているとい

attribute2
attribute3
・・・
attributen(Foreign key)

うことは非常に重要である．そのため，データベーススキーマ

TableName1

ビジネスアプリケーション等において，データベーススキー
マが正しく設計・分割できていること，そのスキーマに対応すの設計は慎重に行われるが，その場合においても実際に運用し・・・

attributem

TableName2
図1

スキーマ例

てみることで不具合を見つけることがある．また，アプリケー
ションの世界は常に変化し続けているため [1]，長年にわたって
データベースを運用し続けることにより，そのスキーマの構造が時代遅れのものとなることがある．その際，業務や時代に則した形へスキーマの改良 (スキーマ進化) を行う必要性があり，
そのスキーマに対する SQL 文も新しいスキーマの形に適するものに変換する必要がある．正しい変更を実現するという試み
は，アプリケーションソフトウェア業界において長年にわたり

sig Address {}sig Name {add : one Address}
fact {Name <: add
in Name lone -> one Address}
run {}

図 2 Alloy 記述例・Alloy Analyzer 出力例

主要な活動とされてきた [2] [3] [4] [5] [6]．スキーマ進化に関してもその例外ではなく，スキーマの変換に関する研究 [7] [8] [9]，T ableN ame1 における attributen は T ableN ame2 の属性をや，XML のスキーマ進化に伴う問い合わせ言語の変更に関す参照している外部キーを表している．

る研究 [10] は過去にも存在している．しかし，著者の調べた限

このように簡単なスキーマでも複数のデータベースを組み合りでは，スキーマ進化に伴い変更された SQL 文が意図通りのわせて構成することは多く，このような構成が意図通りである

ものかどうかを検証する方法に関する研究は見つけることがでことを確認する需要があると考えることができる．

2. 2 Alloy・Alloy Analyzer

きなかった．
一方，ソフトウェアの仕様を形式的に記述できる言語に Al-

Alloy は集合と関係からなる一回述語論理に基づいたオブジェ

loy [11] [12] があり，Alloy の制約記述に対してその制約を満た

クト指向モデリングのための形式仕様記述言語である [11] [12]．

す例 (インスタンス)，満たさない例 (反例) をユーザの指定しAlloy Analyzer は，Alloy の自動解析ツールであり，記述したたスコープ内において網羅的に探索する Alloy Analyzer といモデルに対して表明の検証を行うことができる．一方モデルのうツールがある．小さなスコープであっても非常に大きな空間

探索範囲は有界であり，記述クラスも関係が表現できる，一回内を探索するので，微妙なバグの発見するのにも十分な威力を述語論理のサブクラスに限定されている．Alloy では，オブジェ発揮する．抽象度の高い仕様の段階で Alloy を使って検査してクトに相当するシグネチャやシグネチャが持つフィールド，そおくことで，その後の設計や実装段階で根本的な仕様バグが見してそれらの間に成り立つ論理式などにより，モデルを記述す

つかることによる手戻りの発生を減らすことができる．

る．Alloy Analyzer はモデルに対してその反例，あるいは正例

本研究では，広く使用されている関係データベースにおけるを有限探索した結果として出力することができる (図 2)．

スキーマの変更に関して考え，それに伴う SQL 文の変換が正図 2 では，Address シグネチャと一つの Address をフィール

しく行われていることの確認を Alloy Analyzer によって行うドとして持つ Name シグネチャの間に，一つの Address に対し手法を提案し，その手法の正しさの数学証明を行った．また，てその Address を保持する Name は高々一つであるという記述

在庫管理プログラムで用いるデータベーススキーマに対して手に対して，正例として Name0，Name1 がそれぞれ Address0，法を適用することで，その有用性の確認を行った．結果，Alloy

Address1 を保持している例があることを表すグラフを表してAnalyzer においてスキーマと SQL 文の整合性の確認をするこ

おり，これがこのツールの出力としていることができる．

2. 3 スキーマと SQL 文の整合性とができた．
本稿の構成は以下のとおりである．2 章では本稿に関する諸変更前後のスキーマと SQL 文の満たすべき制約として，以定義について述べ，3 章で提案手法，4 章でケーススタディへ

下のようなスキーマと SQL 文の整合性を定義する．

の適用結果について説明する．5 章では関連研究について言及［定義 1］（整合性） 変更前のリレーションスキーマ R ，変更

し，最後に 6 章でまとめる．

後のリレーションスキーマ R′ ，それぞれに対応する SQL 文

2. 準

備

の系列を s ， s′ とするとき，下の 2 つの写像があるとする．

f : R → R′
g : s → s′

2. 1 ス キ ー マ
スキーマはデータベースの構造を表しており，テーブル名，属性などの情報を持つ．また，テーブル間の関係やテーブ

R を満たす任意のリレーション r に任意の s を適用して得られる h(r, s) とルに関連する制約なども規定されている (図 1)．図 1 では，R′ を満たす任意のリレーション r′ に g(s) を適用して得ら

attribute1 はそれぞれのテーブルの主キーを表している．またれる h(r ′ , g(s)) に対して次の式が成り立つとき，整合性が成り—2—

変更前のスキーマR

SQL文s’

疑似SQL文s

疑似SQL文s’スキーマ(定義)：

R

Alloyで記述

Alloyで記述
Alloyで記述された
スキーマR変更後のスキーマR’

SQL文sAlloyで記述された
SQL文sAlloyで記述された
SQL文s’Alloyで記述された
スキーマR

Alloy Analyzerで整合性の確認
整合性が成り立たないとき，反例を出力
整合性が成り立つとき，反例がないことを出力
図3

：入力

A1
A2
…
Am(FK)
…
An

Am

S

B1
B2
…
Bl

スキーマ(Alloy)：
sig R {r : (DA,1 + NULL)− > · · ·− > (DA,m + NULL)− > · · ·− > (DA,n + NULL)}{
all x1 : r.DA,n. · · · .DA,2 |(x1 != NULL) && one x1.r
DA,m-1.(· · · .(DA,1.(r.DA,n. · · · .DA,m+1)) · · ·) in ((S.r).DB,l. · · · .DB,1 +NULL)}
sig S {r : DA,m− > DB,1− > · · ·− > DB,l}{all x1 : r.DB,l. · · · .DB,1|(x1 != NULL)&&one x1.r}

提案手法の流れ図 5 スキーマの Alloy への変換

入力として与えるSQL文 : DELETE FROM r WHERE Ak = ak
疑似SQL文 : DELETE FROM r WHERE AK = x (x ∈ Ak)
図4

SELECT A’1, …, A’m FROM r1, …, rn WHERE F;↓
πA’1,...,A’m (σF (r1×···×rn))
DELETE FROM r WHERE F;↓
r - σF (r)疑似 SQL 文

立つという．

f (r) = r′ ⇒ f (h(r, s)) = h(r′ , g(s))

3. 提 案 手 法
本節では，提案手法について説明する．提案手法における整UPDATE r SET Ai = ai WHERE Aj = aj;↓(r − σAj=aj (r)) ∪ s(s = {t | t’ ∈ σAj=aj (r)∧t[Ai] = ai∧t[Ak] = t’[Ak](1 ≤ k ≤ n, ≠ i)})

合性確認の流れは次のようになる (図 3)．

INSERT r INTO (a1, …, an);↓r ∪ (a1, …, an)（ 1 ） 入力として変更前後のスキーマ，SQL 文を与える（ 2 ） SQL 文を疑似 SQL 文に変換する（ 3 ） 各スキーマ，疑似 SQL 文を Alloy で記述する

図6

各 SQL 文の関係演算式での記述（ 4 ） Alloy Analyzer を用いて整合性の確認を行う
疑似 SQL 文とは，変数を用いており，その変数に対して取キーといった整合性制約は不変条件として定義している．
文

りうる値に制約を付加した SQL 文である．この SQL 文に変換

SQLすることで，ある特定の値のみでなく，その属性の取りうる値

各 SQL 文は関係演算を用いて記述することができる (図 6)．

すべてに対して検証できる (図 4)．

関係演算の和演算，差演算は Alloy において既に存在おり，そ

従来の実データに依存する検証方法では，実データの状態にの記述はそれぞれ r + s，r − s(r，s はリレーション) である．

よっては検証結果に不備が生じることがあったが，Alloy Ana-

関係演算の選択演算，射影演算，直積演算の Alloy における記

lyzer を用いることにより，データベースの実データによらない

述は図 7 に与える．

有界網羅的かつ論理的な検証が可能となる． 以下では，スキー記述において，A′i (1 <=i<= m) は r1 から rn のいずれかに含

マおよび各 SQL 文，そして定義 1 で与えたスキーマと SQL 文

まれる属性である．また，t[A] はタプル t に含まれる属性 A の要の整合性を Alloy においてどのように記述したかを示す．記述

素を，ai は Ai の要素， F は条件式を表している．ei は DA,1 〜

において，Ai は属性名，そのドメインを DA,i で表している．

DA,n のいずれかである．図 7 の射影演算の記述において DA ,i ∈

なお，記述の正しさの証明に関してはページの都合上割愛する．
定義 1 では，SQL 文は系列として与えていたが，証明では各{((R.r).DA,n . · · · .DA,2 ), . . . , (DA,n−1 .(· · · .(DA,1 .(R.r)) · · · ))}| j <かつ DA ,i =| DA ,j (1 <= m) を満たしており，また，=i=

SQL 文に関してのみ定義している．これは，各 SQL 文においDA ,i [x1 , ..., xi−1 ](2 <==j <= m) はアトム xj ∈ DA ,j (1 <=i<て整合性を保つことができているならば，SQL 文の系列においi − 1) によって制限された範囲式である．

ても整合性を保つことができているからである．各 SQL 文のこれらから各 SQL 文の Alloy における記述は図 8 となる．

Alloy 記述は直観的に行うことができる．基本的には Alloy 記

スキーマと SQL 文の整合性

述に対する整合性の定義の妥当性に帰着することができる．

変更前後のスキーマ間，SQL 文の実行結果間で成り立つべスキーマ

き式を定め，それを Alloy において記述した．なお，SQL 文のスキーマの定義にはシグネチャを使用する．シグネチャは整合性に関しては SELECT 文とそれ以外の SQL 文で式が異フィールドとして属性間の関係を持ち，また，主キーや外部なっている (図 9)．なお， s[r] はリレーション r に SQL 文 s—3—選択演算：σF (r) = {t | t ∈ r ∧ PF(t)}fun Selection[r : (DA,1 + NULL)->···-> (DA,n + NULL),
x1 : e1, ..., xm : em]: (DA,1 + NULL)->···-> (DA,n + NULL){{x1 : r.DA,n.···.DA,2,...,
xn : xn-1.(···.(x1.(r))···)
|F}
}
射影演算：
πA’1,...,A’m (r) = {t[A’1, …, A’m] | t ∈ r}
fun Projection[r : (DA,1 + NULL)->···-> (DA,n + NULL)]: DA’,1−>···->DA’,m {{x1 : DA’,1,...,
xm : DA’,m[x1, ..., xm-1]}}
直積演算：
r × s = {t * u | t ∈ r ∧ u ∈ s}
fun Cartesian[r : (DA,1 + NULL)->···-> (DA,n + NULL),s : (DB,1 + NULL)->···-> (DB,m + NULL)]: (DA,1 + NULL)->···-> (DA,n + NULL)->(DB,1 + NULL)->···->(DB,m + NULL){{x1 : r.DA,n.···.DA,2,...,
xn : DA,n-1.(···.(x1.(r))···),
xn+1 : s.DA,n.···.DB,2,...,
xn+m : DA,n+m-1.(···.(xn+1.(s))···)}}
図 7 関係演算の Alloy 記述を実行した結果を表している．この記述はデータベースに与えられている具体的な値に関わらず，SQL 文とデータベースの整合性の関係を表している．

4. ケーススタディ
本章では，ケーススタディに用いたスキーマの概要と，手法を適用した結果を示す．

4. 1 スキーマ概要
変更前後のスキーマとして図 10 のものを用意した．これは [13] の在庫管理プログラムを参考にして作成している．こSELECT(SQL) : SELECT A’1, …, A’m FROM r1, …, rn
WHERE F;
SELECT(Alloy) :fun Select[r1rows : DA1,1->···-> DA1,k1,…,
rnrows : DAn,1->···-> DAn,kn, x1 : e1, ..., xl : el]: DA’,1->···-> DA’,m{
Projection[Selection[Cartesian[r1rows, …, rnrows], x1, ..., xl]]}
DELETE(SQL) : DELETE FROM r WHERE F;
DELETE(Alloy) :fun Delete[rrows : DA,1->···-> DA,n, x1 : e1, ..., xl : el]: DA,1->···-> DA,n{rrows − Selection[rrows, x1, ..., xl]}
UPDATE(SQL) : UPDATE r SET Ai = ai WHERE Aj = aj;
UPDATE(Alloy) :fun Update[rrows : DA,1->···->DA,n, ai : DA,i, aj : DA,j]: DA,1->···-> DA,n{rrows − Selection[rrows, aj] + UpdatedRows[rrows, ai, aj]}
fun UpdatedRows[rrows : DA,1->···->DA,n, ai : DA,i, aj : DA,j]: DA,1->···->DA,n{{x1 : (rrows).DA,n.··· .DA,2,...,
xi : ai,
xi+1 : DA,i.(xi-1.(···.(x1.((rrows).DA,n.···.DA,i+2))···)...,
xn : xA,n-1.(···.(DA,i.(···.(xn+1.(rrows))···)| xj = aj}}
INSERT(SQL) : INSERT r INTO (a1, …, an);
INSERT(Alloy) :fun Insert[rrows : DA,1->···-> DA,n, a1 : DA,1, ..., an : DA,n]: DA,1->···->DA,n{rrows + a1->···->an}
図 8 SQL 文の Alloy への変換

（ 2 ） 整合性の成り立つ SQL 文を与え，反例がないと表示されることを確認
今回はページの都合により，業務処理 1 におけるそれぞれの適用例の結果のみを示す．

のスキーマは変更前における Request テーブルを変更後にお4. 2 業務処理 1 における実行結果

ける Request，Customer，Item の 3 つのテーブルに，変更前

業務処理 1 は，「顧客の注文を同一コンテナから発送できなにおける Stock テーブルを変更後における Stock，Container，

いかどうかを確認し，できる場合そのコンテナの ID，入庫日，Item の 3 つのテーブルに分割したものとなっている．

在庫数を出力する」といった処理である．適用例 1 に該当す

このスキーマに対して行われうる業務処理を 3 つ用意し，そる SQL 文として図 11 を用いた．図 10 のスキーマと図 11 のれぞれの業務処理に対して 2 つの適用例の観点で検証を行った．

SQL 文を入力として手法を適用した結果，Alloy Analyzer に

今回検証を行った業務処理，適用例は以下のとおりである．

おいて，反例があると出力された (図 12)．その反例の一つと業務処理

して，Alloy Analyzer では図 13 が示された．この図からわか•注文個数以上の在庫を持つコンテナをすべて出力るように，変更前と変更後において，出力結果が異なってい•新規コンテナの入荷

ることがわかる．この反例は，図 11 の変更後の SQL 文にお•新規注文の受付

いて Stock テーブルの ContainerID と Container テーブルの適用

ContainerID が一致するかどうかを確認する一文を記述し忘れ例（ 1 ） 整合性の成り立たない SQL 文を与え，反例が表示されることを確認たために生じたミスである．
続いて，適用例 2 に該当する SQL 文として図 14 を用いた．

—4—

スキーマ分割における整合性(定義)：r = {t'[A1, . . . ,Am] ∗ t''[Am+1, . . . ,An]| t' ∈ r'∧t'' ∈ r''∧t'[B1] = t''[B1]}
スキーマ分割における整合性(Alloy)：
pred SchemaConsistency(r : R, r’ : R’, r’’ : R’’){r.rows = {x1 : (s.rows).DB,1.DA,m. · · · .DA,2,...,
xm : xm-1.(xm-2.(· · · .(x1.(r’.rows.DB,1)) · · ·)),
xm+1 : (DB,1.(r’’.rows)).DA,n. · · · .DA,m+2,...,
xn : xn-1.(· · · .(xm+1.(DB,1.(r’’.rows))) · · ·)| xm.(· · · .(x1.(r’.rows)) · · ·) = (r’’.rows).xn. · · · .xm+1}}
スキーマ分割におけるSQL文の整合性(定義)：
SELECT文：
s[r] = s'[r', r'']
DELETE文，UPDATE文，INSERT文：
s[r] = {t'[A1, . . . ,Am] ∗ t''[Am+1, . . . ,An]| t' ∈ s'[r']∧t'' ∈ s'[r'']∧t'[B1] = t''[B1]}
スキーマ分割におけるSQL文の整合性(Alloy)：
SELECT文：
assert Consistency{
all x1 : e1, . . . , xn : en,r : R, r’ : R’, r’’ : R’’ |(SchemaConsistency[r, r’, r’’])=> (SELECT_Before[r, x1, . . . , xn]= SELECT_After[r’, r’’, x1, . . . , xn])}
DELETE文，UPDATE文，INSERT文：
assert Consistency{
all x1 : e1, . . . , xn : en,r_pre, r_post : R, r’_pre, r‘_Post : R’, r’’_pre, r’‘_post : R’’|
(SchemaConsistency[r_pre, r’_pre, r’’_pre]&&r_post = SQL Before[r_pre, x1, . . . , xn] &&r’_post = SQL_After[r’_pre, x1, . . . , xn] &&r’‘_pre = SQL_After[r’’_post, x1, . . . , xn])=> (SchemaConsistency[r_post, r‘_post, r’’_post])}
図9

スキーマと SQL 文の整合性

変更前
RequestID
ItemName
MakerNameCountainerID
Date

CustomerName
Address
ItemName
MakerName
AmountAmountStock

Request

変更後
RequestID

ItemID(FK)CountainerID(FK)

CustomerID(FK)
ItemID(FK)AmountAmountStock

RequestCustomerID

ItemIDCountainerID

CustomerName
Address

ItemName
MakerNameCountainer

Customer

Date

Item
図 10 検証対象のスキーマ

変更前SQL文：SELECT ContainerID, Date, StockAmount FROM Stock
WHERE ItemName= (SELECT ItemName FROM Request WHERE ReqID=‘ReqID’)
AND MakerName= (SELECT MakerName FROM Request WHERE ReqID=‘ReqID’)
AND StockAmount>= (SELECT Amount FROM Request WHERE ReqID=‘ReqID’);

変更後SQL文:SELECT Stock.ContainerID, Date, StockAmount FROM Stock, Container
WHERE Stock.ItemID= (SELECT ItemID FROM Request WHERE ReqID=‘ReqID’)
AND Stock.StockAmount>= (SELECT Amount FROM Request WHERE ReqID=‘ReqID’);

図 11

変更前後の SQL 文 (適用例 1)

適用例 1 における変更後の SQL 文と異なる点は，太字で示されている箇所である．変更前の SQL 文は図 11 と同様のものである．これらの SQL 文と図 10 のスキーマを入力として手法を適用すると，Alloy Analyzer では反例がないことが示された(図 15)．

図 12 Alloy Analyzer 出力結果 (適用例 1)

これにより，与えた SQL 文は期待通りの変換が行えていたことがわかる．

4. 3 考察検証した 3 つの業務処理，2 つの適用例に対して，期待通りの結果を得ることができた．しかし，今回採用した記述方法では，大規模なスキーマの検証は不きであることが分かった．また，各業務処理，各適用例における記述行数は表 1 のとおりである．表 1 からわかるように，記述においてかかるコストは決して低いとは言えない．しかし，証明を通して SQL 文からストを行うツールとして ADUSA [14] がある．このツールは，

Alloy Analyzer の有界網羅的に正例を探索する特性を活かして，スキーマと SQL 文を Alloy で記述し，DBMS のテストデータを大量に作成するといったものである．このツールを用いることにより，人力で作成するよりも大量のテストデータを短時間で作成することができる．また，テスト用の SQL 文を生成する
アプローチ [15] と組み合わせることにより，DBMS のテストの自動化も行っている [16]．しかし，この研究において SQL 文はAlloy 式への変換を機械的に行えることは確認している．
表1

5. 関 連 研 究
スキーマや SQL 文を Alloy に変換することで，DBMS のテ

記述行数

業務処理 1 業務処理 2 業務処理 3
適用例 1

203

231

242

適用例 2

207

232

240

—5—

RequestID

Customer
Name

Address

Item
Name

Maker
Name

Amount

ID0

Name0

Add0

IName0Maker0

1

ID1

Name1

Add1

IName1

Maker1

2

RequestID

ID1
検索条件

文

Request
Item
Name

Maker
Name

Container
ID

Date

Amoun
t

IName0Maker0ConID0Date01

IName1

Maker1ConID1

Date1

2

実行結果(変更前)
ContainerID

DateAmountConID1

Date1

2

Stock
Customer Customer Item AmountID
ID(FK)
ID(FK)

Container
ID

Date

ID0

CID0

IID0

1

CID0

Date0

ID1

CID1

IID1

2

CID1

Date1

Container

RequestItem
ID(FK)

Container
ID(FK)

Amount

IID0

CID0

1

IID1

CID1

2

Stock

図 13

実行結果(変更後)
ContainerID

DateAmountConID1

Date0

2

ConID1

Date1

2

得られた反例 (上：変更前，下：変更後)

SELECT Stock.ContainerID, Date, StockAmount FROM Stock, Container
WHERE Stock.ItemID= (SELECT ItemID FROM Request WHERE ReqID=‘ReqID’)
AND Stock.StockAmount>= (SELECT Amount FROM Request WHERE ReqID=‘ReqID’)
AND Stock.ContainerID=Container.ContainerID;
図 14

謝辞 本研究は，科学研究費補助金基盤研究 (S)(課題番号：

25220003)，基盤研究 (C)(課題番号：21500036) の助成を得た．

変更前後の SQL 文 (適用例 2)

図 15 Alloy Analyzer 出力結果 (適用例 2)

SELECT 文の変換のみしか考慮されておらず，データベースの更新が生じる操作 (DELETE，UPDATE，INSERT) の Alloyへの変換は考慮していない．
本研究では，スキーマや SELECT 文の Alloy 記述は [14] を参考にして変換を行ったが，データベースの更新を伴う操作に関しても変換を行い，検証を行っている．

6. あ と が き
本稿では，スキーマ変換が生じた際の SQL 文の変更が正し
く行われているかどうかの確認を Alloy Analyzer を用いて行

献[1] D. Sjoberg, “Quantifying schema evolution,” Informationand Software Technology, vol.35, no.1, pp.35–44, 1993.
[2] M.V. Zelkowitz, “Perspectives on Software Engimeering,”
ACM Computing Surveys, vol.10, no.2, pp.197–216, June
1978.
[3] L.H. Putnam, Software Cost Estimating and LifeCycle Control, IEEE Computer Society, 1982.
[4] G. Parikh and N. Zvegintzov, “The World of Software Maintenance,” Tutorial on Software Maintenance, pp.1–3, IEEE
Computer Society, 1983.
[5] T.A. Corbi, “Program Understanding: Challenge for the
1990s,” IBM Systems Journal, vol.7, no.2, pp.294–306,
1989.
[6] E.J. Chikofsky and J.H.C. II, “Reverse Engineering and Design Recovery: A taxonomy,” IEEE Software, vol.7, no.1,
pp.13–17, Jan. 1990.
[7] P. McBrien and A. Poulovassilis, “Schema Evolution in
Heterogeneous Database Architectures, A Schema Transformation Approach,” Lecture Notes in Computer Science,
vol.2348, pp.484–499, 2002.
[8] S. Monk and I. Sommerville, “Schema evolution in
OOODBs using class versioning,” ACM SIGMOD Record,
vol.22, no.3, pp.16–22, 1993.
[9] M. Blaschkaand, C. Sapia, and G. Hofling, “On Schema
Evolution in Multidimensional Databases,” Lecture Notes
in Computer Science, vol.1676, pp.153–164, 1999.
[10] 長谷川数馬，池田光雪，鈴木伸崇，“スキーマ進化に伴う XPath
式修正アルゴリズム，” 情報処理学会第 74 回全国大会，pp.4–6，
2012．
[11] D. Jackson, Software Abstractions, MIT Press, Nov. 2011.
[12] 中島震，鵜林靖，“Alloy:自動解析可能なモデル規範形式仕様言語，” コンピュータソフトウェア，vol.26，no.3，pp.78–83，July
2009．
[13] 尾鷲方志，岡野浩三，楠本真二，“在庫管理プログラムに対するJML 記述と ESC/Java2 を用いた検証の事例報告，” 電子情報通信学会論文誌，vol.J91D，pp.2719–2720，Nov. 2008．
[14] S.A. Khalek，B. Elkarablieh，Y.O. Laleye, and S. Khurshid, “Query-aware Test Generation Using a Relational
Constraint Solver,” Proc. of 23rd ASE 08, IEEE/ACM
Int. Conf. on Automated Software Engineering, pp.238–247,
2008.
[15] S.A. Khalek and S. Khurshid, “Automated SQL Query Generation for Systematic Testing of Database Engines,” Proc.
of 25th ASE 10, IEEE/ACM Int. Conf. on AutomatedSoftware Engineering, pp.329–332, 2010.
[16] S.A. Khalek and S. Khurshid, “Systematic Testing of
Database Engines Using a Relational Constraint Solver,”
ICST’11 Proc. of the 2011 Fourth IEEE Int. Conf. on Software Testing, Verification and Validation, pp.50–59, March
2011.

う手法を提案した．また，ケーススタディとして在庫管理プロ
グラムにおける 3 つの業務処理に対して手法を適用し，いずれの業務処理においても整合性が成り立たない SQL 文に対しては反例を，整合性の成り立つ SQL 文に対しては反例がないことを示すことが確認された．
今後の課題として，より大規模なスキーマに手法を適用する
ことによる検証，スキーマや SQL 文を Alloy に自動変換する
ツールの作成を行うことを考えている．

—6—