プロフィール
| |
- Author:あろは (alohakun)
- 若槻俊宏 (WAKATSUKI toshihiro)
連絡先 : alohakun ___at___ gmail.com mixi : http://mixi.jp/show_friend.pl?id=182927 twitter : http://twitter.com/alohakun
abstract
プログラミングという人間の知的行為を体系化し,単なる職人芸ではなく,サイエンスにするための研究をしています.
具体的には,等価変換計算モデルに基づいた,仕様記述からのプログラム合成の研究をしています.
もっと噛み砕くと,プログラムの正しさをどのように定式化し,どのような枠組みで,どのように変換を進めていけば,正しさを保証したまま,効率的なプログラムを手に入れることができるのか,ということについて研究しています.
キーワード : equivalent transformation, computation model, programming paradigm, formal specification, program synthesis





|
FC2カウンター
| |
|
ブロとも申請フォーム
| |
この人とブロともになる
|
|
Debian GNU/Linux で加速度センサを使う
| 2008/04/23(水) 01:49:28
|
とりあえず,DesignWave 2008 年 5 月号の加速度センサは,miniUSB-USB 変換ケーブルでつなぐだけで LED が点いて認識されました.
僕が使ったのは,ヨドバシカメラで 750 円で買った 型番 AUSM20BK 「極細 USB ケーブル PSP 対応 USB 2.0 対応 mini-B タイプ 2m」とかいうやつです.mini-B タイプなら何でも良いと思う (最初 miniUSB にもいっぱい種類があってかなり困った.つながってよかった)
最初は
$ cat /dev/ttyACM0
しても,何の反応もありません.
$ echo '*' > /dev/ttyACM0
とかすると動きだす感じです.
$ cat /dev/ttyACM0 2052,2022,2873 2060,2022,2896 2053,2028,2866 2047,2015,2905 2050,2020,2886 2051,2023,2885 2052,2027,2865 2056,2026,2888 2049,2022,2896 2054,2024,2887 2059,2025,2873 1994,2005,2897 2076,2028,2861 2057,2022,2868 2055,2024,2886 2050,2025,2889 2082,2027,2837 ...
う〜ん,とりあえず gnuplot で表示してみた.Z 軸のセンサーだけ
$ cat /dev/ttyACM0 | awk -F, '{print NR" "$3}' > log.txt
// センサーを振ったりしてみる
^C $ gnuplot gnuplot> set yrange [1000:5000] gnuplot> set terminal png Terminal type set to 'png' Options are 'nocrop medium ' gnuplot> set output "log20080423.png" gnuplot> plot "log.txt"

なるほど.最初激しく振って,こうはんはゆっくり大きく動かしたりしたから,こんなもんだと思う.
gnuplot (じゃなくてもいいけど) って,リアルタイム表示はできないのかなぁ… まぁ,何秒かごとにログを捨てて,再描画を繰り返せばできそうだけど.こういういかにも理系っぽい,実験結果の可視化とかはあんまりやったことが無い文系ソフトっ子なので,よくわかりません…
最近はヨドバシカメラしか行かないからすっかり忘れてたけど,札幌駅前のツクモ電気って,思いっきりロボット王国あるじゃん !「関東以北最大級」という恵まれた環境が,実は思いっきり近所にあったという.
DEPO ツクモ札幌駅前店
もしかしてDWM追加部品キットとか店頭に置いてたりするのかな (これ買って,ハンダ付けすれば USB 経由でプログラマブルになる.SD カードからプログラムをロードすることもできるようになる).今度行って見てみよう.店頭の方が保証とかもいろいろ楽だし,送料の1000円がかからないのは大きい (一応読者プレゼントに応募したので,まだ買わないけど(笑)) 1000 円の品買って,送料1000円とかばかばかしすぎるからなぁ
gnuplot でリアルタイム可視化できた.
$ cat kskd.plot set yrange[1000:5000] plot "log.txt" pause 0.1 reread watch $ echo '*' > /dev/ttyACM0 $ cat /dev/ttyACM0 | awk -F, '{print NR" "$3}' > log.txt & $ gnuplot kskd.plot
で,0.1 秒ごとに log.txt を watch して再描画されるようになる.
参考 : Fujie's Blog : 2006年07月08日 gnuplotでリアルタイムプロット
|
小ネタ|TB:0|CM:0|
|

