Alloyの~演算の結果確認。 arityが3だとエラーになる。 sig Mail { to:one Name } sig Name { address: one Addr } sig Addr {} fun transpose1 []:set univ -> univ { ~to } /* fun transpose2 []:set univ -> univ -> univ { ~(Mail -> Name -> Addr) }*/ …

早いもので、もう第6回FormalMethods勉強会のお知らせです。 http://atnd.org/events/4750 今回はマイスペース「大久保店」です。会場間違えないようにご注意ください。CoqはcpdtのChapter4からですかね。 Alloyは7月の無料セミナー直前対策です。 第5回で、…

Alloyの:>, sig Group {} sig Alias {} sig Addr {} fun address [] : set univ -> univ { Group -> Alias + Group -> Group + Alias -> Addr } fun domain_restriction []: set univ -> univ { address :> Alias } fun range_restriction []: set univ -> u…

Alloyの.(ドット)演算。 sig Mail { to:one Name } sig Name { address: one Addr } sig Addr {} fun dot_join []:set univ -> univ { to.address } pred show [] { } run show for 4

Alloyのarrow(product)演算のサンプル。funで定義すると何がおこっているかよく分かる。 sig Name {} sig Addr {} fun arrow []:set univ->univ { Name -> Addr } pred show [] { #Name = 2 #Addr = 2 } run show for 5

Alloyのデフォルトで用意されている集合、none(空集合)、univ(全体集合)、iden(Identity集合)を確認。 pred empty_set [] { #none > 0 } //run empty_set for 4 sig Unit {} sig Value {} pred univ_set [] { some u:Unit | u not in univ some v:Value | v …