形式仕様記述Alloyを試してみる - きしだのHatena
試してみるよ。 とりあえず商品をまとめたセット商品についての仕様を書いてみる。 まず商品の定義 module exec/shohin sig Shohin{} pred show{ } run show sigはJavaとかのclassだと思えばだいたいOK。 なんか商品がみっつ出た。 じゃあ、セット商品を定義してみる。 sig SetShohin{ bundle: set Shohin } おー、同じ商品が３つのセットに含まれてしまった。Alloyさんイヤらしいとこついてくる。 ということで、ひとつの商品は多くてもひとつのセットにしか含まれない、っていう制約を加えます。 fact { all s: Shohin | lone bundle.s } 書き下ろすと「すべての商品について、商品をbundleとして持つのはたかだか１つ」になるんですけど、この、フィールドを左に書く書き方は通常のプ
Alloy4 Tutorial
Alloy 4 Tutorial Materials Tutorial Slides: Session 1 - Intro & Logic (ODP) (PDF) Session 2 - Language & Analysis (ODP) (PDF) Session 3 - Static Modeling (ODP) (PDF) Session 4 - Dynamic Modeling (ODP) (PDF) files with the ".odp" extension can be opened with OpenOffice Exercises Properties of Binary Relations (properties.als) Refactoring Navigation Expressions (distribution.als) Modeling the T
陶器のカタログ受発注の仕組みをAlloyで - osiire’s blog
仕事に関連して、とあるビジネスの仕組みを記述する必要があったので、Alloyで書いてみた。具体的には、 陶器を製造・販売している企業がたくさんいる。 その企業が集まってカタログを作り、そのカタログを見たお客さんから受注を受ける。 もちろん、カタログに載っている自社製品以外の陶器を注文受けることもあるので、それはカタログを共同で出している企業さんから仕入れて売る。 企業は複数のカタログに参加している。 という、よくあるカタログ販売の仕組み。本当は日付とか請求書とか納品書とかも定義してあったけど、大きくなりすぎるので割愛。コードは以下。 // // 陶器のカタログ販売受発注のモデル化 // // カタログから注文をするお客さん sig Customer { } // カタログ参加業者 sig Seller { belong : some Catalog, // 属しているカタログ produc
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
日々精進 - スパークスシステムズ ジャパン代表のBlog:Alloy Analyzerによるクラス図の検証(3) - livedoor Blog（ブログ）
