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

プログラムの処理をAlloyで表現する基本型は、 事後状態をあらわす式に引数を与えること であるってことを前々回確認しました。図を再掲しましょう。 今回はそこに、繰り返し処理を織り交ぜてみます。形式手法入門―ロジックによるソフトウェア設計―作者: 中…

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

※ 2013/07/31 ソースコードを修正しました。ここまでは、Alloy Analyzer を使って、エンティティの関連を表現してきました。 しかし形式記述言語 Alloy には pred (=predicate 述語) というものがあります。ん、あれ？述語？Alloy の記述の基本は式です。tru…

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