Archive for 4月, 2011

引っ越し

4月 30th

Posted by snoozer05 in [...]

引っ越し

社員が増えて事務所が手狭になってきたこともあって、住空間のみ近所に引っ越し。今日と明日である程度区切りの良いところまで持っていきたいので、明日も引き続きがんばろう。

ツッコミを入れる

日記力

4月 29th

Posted by snoozer05 in [...]

日記力

140文字に満たない程度でも、少しずつ日々の記録を残していけるようにリハビリ。日記力が失われていたここ2ヶ月くらいのことも少しづつdumpしていけるといいな。

ツッコミを入れる

[TDD] テスト駆動開発チートシート

4月 29th

Posted by shuji_w6e in TDD

TDD（テスト駆動開発）のチートシートを作ってみた。 TDDBCでid:t-wadaさんが話している内容とかテスト駆動開発入門から引っ張ってきています。 ダウンロードはこちらからどうぞ。 PNGイメージ: http://dl.dropbox.com/u/1393956/tdd_cheatsheet.png PDFファイル: http://dl.dropbox.com/u/1393956/tdd_cheatsheet.pdf 追記 印刷・再配布などはご自由にどうぞ。 もし、元データ（OmniGraf ...

社内勉強会で発表した

4月 28th

Posted by HaseHiro in Ruby


Photo by Flickr http://farm1.static.flickr.com/110/255426966_e5d40089b8.jpg

以前の日記で書いていたのですが、4/27に無事第一回目の勉強会を終えることができました。

勉強会と銘打っていますが、初回は発起メンバーでLTしようという話になり、僕は「こんな僕でも伝えられるRuby」と題して、ありきたりな内容ではありますが、僕なりにRubyがもっと世の中に、ビジネスの世界に浸透する可能性の「芽」についてお話させて頂きました。

人生初LTだったのですが、それなりに好評だったようで、良かったです。

一応、PDF化してSlideShareにあげておきました。

公開できない箇所は伏せてあげているので、見苦しいところもありますが、興味があれば見てやってください。たいしたもんではないですけどねｗｗｗ

こんな僕でも伝えられるRubyについて
View more presentations from hasehiro


社内勉強会で発表した

4月 27th

Posted by HaseHiro in Ruby

Photo by Flickr http://farm1.static.flickr.com/110/255426966_e5d40089b8.jpg

以前の日記で書いていたのですが、4/27に無事第一回目の勉強会を終えることができました。

勉強会と銘打っていますが、初回は発起メンバーでLTしようという話になり、僕は「こんな僕でも伝えられるRuby」と題して、ありきたりな内容ではありますが、僕なりにRubyがもっと世の中に、ビジネスの世界に浸透する可能性の「芽」についてお話させて頂きました。

人生初LTだったのですが、それなりに好評だったようで、良かったです。

一応、PDF化してSlideShareにあげておきました。

公開できない箇所は伏せてあげているので、見苦しいところもありますが、興味があれば見てやってください。たいしたもんではないですけどねｗｗｗ

こんな僕でも伝えられるRubyについて
View more presentations from hasehiro

eclipse日本語化 for mac

4月 27th

Posted by onodes in [...]

pleadesを用いたとき．

echo "-javaagent:/Applications/eclipse/plugins/jp.sourceforge.mergedoc.pleiades/pleiades.jar" >> /Applications/eclipse/Eclipse.app/Contents/MacOS/eclipse.ini

RSpec Rails3 + ruby1.9

4月 27th

Posted by y_ogagaga in [...]

RSpec Rails3 + ruby1.9

今日も

Rubyist Magazine - スはスペックのス 【第 1 回】 RSpec の概要と、RSpec on Rails (モデル編)

を写経しました。

まだ、rails3の流儀になれずにハマりながらでしたがblog_spec.rbのテストコードが成功するところまでやりました。

次はEntryモデルをやります。

ツッコミを入れる

[Cocoa][iPhone]XcodeのビルドのRun Scriptではシグナルがブロックされているぽい

4月 26th

Posted by hiratara in Cocoa

XcodeのBuild Phasesの設定でRun Script を追加できますが、例えば以下のようなスクリプトを設定してビルド中に実行すると、kill -TERM を送っても止められなくなります。

#!/bin/sh
perl -e 'sleep 3600'

普段は困らないのですが、例えばTest::TCP のように子プロセスにTERMを送って処理を終了させるようなコードを動かす場合には困ってしまいます。

