こんにちは、SWETの鈴木穂高（@hoddy3190）です。
私はこちらの記事に記載の通り、形式手法の可能性を模索しています。 現在はツールやゲームの仕様を形式的に記述すること（形式仕様記述）で、仕様の欠陥をなるべく早く見つける取り組みにチャレンジしています。 今回は仕様記述をするにあたりよく使う重要な記述テクニックである「Promotion」を紹介します。
形式仕様記述とAlloyというツールを知っている人を対象にしています。 もし形式仕様記述やAlloyをご存じない方は、以前私がbuilderscon tokyo 2019で発表したときに使った資料をご覧ください。
Promotionとは
一般にソフトウェアシステムは複数のコンポーネントから構成されます。 システム全体としての状態（以下、システム状態）は各コンポーネントの状態の組み合わせからなります。 たとえどんなに奥深くのどんなに小さなコンポーネントが変化したとしてもそれはシステム状態の変化になります。
Promotionはコンポーネントの中で起こる局所的な変化をシステムレベルの大局的な変化に"昇格"させるテクニックです。 Promotionはシステム状態の変化といったグローバルな操作を、コンポーネントの変化といった「ローカルな操作」と 「ローカルとグローバルの状態の関係を表す述語」に分解して記述します。
分解せずに記述する方法と比べ、関心の分離ができる上、ローカルとグローバルの状態の関係を表す述語は再利用できるのでリファクタが容易になるといったメリットがあります。
一般的にPromotionは、ローカルの事前・事後を表す変数LocalVariables・LocalVariables'、ローカルの操作を表す述語PredLocal、ローカルとグローバルの状態の関係を表す述語PredPromoteを使い、次の形で表現されます。
これがグローバルな操作と同じ意味になります。
本記事の題材
題材としてGitを扱います。Gitのシステムはいくつかのコンポーネントからなります。 ここでは簡略化してシステムの状態とブランチ、コミット、ファイルの4つの関係を例に挙げます。次の図がその関係の例を示したものです。
ブランチ、コミット、ファイル枠内の丸1つ1つは、それぞれブランチ、コミット、ファイルを表します。
1つのブランチは1つの先頭コミットに紐付きます。あるコミットが、異なる複数のブランチに紐付けられることもありえます。
コミットは0以上のファイルに紐付きます。紐付けられたファイルは、差分ファイルではなくコミットに含まれているファイルを意味しています。
システム枠内の四角1つ1つは、Gitシステムが取りうる「状態」を表します（状態であることを区別するため丸ではなく四角で表現しています）。
状態は「どのブランチ・コミットの関係を持つか」、つまり、存在しているブランチそれぞれがどのコミットを指しているかによって決まります。
1つの状態に対し、「ブランチ・コミットの関係」は1つ以上紐付けられます。
今回はこのシステムを題材に「新しいファイルを追加するコミットを行う」を考えてみたいと思います。
システムの事前状態と事後状態
「新しいファイルを追加するコミットを行う」は、「コミットcに紐付いているある1つのブランチbが別のコミットc'に紐付く（今回はコミットの親子関係を考えない）」という状態変化があります。
図で表すとこのようなイメージです。
事前のシステムの状態をs、事後のシステムの状態をs'と表現しています。
ブランチbはsに紐付けられたブランチです。sでは、ブランチbはコミットcに紐付きます。
「新しいファイルを追加するコミットを行う」を行った結果、s'では、ブランチbはコミットc'に紐付きます。
このとき、c'に紐付けられたファイルは、c'に紐付けられたファイルに新しいファイルを加えたものになります。
共通部分
上の図をAlloyで記述するのに必要な集合、関係は次の通りです。これはPromotionを使う・使わないに関わらず共通です。
sig System {
bc: Branch -> one Commit
} {
some bc
}
sig Branch {}
sig Commit {
files: set File
}
sig File {}
Promotionを使わないストレートな書き方
Promotionを使った書き方を紹介する前にまずは条件をすべてそのまま書き下して書いてみます。
// システムの事前の状態: s
// システムの事後の状態: s'
// 向き先コミットが変わるブランチ: b
// コミットで新しく加わるファイル: newFile
pred commitNewFile(s, s': System, b: Branch, newFile: File) {
// 【事前条件】追加されるファイルは元のコミットには含まれていない
newFile not in (b.(s.bc)).files
// 【事前条件】コミットに含まれるファイルの集合にnewFileを加えたものが新しいコミットのファイルの集合となる
(b.(s'.bc)).files = (b.(s.bc)).files + newFile
// s.bcのbの関係を上書き（b以外の関係は変えない）
s'.bc = s.bc ++ b -> b.(s'.bc)
}
「b以外の関係は変えない」は(Branch - b) <: s'.bc = (Branch - b) <: s.bcとも書けます。
Promotionを使った書き方
先述の通り、Promotionはローカルな操作・ローカルとグローバルの状態の関係を表す述語でグローバルな操作を表現する書き方です。
Promotionを使って書いてみると次のようになります。
// もともと向いていたコミット: c
// 新しい向き先のコミット: c'
// コミットで新しく加わるファイル: newFile
pred commitNewFileLocal(c, c': Commit, newFile: File) {
// commitNewFile内から必要なものを持ってくる
newFile not in c.files
c'.files = c.files + newFile
}
// システムの事前の状態: s
// システムの事後の状態: s'
// もともと向いていたコミット: c
// 新しい向き先のコミット: c'
// 向き先コミットが変わるブランチ: b
pred promoteCommitToSystem(s, s': System, c, c': Commit, b: Branch) {
// 【事前条件】cはbがもともと向いていたcommitであること
c = b.(s.bc)
// システムの状態s.bc内のb->cをb->c'で上書き（b->c以外の関係は変えない）
s'.bc = s.bc ++ b -> c'
}
// システムの事前の状態: s
// システムの事後の状態: s'
// 向き先コミットが変わるブランチ: b
// コミットで新しく加わるファイル: newFile
pred commitUsingPromotion(s, s': System, b: Branch, newFile: File) {
some c, c': Commit {
commitNewFileLocal [c, c', newFile]
promoteCommitToSystem [s, s', c, c', b]
}
}
それぞれの述語がどのような役割を担っているのか次の図をもとに説明します。
コミットとファイルに関わるローカルな操作（1の矢印）はcommitNewFileLocal で記述しています。
ローカルとグローバルの状態の関係を表す述語（2-a、2-bの線）はpromoteCommitToSystemで記述しています。
c = b.(s.bc)は、sの中のブランチbに対応するコミットとcが同じであることを意味しています（2-aの線）。
s'.bc = s.bc ++ b -> c'は2つのことを意味しています。1つはs'の中のブランチbに対応するコミットとc'が同じであること（2-bの線）、もう1つはb以外のブランチ（グレーのゾーン）が変化しないということです。
また、promoteCommitToSystemはcがどのように変化するかは関与しません。
そのためpromoteCommitToSystemは他のローカル操作でも再利用ができます。
システムの事前状態sから事後状態s'に関するグローバルな操作（3の矢印）はcommitUsingPromotionで記述しています。
promoteCommitToSystemとcommitNewFileLocalを組み合わせてグローバルな操作を表しています。
同値であることを確認
Promotionを使わない書き方とPromotionを使った書き方は同値なのでしょうか。2つの方法で確かめてみます。
Alloyのアサーションを使って確認
Alloyはアサーション検査ができるのでこの機能を使って確かめてみます。
assert promotion {
all s, s': System, b: Branch, newFile: File {
commitNewFile [s, s', b, newFile] <=> commitUsingPromotion [s, s', b, newFile]
}
}
check promotion
検査をしてみましょう。
Executing "Check promotion" Solver=minisatprover(jni) Bitwidth=0 MaxSeq=0 SkolemDepth=1 Symmetry=20 1032 vars. 60 primary vars. 2209 clauses. 113ms. No counterexample found. Assertion may be valid. 14ms. Core contains 4 top-level formulas. 12ms.
結果、反例は見つかりませんでした。 アサーションの検査で可能な有限の範囲に限れば、2つの表現は同値であることが確認できました。
同値変形を使って確認
別のアプローチとして同値変形を利用してみましょう。
まず、commitUsingPromotionの中のcommitNewFileLocalとpromoteCommitToSystemを定義で置き換えてみます。
pred commitUsingPromotion(s, s': System, b: Branch, newFile: File) {
some c, c': Commit {
// commitNewFileLocalの定義
newFile not in c.files
c'.files = c.files + newFile
// promoteCommitToSystemの定義
c = b.(s.bc)
s'.bc = s.bc ++ b -> c'
}
}
限量子someが束縛する変数cはc = b.(s.bc)なので、一点規則と呼ばれる次の規則が適用できます。
すると次のように同値変形できます。
pred commitUsingPromotion(s, s': System, b: Branch, newFile: File) {
some c': Commit {
// commitNewFileLocalの定義
newFile not in (b.(s.bc)).files
c'.files = (b.(s.bc)).files + newFile
// promoteCommitToSystemの定義
s'.bc = s.bc ++ b -> c'
}
}
また先述した通り、s'.bc = s.bc ++ b -> c'には「s'の中のブランチbに対応するコミットとc'が同じであること」という意味があります。
つまり、c' = b.(s'.bc)が成り立ちます。限量子someが束縛する変数c'についても一点規則が適用できます。
pred commitUsingPromotion(s, s': System, b: Branch, newFile: File) {
// commitNewFileLocalの定義
newFile not in (b.(s.bc)).files
(b.(s'.bc).files = (b.(s.bc)).files + newFile
// promoteCommitToSystemの定義
s'.bc = s.bc ++ b -> b.(s'.bc)
}
本記事で一番最初に紹介したPromotionを使わない書き方commitNewFileと同じ形になりました。
まとめ
Promotionを使えばグローバルな操作をローカルな操作・ローカルとグローバルの状態の関係を表す述語に分けて書くことができます。 操作がローカルな部分のみを変更する場合はPromotionを検討してみると良いかもしれません。
