2013-08-08

今回は、JPAでいう Orphan Removal のような、依存のある関連を扱ってみます。
Ruby on Rails でいうと
:dependent => :destroy とか、 :dependent => :delete_all といった、
アソシエーションのオプションを使って制御するアレですね。
JPA2でいうと、
@OneToMany(orphanRemoval=true) のようなアノテーション属性で制御するアレですね。
要は、親レコードが削除されたときに、親の無い子レコード（orphan）が発生しないようにするための策です。

ここでちょっと今までのやり方について再考しました。

今までにおぼえたやり方だと、
たとえば写真共有サービスを題材に考える場合

sig User {
  photos: set Photo
}
sig Photo { 
  owner: one User
}
fact {
  // User <: photos = ~(Photo <: owner)
  // 相互な参照関係を↑いままでこう書いていたが、冗長だった。
  // ↓このほうがスマート。id:kencoba さん、ご指摘ありがとうございます。
  photos = ~owner
}

このように、

Photo の owner の限定子は、one にする
相互に参照しあう fact を書く

ことで
『Userに関係されていないPhotoは存在しない』
状態を定義できています。
しかしこれはあくまで静的な状態、つまり、エンティティ群のある状態を表現しているに過ぎないので、
『Userがサービスを退会したときにそのUserのphotosも削除されるかどうか』
というように、状態の遷移を伴う制約が成り立つかどうかは、定義できていません。

Orphan Removal の挙動を表現するにあたっては少なくとも、

まず、User.photos を削除。そのあとに User を削除

というところも表現すべきかと。

Orphan Removal
今回のような、エンティティ = sig の追加削除を検査するには、どうも以下のような要領でやるのが基本のようです。

状態を表す sig を作り
pred で、事前状態/事後状態で結びこみ
その pred の式を「成り立たせることができる」コンテキストを定義する

1.状態を表す sig を作る。
Tevfik Bultan 先生の資料では、事前状態・事後状態を、それぞれ sig で表現していたので、まずはそれに倣います。
この、状態を表す sig が、エンティティとしての sig を、フィールドに保持する形をとっています。
エンティティとしての sig を単独で持たせるだけでなく、そいつが持つ「関連」ごと保持するパターンが多いでしょうね、状態を管理する以上は。

　でも状態を sig で表現するのはちょっとコツがいりますすね。
sig の定義に続けて書く {} （シグネチャファクト）内は、fact なので、どんな条件でも書けるんですが、
ここには、例えば、"User - u" のように、User エンティティ群全体を利用するような条件は
書かないのが正しいようです。書くと、そのあとの pred を構成する段になって、反例ばかり出てきて行き詰まりますし。
あくまでこの sig の中で完結するように条件を書くようにするのがよいようです。

2014/01/08　訂正

PhotoRel_RightState の各フィールドが、すべてのインスタンスを指し示していることを
意図して fact を書いていたんですが、そのようになっていなかったので、修正しました。

one sig PhotoRel_RightState {
  u: set User,
  p: some Photo,
  rel: Photo some -> User
}
fact {
  // PhotoRel_RightState の各フィールドは、すべてのインスタンスを指し示している、という状態を表現するfact
  all anyUser: User, anyPhoto: Photo, rs: PhotoRel_RightState | 
		(anyUser in rs.u) && (anyPhoto in rs.p) && (rs.rel = rs.p <: owner) 
}
/* User.photos の削除後の状態 */
lone sig PhotoRel_OrphanRemovedState {
  u': one User,
  p': some Photo,
  rel': Photo some -> User
}{
  #p' = 0
  rel' = p' -> u'
}
/* そして User 削除後の状態 */
lone sig UserRemovedState { _u: lone User }{ #_u = 0 }

こうしました。なお、削除まわりの状態を表す sig は、通常状態を表す sig の限定子が one なのに対して、lone です。
削除のときだけあらわれる、一時的な状態にはこういう対処でよい？

2.pred で、事前状態/事後状態で結びこみ
ここでの pred は、事前状態/事後状態/操作するエンティティを引数にとり、
事前状態を事後状態を何らかのかたちでイコールで結びつけるのが基本の形みたいですね。
ここでは、子(Photo)エンティティの削除と親(User)エンティティの削除を、ふたつの pred に分けています。

pred deleteUser(rightState: PhotoRel_RightState, orphanRemoved: PhotoRel_OrphanRemovedState, 
            userRemoved: UserRemovedState, u: User) {
  // まず子を削除 ついで親を削除
  after_PhotoRel_OrphanRemoved[
  	orphanRemoved, 
  	(u.photos - u.photos) -> u
  ] && 
    after_UserRemoved[    // u.photos - u.photos がつまり削除をあらわしている。
      userRemoved, 
      u - u    // u - u がつまり削除をあらわしている。
    ]
}
pred after_PhotoRel_OrphanRemoved(orphanRemoval: PhotoRel_OrphanRemovedState, rel: Photo -> User) {
  orphanRemoval.rel' = rel
}
pred after_UserRemoved(userRemoved: UserRemovedState, u: User) { userRemoved._u = u }

3.pred の式を「成り立たせることができる」コンテキストを定義する
それを check とするわけです。

check {
  all u: User, 
    rightState: PhotoRel_RightState, 
    orphanRemoval: PhotoRel_OrphanRemoval, 
    userRemoved: UserRemovedState | 
      deleteUser[rightState, orphanRemoval, userRemoved, u]
}

ここは特にひねりはいらなかった。

以上です。
ところで、pred に引数を渡すときの要領は、これでいいのかな？
上の例でいうと、



  after_PhotoRel_OrphanRemoved[orphanRemoved, (u.photos - u.photos) -> u]

  after_UserRemoved[userRemoved, u - u]

のところ。
photos の削除を表すのに u.photos - u.photos と書いたり、
User の削除を表すのに、u - u と書いたりしてますが、
この書き方が適切なのかどうかは、自信ないです。

プログラム処理をAlloy で表現するときの基本は、
「状態を表す式=関数に、その式が真になるような引数を渡すこと」であるという原則は理解したんですが、
その「引数の渡し方」について学ぶ材料がもっと欲しいな。
WEBや書籍でみつかる Alloy のサンプルは、この、引数の渡し方の記述を示していない例が多くて、
なんでそんな文化になってんのかなー。

まあ、この先学習を進めて、様々なケーススタディをこなす段階になったら、きっとまた理解が進むでしょう。

さて、Orphan Removal をやったからには、
Nullify = 外部キーがnull を許容するケースについても考えないといけないですね。
それは次回に。

ソフトウェア開発のひみつ

Alloy Analyzer でOrphan Removal