状態遷移を表現するように変更。 open util/ordering[State] as so /* 4日で学ぶモデル検査 システムα 仕様： 変数a 0->1 1->2 2->0と繰り返して変化する。 ただしb=1のときは次の時点でもその値を保ち変化しない。 初期状態は0とする。 変数b 0->1 1->2 2->…

「4日で学ぶモデル検査」より。 愚直にモデリングしてるだけで、これではスイッチがOn,Offされることを 確認できない・・・ open util/ordering[State] as so /* 4日で学ぶモデル検査 システムα */ abstract sig Switch {} one sig On,Off extends Switch {}…

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 …

やったー！VBAとおさらばだー。 user=> (import '(org.apache.poi.hssf.usermodel HSSFSheet HSSFWorkbook HSSFRow HSSFCell)) org.apache.poi.hssf.usermodel.HSSFCell user=> (def wb (new HSSFWorkbook)) #'user/wb user=> (import '(java.io FileOutputS…

最初に見つけた要素だけ置き換えたいんです。 (use '[clojure.contrib.seq-utils]) ;(defn- position-sub [x coll i] ; (if (= (first coll) x) i ; (position-sub x (rest coll) (inc i)))) ; ;(defn position [x coll] ; (position-sub x coll 0)) ; ;別バ…

Clojureハッカソンで教えていただいたこと、その１。leiningen:Clojure版MAVENみたいなもの。 http://github.com/technomancy/leiningenWindows版は自動インストールできないので、 以下のファイルを用意する。 leiningen-1.1.0-standalone.jar lein.bat(Git…

CommonLispにもML系Matchがないのか。 (in-package "ACL2") (defun not-3 (x) (cond ((equal x "yes") "no") ((equal x "no") "yes") ((equal x "maybe") "maybe"))) (defun and-3 (x y) (cond ((and (equal x "yes") (equal y "yes")) "yes") ((and (equal …

某ProofCafeではCoqでやってみたという話の、 リストの反転問題。 reverse (reverse xs) = xs http://study-func-prog.blogspot.com/2010/04/coq-reverse-reverse-xs-xs.htmlACL2ではどうなんのかな、と思ってやってみた。 環境はACL2s。 (in-package "ACL2"…

clojure.contrib.typesの使い方がいまいち分からない。 もうちょっと賢いマッチングしてくれないのかな。 (use '[clojure.contrib.types]) (defn not-3 [x] (match [x] [:yes] :no [:no] :yes [:maybe] :maybe)) (defn and-3 [x y] (match [x y] [:yes :yes]…