▲
| |
|
NaN の話
| 2008/03/01(土) 16:19:30
|
たまたま検索で見つけて,なんとなく面白かったのでメモ.
Shiro:log:2005前半 (2005/05/11 15:52:00 PDT)
天泣記2005/05/01 64bit なシステムで、64bit 浮動小数点数を即値で扱うとしたら、どういうふうにして浮動小数点数を区別するのが適切か?
おそらく、(Fixnum が 63bit 整数であるのと同様に) 64bit よりもちょっと小さい浮動小数点を定義することになる。たぶん指数を削るのが適切だと思うが、他の選択肢はあるか?
「浮動小数点数でNaNになるビットパターンに他の型のオブジェクトを詰め込む」というLisp処理系があったはず。実装したのはFritz Kunze (Franz Inc.の社長)。 Fritzから聞いたところによれば、浮動小数点数の性能は格段に向上したが、非常に稀な確率で演算結果が別の型のビットパターンになってしまう可能性があって使えなかったそうだ (ここんとこ、具体的な話は聞かなかったんだけど)。
ネイティブコンパイラを持つ現在のCL処理系では、型をちゃんとdeclareしとけばコンパイラがboxing/unboxingを避けるコードを出してくれる。でもインタプリタでうまくやる方法は知らない。 VM上に浮動小数点数レジスタを持っておくなんてことをちらりと考えたんだけど、継続やクロージャ作成に伴うコンテキストの保存がとても面倒になりそうなんで試してない。
日々の流転 2008-02-23 RHG読書会::東京 ふつパイラ篇
久しぶりの青木さん本 & 久しぶりの面子。
3次会にて、先日の最近のRuby処理系の話に関係してLuaの浮動小数点数の表現の話が出た。 Luaは浮動小数点数も整数もポインタも全部まとめたunionにタグをつけて、rubyでいうところのVALUEとして扱っているそうな。ただ、タグの部分が勿体無いので、IEEE 754のNaNの仮数部は0以外であれば良いことを利用して、そこに整数とポインタを埋め込もうとしているとかしたとか。仮数部は52bitあるので、32bit環境ならば整数やポインタは余裕で埋め込めるが……
ハードウェアってまだまだ魔窟だよなぁと.理屈上は正しくても,FPU の気まぐれとかでバグが発生したら,ほぼ突き止めるのは不可能だよなぁと思うと,いろいろ躊躇してしまう場面もありそう.
まぁ,そんなこといったら,熱暴走とか,宇宙線とかでメモリ上の値がランダムに変化したとか,他にも再現不可能,あるいは困難なバグはたくさんあるので,浮動小数点数だけがキモくて不恰好な存在というわけではないんだけど.
ソフトウェアの世界,たくさんの抽象化の壁に守られて,数学的な理屈が通る世界ってのは,幸せだなぁと.ハードウェアの住む物理世界は,どちらかというと熱力学とか統計的な世界というイメージがある.natsutan さんが twitter で,今日はあたたかいから回路が上手く動かなかった,とか言ってるのを見てそんなことを思った.ハードウェアは生き物ですね.
|
小ネタ|TB:0|CM:0|
|

▲
| |
|
プレゼンタイマー
| 2008/02/10(日) 02:45:25
|
Windows XP はどうでもいいゲームとかアクセサリはたくさん入ってるのに,なぜかストップウォッチが標準で入って無い.修論発表会の練習の時,時間が計れないと困るので,ActiveTcl で作った.
button .start -text 開始 -font {{MS ゴシック} 20} -command { bell global startTime global end global input global over set startTime [expr [clock seconds] + [expr $input * 60]] set end 0 set over 0 timer }
button .end -text 終了 -font {{MS ゴシック} 20} -command { global end set end 1 }
grid .start .end -columnspan 3 -sticky ew
proc timer {} { global buffer global startTime global end global over set currentTime [clock seconds]
if {$over == 0} { set count [expr $startTime - $currentTime] if {$count <= 0} { set over 1 set startTime [clock seconds] bell } } {set count [expr $currentTime - $startTime]}
set f "" if {$over == 1} {set f "- "} set buffer [append "" $f [format "%02d" [expr $count / 60]] 分 [format "%02d" [expr $count % 60]] 秒] if {$end == 0} {after 1000 timer} }
label .rem -text "残り時間" -font {{MS ゴシック} 32} grid .rem -columnspan 3
label .timer -textvariable buffer -font {{MS ゴシック} 96} set buffer 09分00秒 grid .timer -columnspan 3
entry .input -width 2 -textvariable input -font {{MS ゴシック} 20} set input 9 label .m -text "発表時間(分)" -font {{MS ゴシック} 20} label .t -text "分" -font {{MS ゴシック} 20} grid .m .input .t
Windows の場合は,適当に ptimer.tcl とかの拡張子で保存しておくと,ダブルクリックだけで (ActiveTcl が関連付けてあれば) 起動するので便利.

Linux とかでも tcl/tk が入ってれば動くと思う (フォント名とかは変えないと駄目かも).
|
小ネタ|TB:0|CM:2|
|

▲
| |
|
なつたん Verilog
| 2007/10/19(金) 18:38:52
|
偶然気が付きました.カコイイ !

僕もいつか「あろは gcc」と出る日がくるまでがんばります !

|
小ネタ|TB:1|CM:0|
|

▲
| |
|
Unicode はもっと有効に使うべき
| 2007/03/21(水) 10:53:55
|
ワラタ
きしだのはてな ■ throwの代わりに(ノ∀`)
捕まえる側はこんな感じ。
(屮゚Д゚)屮{ Reader r = new FileReader("aa"); (´-`).。oO(Hello Java); } IOException Σ(゚д゚lll) { _| ̄|○ }
Fortress もびっくりだね !
ひらさんとこについてたコメント経由でたどり着いた方の日記なんだけど.
「人間の意識は計算不可能」 云々のところには,非常に強い違和感を感じた.
人間が計算不可能なことをしているということは証明不可能? オブジェクト指向の中の計算不可能性 計算不可能だけど決定論的なこと
まぁ,単なる用語の使いかたの問題なのかもしれない.個人的には,思考する機械は実現可能だし,人間は何らかのアルゴリズム通りに動いていると思いますがね (ただし,それを人間自身が理解できるかどうかはまた別問題).
と,スルー力を遺憾無く発揮し,立ち去ろうとしたその刹那 !!
目に入ってきた面妖な理論と 「区体論」 の文字っ !! そしてリンク先の特徴的な文体 ! すぐにピンっ ときた管理人が,おそるおそる筆者名を確認すると…
キタ━━━━(゚∀゚)━━━━ッ !!
今,まさに旬のあの御方が !!
君は 『引力』 を信じるか ? Unicode の引力 ! 来いッ ! プッチ神父 !!
まぁ,オイラぁ 深入りしないでクールに去るぜ w うひひひ
|
小ネタ|TB:0|CM:2|
|

▲
| |
| |
|
|
最近のコメント
| |
| リンク
| |
このブログをリンクに追加する
| 最近のトラックバック
| |
| 人生の残り日数
| |
日本人男性の平均寿命は 28700日.
| RSSフィード
| |
| カテゴリー
| |
|
|