a-sanさんの日記より、 http://d.hatena.ne.jp/a-san/20090626/p2Alloyだとこれだけなのか？ /* http://d.hatena.ne.jp/a-san/20090626/p2 */ abstract sig State { transient:set State } one sig O,A,B,C,D,E,F,G,H,I extends State {} fact { transient =…

12/22 18:00-20:00 「関数型言語＆形式手法セミナー(1)F#が拓く新たな世界」 ということで、有限会社ITプランニングの小笠原さんに セミナーを開催していただいた。http://kokucheese.com/event/index/6300/来年の活動に向けて、十分な意見を集めることが出…

Clojureで引っかかった論文 "Multi-core Parallelization in Clojure – a Case Study.",Johann M. Kraus "Modeling Ontologies as Executable Domain Specific Languages",Dragan Djuric

(defmacro もし [test then t-exp else f-exp] `(if ~test (do ~@t-exp) (do ~@f-exp))) こうすれば、 echoserver=> (もし true ならば (println "a") でなければ (println "b")) "a" と出来るわけだ。

TAPLのラムダ計算の箇所をちょっとメモ書き。 (def tru (fn [t f] t)) (def fls (fn [t f] f)) (def iff (fn [c t f] (c t f)))

https://gist.github.com/736375 とりあえず動く状態。

今回の発表資料は深町氏作のClojureによるプレゼンツール、L5 (https://github.com/fukamachi/L5)を使用した。便利。 2010年振り返り https://gist.github.com/729087今年も本当にありがとうございました。 勉強会は1年間で12回開催。 イベント等発表あり、…

http://www.csp-consortium.org/index.html 「形式手法ツールAlloy Analyzerを用いたアジャイルモデリング」 という題で発表してきた。見返りとして、Alloy Analyzerに対する提言以外にも CSPの図形表記の拡張や、 並行システムを図形表現するなら３次元がい…

でました。 http://www.amazon.co.jp/dp/4864010099翻訳が終わって改めて思うのは、「リファクタリング」の訳者あとがきでの、友野氏の言葉。 「この技法は、依然としてリアルタイム系、分散系、データベースのように 状態の変化に敏感なソフトウェアにつき…

だんだん込み入ってきた。 Include "../usr/guru-lang/lib/nat.g". Include "../usr/guru-lang/lib/plus.g". Define plusZ' := foralli(x:nat)(u : {x = Z}). trans cong (plus * *) u % (plus x x) = (plus Z Z) join (plus Z Z) Z. % (plus Z Z) = Z Defin…

Commutativityの証明。 Include "../guru-lang/lib/plus.g". Define ch4_th : Forall(n m:nat). { (plus n m) = (plus m n) } := induction(n:nat) return Forall(m:nat). { (plus n m) = (plus m n) } with Z => foralli(m:nat). trans cong (plus * m) n_e…

Chapter4を読み進める。 Include "../lib/plus.g". Classify induction(n:nat) return Forall(m:nat). { (plus n (S m)) = (S (plus n m)) } with Z => foralli(m:nat). trans cong (plus * (S m)) n_eq trans join (plus Z (S m)) (S (plus Z m)) cong (S (…

というわけで一通り証明が終わったようだ。 Include "../usr/guru-lang/lib/plus.g". Include "../usr/guru-lang/lib/mult.g". Include "../usr/guru-lang/lib/bool.g". Define 3_8_1_1 := join (mult zero three) zero. Classify 3_8_1_1. Define 3_8_1_2 :…

http://code.google.com/p/guru-lang/ Coqに強く影響を受けたとかいう、Guruという言語があります。 JVM上で動く、証明機能付きの関数型言語です。こまかいことはともかく、"Verified Programming in GURU"(http://guru-lang.googlecode.com/svn/branches/1.…

BirthdayBookという仕様がある。 http://spivey.oriel.ox.ac.uk/~mike/zrm/これをAlloyで書いてみた。 open util/relation sig NAME {} sig DATE {} sig BirthdayBook { known: NAME, birthday : NAME -> lone DATE } { known = dom[birthday] } pred AddBir…

LinuxでもFormsが動くんですね。 open System.Drawing open System.Windows.Forms type HelloWindow() = let frm = new Form(Width = 400, Height = 140) let fnt = new Font("Times New Roman", 28.0f) let lbl = new Label(Dock = DockStyle.Fill, Font = …

TAPL(Types and Programming Languages)の課題を適当に実装する。 type Term = | TmTrue | TmFalse | TmZero | TmIsZero of Term | TmIf of Term * Term * Term | TmSucc of Term | TmPred of Term | TmNot of Term let rec Eval t = match t with | TmTrue …

なんとなく言語比較。 --Clojure (defn rotate [lst] (reverse (map reverse lst))) --Common Lisp (defun rotate (lst) (reverse (mapcar #'reverse lst))) --F# > let rotate lst = - List.rev (List.map List.rev lst);; val rotate : 'a list list -> 'a…

tmiyaさんが出している問題に触発されました。 http://study-func-prog.blogspot.com/2010/07/coq-coq-99-part-1.html数をこなせば自然と出来るようになるのではないか。 Section FoundationOfSoftwareScience. Lemma e_1_23 : forall A B C : Prop, (A -> B…

連載：モデリング技術の新しい動向 第3回 形式手法とモデリング - Alloy Analyzerを中心にという記事が掲載された。 http://thinkit.co.jp/story/2010/09/22/1766今回はFormal Methods Forumのみなさんの力を借りられなかったのが心残り。最低限の査読は入っ…

Alloy Analyzerはアジャイルモデリングをサポートできるツールだと 思っているわけですが、現時点では識別子に日本語が使えません。 このままだと分析モデリングに使えない(と、会社の人が文句を言ってきた)。コードを調べてみたら何のことはなかったので、…

ASDF(Another System Definition Facility)というのはCommon Lisp版パッケージ管理ライブラリ(http://www.cliki.net/asdf)。Windowsではどうにも動いてくれないなーと思っていたが。 http://f34.aaa.livedoor.jp/~kumadasu/pukiwiki/index.php?Maxima#w69d91…

http://alloy.mit.edu/community/node/506 に、LaTeXでAlloyのリストを表示するサンプルがあったので試す。 \documentclass{jarticle} \usepackage{amsmath} \usepackage{listings,jlisting} \lstdefinelanguage{Alloy} {morekeywords={abstract, all, and, …

お客様と講座開催日程の連絡をすることがあるので、 あってもよいかなと。 (defun weekday (year month day) (nth (nth 6 (decode-time (encode-time 0 0 0 day month year))) '(日 月 火 水 木 金 土))) (defun string-to-weekday (yyyymmdd) (let* ((ymd (…

市民講座でやってました。 ;最大部分列和問題 ;数列の中で和が最大となる、連続している部分列の和を求める (def x [31,-41,59,26,-53,58,97,-93]) (defn sum [a b] (if (< 0 (+ a b)) (+ a b) 0)) (defn s ([coll-x] (s (next coll-x) (list (first coll-x)…

いわゆる「ルール30」。 もっとコンパクトなコードにする方法があったら教えてください。 (defn next-cell-state [x y z] (cond (and (= x "□") (= y "□") (= z "□")) "□" (and (= x "□") (= y "□") (= z "■")) "■" (and (= x "□") (= y "■") (= z "□")) "■"…

7/12 名古屋市工業研究所にて、無事実施できました。ここまでいろいろとネタ提供、成果物レビューしてくれたみなさん、ありがとうございました。 当日会場でサポートしてくれたyoshihiro503さん、ありがとうございました。使用した資料はこちらにあります。 …

(defn hq9+ [commands] (let [ reg 0 h-eval (fn [x] (cond (= x \H) "Hello World" (= x \Q) commands (= x \9) "99 Bottles" :else "Illegal Command"))] (map h-eval commands))) 正直"+"命令は逃げてるわけですが、 http://rosettacode.org/wiki/Execute…

出た。 http://userweb.cs.utexas.edu/users/moore/acl2/Alloyが一段落したら挑戦します。

頑張って計算はしているようだが、 数分では結果がかえってこない・・・。 /* sudoku solver */ sig Cell { x:Int, y:Int, v:Int } { x >= 0 and x <= 8 y >= 0 and y <= 8 v >= 1 and v <= 9 } fact AllCellsPosition { no disj c1,c2:Cell | c1.x == c2.x …