Alloy Analyzer
alloyで状態の変化を表現する方法はいろいろありますが、なるべく単純なかたちでこれを実現してみたいと思います。 状態は、事前状態と事後状態のふたつだけ 事前状態と事後状態が同時に表示される中で、どのAtomが事前状態にあり、その事後状態を表すのがど…
If you are software developer, you often implement the object which generated by some other event. But when I represent such objects on Alloy, I always make a mistake. Why? Now I've got the reason. Here it is.Modeling a "login page".Genera…
前回扱った仕様の完全版を記述してみます。 <仕様> 何枚かの"くちばし" があります。くちばしには、金、銀、黄色、の三種の色分けがあります。 金のくちばし1つにつき、缶詰め1つと交換できます。 銀のくちばし5つにつき、缶詰め1つと交換できます。 これ…
ruby のユーザーにとって、Array#select() などの、「ブロック」の概念を化通用したメソッドは強力に便利です。 こんなふうに。 arr = "second baseman", "third baseman", "first baseman", "shortstop" # => ["second baseman", "third baseman", "first b…
前回のモデリング、を何度もいじくり回しているうちに、間違いが2点見つかったので、まず訂正します。 一つ目は、MinInterval。 当年と座り始めた年との間には、最低3目盛り、距離でいうと、4離れていないといけない という理由で、 one sig MinInterval { v…
前回あつかった「石の上にも三年」のモデリングを再度試みます。 前回まで、 「Alloy で発見されたモデルインスタンスは、つまりそのまま(Happy pathの)テストデータとして 使えるんじゃないか、つまり、Alloy はテストデータ生成器として転用できるんじゃ…
“石の上にも三年” という格言を Alloy でモデリングします。まあ、格言は実はどうでもよくて、Alloyにおける、数値(Integer)の扱いについて確認したかったんです。Alloy 教科書 の131ページには 整数の演算が必要に思えるなら、考え直したほうがいい。 よ…
前回、写真共有サービスを想定して、@OneToMany(orphanRemoval=true) な エンティティ群を定義してみました。その書き直し版です。前回は、「状態をあらわすsig」を、書くと言っておきながら、 操作対象のインスタンス(=削除するUserとPhoto)のことだけを…
今回は、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 というのは、えーと僕も素人なんで、説明が難しいんですが 独自の言語でモデリングを記述するようになってます そうすると、モデル同士のあり得る組み合わせを自動で…