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…