で実際に困ったわけで、@havanaclub_さんにアドバイスをもらったりしつつ見つけた解決法が以下。ただし、*nixのプロセスやシグナル周りはよくわかってないので、これが正しい解決法なのかはわかりません。

#!/usr/bin/perl
use POSIX ();

defined POSIX::sigprocmask(
    POSIX::SIG_UNBLOCK, 
    POSIX::SigSet->new(POSIX::SIGTERM), 
    undef
) or die;

これを、TERMを受け取りたいプロセス内でやっておけばOKです。Test::TCPであれば、serverブロック側。


ちなむと、実際にブロックされてるシグナルは以下です。

#!/usr/bin/perl
use POSIX ();

my $old_set = POSIX::SigSet->new(POSIX::SIGTERM);
defined POSIX::sigprocmask(POSIX::SIG_SETMASK, undef, $old_set) or die;

for (qw/
	SIGABRT SIGALRM SIGCHLD SIGCONT SIGFPE SIGHUP SIGILL SIGINT SIGKILL 
	SIGPIPE SIGQUIT SIGSEGV SIGSTOP SIGTERM SIGTSTP SIGTTIN SIGTTOU 
	SIGUSR1 SIGUSR2
/) {
	no strict 'refs';
	my $sig = &{"POSIX::$_"};
	$old_set->ismember($sig) and warn "$_ is blocked.\n";
}

__END__

【結果】
SIGALRM is blocked.
SIGCONT is blocked.
SIGHUP is blocked.
SIGINT is blocked.
SIGQUIT is blocked.
SIGTERM is blocked.
SIGTSTP is blocked.
SIGTTIN is blocked.
SIGTTOU is blocked.
SIGUSR1 is blocked.
SIGUSR2 is blocked.

止められる物は全部止めてる感じでしょうか？ ビルド中に割り込まれると何が起こるかわからんからってことだと思います、タブン。

会社のマシンにインストールしようとし..

4月 25th

Posted by y_ogagaga in [...]

会社のマシンにインストールしようとしたらエラーが出た。

最近自宅のMacでもちょいハマりしたのでメモっておく。

makeのログを見ると

Error running 'make ', please check /Users/ogasawara/.rvm/log/ruby-1.9.2-head/make*.log

とあったので、

readline をインストール

$ rvm package install readline

次に

$ rvm install 1.9.2-head --with-readline-dir=$HOME/.rvm/usr
$ rvm list
rvm rubies
  ruby-1.8.7-p174 [ x86_64 ]
  ruby-1.8.7-p249 [ x86_64 ]
  ruby-1.9.2-head [ x86_64 ]
  ruby-1.9.2-preview3 [ x86_64 ]

でインストールできました。

  • ruby のバージョン
$ ruby -v
ruby 1.9.2p188 (2011-03-28 revision 31204) [x86_64-darwin10.7.0]
  • rails3用のgemset作成
$ rvm gemset create rails3dev
info: Gemset 'rails3dev' created.
$ rvm gemset use rails3dev
info: Now using gemset 'rails3dev'
  • rails3 インストール
$ gem install rails --version=3.0.7
/Users/ogasawara/.rvm/rubies/ruby-1.9.2-head/bin/gem:4: warning: Insecure world writable dir /usr/local/bin/clang in PATH, mode 040777
Fetching: activesupport-3.0.7.gem (100%)
Fetching: builder-2.1.2.gem (100%)
WARNING: builder-2.1.2 has an invalid nil value for @cert_chain
Fetching: i18n-0.5.0.gem (100%)
Fetching: activemodel-3.0.7.gem (100%)
Fetching: rack-1.2.2.gem (100%)
Fetching: rack-test-0.5.7.gem (100%)
Fetching: rack-mount-0.6.14.gem (100%)
Fetching: tzinfo-0.3.26.gem (100%)
Fetching: abstract-1.0.0.gem (100%)
WARNING: abstract-1.0.0 has an invalid nil value for @cert_chain
Fetching: erubis-2.6.6.gem (100%)
Fetching: actionpack-3.0.7.gem (100%)
Fetching: arel-2.0.9.gem (100%)
Fetching: activerecord-3.0.7.gem (100%)
Fetching: activeresource-3.0.7.gem (100%)
Fetching: mime-types-1.16.gem (100%)
Fetching: polyglot-0.3.1.gem (100%)
Fetching: treetop-1.4.9.gem (100%)
Fetching: mail-2.2.17.gem (100%)
Fetching: actionmailer-3.0.7.gem (100%)
Fetching: thor-0.14.6.gem (100%)
Fetching: railties-3.0.7.gem (100%)
Fetching: bundler-1.0.12.gem (100%)
Fetching: rails-3.0.7.gem (100%)
Successfully installed activesupport-3.0.7
Successfully installed builder-2.1.2
Successfully installed i18n-0.5.0
Successfully installed activemodel-3.0.7
Successfully installed rack-1.2.2
Successfully installed rack-test-0.5.7
Successfully installed rack-mount-0.6.14
Successfully installed tzinfo-0.3.26
Successfully installed abstract-1.0.0
Successfully installed erubis-2.6.6
Successfully installed actionpack-3.0.7
Successfully installed arel-2.0.9
Successfully installed activerecord-3.0.7
Successfully installed activeresource-3.0.7
Successfully installed mime-types-1.16
Successfully installed polyglot-0.3.1
Successfully installed treetop-1.4.9
Successfully installed mail-2.2.17
Successfully installed actionmailer-3.0.7
Successfully installed thor-0.14.6
Successfully installed railties-3.0.7
Successfully installed bundler-1.0.12
Successfully installed rails-3.0.7
23 gems installed

