alloyで状態の変化を表現する方法はいろいろありますが、なるべく単純なかたちでこれを実現してみたいと思います。 状態は、事前状態と事後状態のふたつだけ 事前状態と事後状態が同時に表示される中で、どのAtomが事前状態にあり、その事後状態を表すのがど…

前回、写真共有サービスを想定して、@OneToMany(orphanRemoval=true) な エンティティ群を定義してみました。その書き直し版です。前回は、「状態をあらわすsig」を、書くと言っておきながら、 操作対象のインスタンス（=削除するUserとPhoto）のことだけを…

今回は、JPAでいう Orphan Removal のような、依存のある関連を扱ってみます。 Ruby on Rails でいうと :dependent => :destroy とか、 :dependent => :delete_all といった、 アソシエーションのオプションを使って制御するアレですね。 JPA2でいうと、 @On…

(※追記あり) (※結論へ) 今回も引き続き、pred について調べます。 以下のような動きを Alloy で表現する方法を探りたいと思います。 User エンティティが Instantiate される。 User エンティティの id フィールドに、発番されたidが格納される。 テーブルを…

モデリング検査ツール Alloy Analyzer を使いたい！のエントリ。第五回目です。今回は、条件のある関連を扱ってみます。 ここでいう条件のある関連っていうのは、具体的にいうと、Ruby on Rails でいうところの ポリモーフィック関連です。例として、faceboo…

モデリング検査ツール Alloy Analyzer を使いたい！のエントリ。第四回目です。今回は Many to Many をモデリングしてみます。映画エンティティと出演者エンティティの関係づけ。通常、RDB上で実現される Many to Many は、中間テーブルを使いますね。 こん…

モデリング検査ツール Alloy Analyzer を使いたい！のエントリ。第三回目です。今回は、自己参照用の関連を定義してみました。例えば、変更履歴を管理するために、「自身のひとつ前のレコード」の id を、外部キーとして保持するようなケースです。 こういっ…

モデリング検査ツール Alloy Analyzer を使いたい！のエントリ。第二回目。先回はシンプルな『親子関係』をモデリングしました。 その際の fact（＝モデル定義から導かれる静的なタイプの制約を書くところ） が、明らかに場当たり的な記述だったんで、もっと…

モデリング検査ツール Alloy Analyzer を使いたい！モデリング検査ツール Alloy Analyzer というのは、えーと僕も素人なんで、説明が難しいんですが 独自の言語でモデリングを記述するようになってます そうすると、モデル同士のあり得る組み合わせを自動で…