だけどrdoc関連でエラーが発生。各gemはインストールされているようなのでここでは気にしないことにする

/Users/ogasawara/.rvm/rubies/ruby-1.9.2-head/lib/ruby/site_ruby/1.9.1/rubygems/custom_require.rb:36:in `require': /Users/ogasawara/.rvm/gems/ruby-1.9.2-head@global/gems/rdoc-3.5.3/lib/rdoc/ruby_lex.rb:831: invalid multibyte escape: /[\w\x80-\xFF]/ (SyntaxError)
from /Users/ogasawara/.rvm/rubies/ruby-1.9.2-head/lib/ruby/site_ruby/1.9.1/rubygems/custom_require.rb:36:in `require'
from /Users/ogasawara/.rvm/gems/ruby-1.9.2-head@global/gems/rdoc-3.5.3/lib/rdoc/parser/ruby.rb:11:in `<top (required)>'
from /Users/ogasawara/.rvm/rubies/ruby-1.9.2-head/lib/ruby/site_ruby/1.9.1/rubygems/custom_require.rb:36:in `require'
from /Users/ogasawara/.rvm/rubies/ruby-1.9.2-head/lib/ruby/site_ruby/1.9.1/rubygems/custom_require.rb:36:in `require'
from /Users/ogasawara/.rvm/gems/ruby-1.9.2-head@global/gems/rdoc-3.5.3/lib/rdoc/rdoc.rb:8:in `<top (required)>'
from /Users/ogasawara/.rvm/rubies/ruby-1.9.2-head/lib/ruby/site_ruby/1.9.1/rubygems/custom_require.rb:36:in `require'
from /Users/ogasawara/.rvm/rubies/ruby-1.9.2-head/lib/ruby/site_ruby/1.9.1/rubygems/custom_require.rb:36:in `require'
from /Users/ogasawara/.rvm/rubies/ruby-1.9.2-head/lib/ruby/site_ruby/1.9.1/rubygems/doc_manager.rb:42:in `load_rdoc'
from /Users/ogasawara/.rvm/rubies/ruby-1.9.2-head/lib/ruby/site_ruby/1.9.1/rubygems/doc_manager.rb:214:in `setup_rdoc'
from /Users/ogasawara/.rvm/rubies/ruby-1.9.2-head/lib/ruby/site_ruby/1.9.1/rubygems/doc_manager.rb:115:in `generate_ri'
from /Users/ogasawara/.rvm/rubies/ruby-1.9.2-head/lib/ruby/site_ruby/1.9.1/rubygems/commands/install_command.rb:147:in `block in execute'
from /Users/ogasawara/.rvm/rubies/ruby-1.9.2-head/lib/ruby/site_ruby/1.9.1/rubygems/commands/install_command.rb:146:in `each'
from /Users/ogasawara/.rvm/rubies/ruby-1.9.2-head/lib/ruby/site_ruby/1.9.1/rubygems/commands/install_command.rb:146:in `execute'
from /Users/ogasawara/.rvm/rubies/ruby-1.9.2-head/lib/ruby/site_ruby/1.9.1/rubygems/command.rb:278:in `invoke'
from /Users/ogasawara/.rvm/rubies/ruby-1.9.2-head/lib/ruby/site_ruby/1.9.1/rubygems/command_manager.rb:133:in `process_args'
from /Users/ogasawara/.rvm/rubies/ruby-1.9.2-head/lib/ruby/site_ruby/1.9.1/rubygems/command_manager.rb:103:in `run'
from /Users/ogasawara/.rvm/rubies/ruby-1.9.2-head/lib/ruby/site_ruby/1.9.1/rubygems/gem_runner.rb:64:in `run'
from /Users/ogasawara/.rvm/rubies/ruby-1.9.2-head/bin/gem:26:in `<main>'
  • gem の確認
$ gem list
/Users/ogasawara/.rvm/rubies/ruby-1.9.2-head/bin/gem:4: warning: Insecure world writable dir /usr/local/bin/clang in PATH, mode 040777
*** LOCAL GEMS ***
abstract (1.0.0)
actionmailer (3.0.7)
actionpack (3.0.7)
activemodel (3.0.7)
activerecord (3.0.7)
activeresource (3.0.7)
activesupport (3.0.7)
arel (2.0.9)
builder (2.1.2)
bundler (1.0.12)
erubis (2.6.6)
i18n (0.5.0)
mail (2.2.17)
mime-types (1.16)
polyglot (0.3.1)
rack (1.2.2)
rack-mount (0.6.14)
rack-test (0.5.7)
rails (3.0.7)
railties (3.0.7)
rake (0.8.7)
rdoc (3.5.3)
rubygems-update (1.7.2)
thor (0.14.6)
treetop (1.4.9)
tzinfo (0.3.26)

ツッコミを入れる

[Coq][Monad][math][planet]第15回FormalMethods勉強会に行ってきた

4月 23rd

Posted by hiratara in Coq

Coqのお勉強をしたくて出席してきました！ 非常〜にわかりやすいチュートリアルで、おかげさまで概要がわかるようになりました。やはりこういう抽象的な内容は、文章より実際にレクチャーして頂いた方が掴みやすいですね。


Coq入門(+α) / @tmiya_ さん

形式手法とは
  • 形式手法は色々ある
    • 自然言語ではなく、機械的検証可能な記述
    • 仕様アニメーション(Lightweight FM)
    • 定理証明系 → 実装を証明する or 証明からコードを生成する
  • 形式手法2.0
    • ハードの向上で、実用的に
    • 知識の普及
    • 正しさへの関心
    • スーツにもギークにも流行。組み込み系で特に。
  • 定理証明系とは？
    • 正しいもの(enumや自然数、公理)+正しい組合せ規則(自然演繹)
    • カリーハワード対応。正しい定理⇔正しいプログラム
    • ユニットテストでは得られないレベルの「正しい」
  • 証明はラクラク!(多少脚色ありｗ)
    • 30分程度のチュートリアルで十分
    • ユニットテストもそこまで簡単ではないよね？
    • 計算機によるレビューと考える。計算機への説明責任。
    • 定理証明系の動作は大昔より軽快
  • Domain Specific Languages
    • 読み書きが楽
    • 機能制限=安全性
  • DSLの正しさをCoqで証明
    • AURA : 認可・監査論理 →「誰は何をしてもよい」をコンパイル時に保証
    • 金融商品用
      • SECがPython使うって言ってるけどなんで？
      • FpMLはXML。仕様変更に弱い
      • 証明付きDSL使った方がいいじゃん
  • 形式手法のまとめ
    • 最近注目を浴びている
    • 仕様検証以外にも使える
Coq入門
  • 形式手法の比較
    • モデル検査: 手軽。状態爆発が起こる
    • 対話的定理証明: 訓練は必要。証明出来るものすべてに利用可。実装と直結。
  • Coq
    • 対話的定理証明のための言語処理系
    • Ocamlで記述。CIC(Calculus of Inductive Construction)
    • 高階述語論理で記述。"tactic" により、証明を構成
    • 機械的検証が可能。人間も検証が可能。
    • OCaml, Haskell, Scheme のプログラムの自動生成
  • Coqを使う
    • coqtopが対話環境。コマンドの最後にはピリオド。
    • 空白が省略できない部分もある
  • 型は推論。ただし、スコープによって2はnatか整数か変わる
  • Definition, Check, Eval compute in, Inductive などなど
  • ;を使うと、サブゴールすべてに対して実行できる(例:destruct b1; destructb2.)
  • 練習: 3値論理のドモルガン則
  • nat: peanoの自然数。0はOのこと。3は(S (S (S O)))のこと。
  • 再帰関数の定義はDefinitionではなく「Fixpoint」
    • 停止性の保証が必要。{struct n}。推論させることも可能。
  • 定理証明系へのよくある誤解
    • 「(すべてのプログラムに対して)チューリングマシンの停止性を判定することは出来ない」
      • ・・・が、Coqでは停止性が保証されたプログラムのみ受理
    • ライスの定理「(すべてのプログラムに対して)仕様を満たすか判定することは出来ない」
      • ・・・が、Coqで仕様を満たすことが判定された物は、当然仕様を満たす
  • Coqでは任意の割り算を定義するのは難しい (停止性の保証が難しい)
  • {}で定義をすると、型推論させられる: 例: {A:Set}
    • @関数名 と呼び出すと、型も明示的に指定できる(cond false 2 3 を @cond nat false 2 3 と書ける)
    • @nil とかは使うらしい
  • option型 : null値、Maybe のように値がないことを示す。
  • sumor型 : option型と同様だが、ない理由の証明も返せる
  • prod A B は A * B と書く。直積。
    • (x , y , z ...) は (pair .. (pair (pair x y) z)..) のこと
  • sum A Bは直和。
  • cons は :: と書く
  • 末尾再帰にこだわると、証明が難しくなるので注意が必要
  • Coqは直観論理なので、排中律は成り立たない
    • 「a^bが有理数になるような無理数がある」の証明。排中律を使っているが、実際の値を求めることができない
    • 公理と推論規則を利用
  • tacticを覚える必要がある(200個くらいあって結構ダブってるらしい!!)
    • assumption(trivial, exact(仮定だけじゃなく既存の定理へも使える)) → 仮定から
    • apply → ⊂E
    • intro, intros → ⊂I
    • destruct pq as [p q], split → ∧I
    • destruct pq as [p|q], left, right → ∨I_L, ∨I_R
    • ¬XはX→⊥なので、introする。
    • elim → ¬E
  • 二重否定が除去できないので、¬が入った定理は使いにくい
  • Curry-Howard対応
    • 証明はexactで直接与えてもよい
    • Coqは型チェックをしているに過ぎない
    • つまり、(命題論理であれば)Javaでも同じことができる。Coqは対話的に支援をしてくれているだけ
  • 述語論理 → 量化子∃∀を用いた記述
    • Coqは高階もサポート(∀P:A→Prop 述語)
    • forall についてはintro
    • exists についてはdestruct。exists で具体的な値を与える
  • 述語eq(=) → 型が等しい、コンストラクタが等しい、コンストラクタ引数が等しい
    • reflexivity → 同値の公理
  • simpl → 項を展開して簡単にするが、困ることもあるので注意
    • reflexivityは、内部で勝手にsimpleを呼ぶ。
  • n+0 は simplで展開不可 → 帰納法の利用
    • induction n as [|n']。内部的にはnat_ind という定理が使われる。
    • 帰納法はlist Aなどにも利用できる
  • rewrite->(rewrite),rewrite<- → 代入
  • SearchAbout xxxx. → 関連する定理の検索
  • 無闇にintroしない方がよい。
    • forall が具体化されて、帰納法の仮定が弱くなってしまう。
    • 慣れてくるとintroはしなくなる
  • Lemma と Theorem は Coqでは同じ
  • 引数と戻り値に条件をつけて定義 : Definition sub(m n:nat)(H:le n m) : {x:nat|x+n=m}
    • 引数は n < m、戻り値xは x + n = m
    • 定義すると証明が始まる。最後にDefined.とすると関数が定義される(Qed.としてはダメ)
    • 仕様を満たす関数が完成する
    • 利用するときは、le 2 5 というTheorem が必要
  • generalize dependent → ∀E
  • eapply → 自動引数を推測してapplyする
  • assert → 新しいゴールを設定する
  • Coqで関数と証明を扱う場合は？
    1. 関数を書き、定理を作って証明する
    2. 関数を書き、それをラップした証明付きの関数を定義する
    3. 証明から直接関数を定義
    4. refineを使って、証明を後回しにする
  • 今日やらなかったとこ
    • 自動証明のコマンドが楽(autoとかringとかmegaなど)
      • ただし、生成される関数は複雑になる
    • 各種ライブラリ
    • Haskell, OCamlのコードの生成
    • tacticの開発
    • 型クラス、Module
    • 名古屋のProofCafeとか、RubyとかJSとかSchemaとかの生成
    • Coq Standard Library
    • 「Twitter, MLとかで質問もらえれば、サポートします！」

懇親会

Coqでゴルフ → Anarchy Proof

合わせて読みたい

1234»