次回に向けて、はやくも落ち穂拾い。 double intだけでなくdoubleでも使えるか、確認。 #include <stdio.h> #include <stdlib.h> #include <assert.h> int main (int argc, char **argv) { int _rand = rand(); double r; #ifdef __CBMC__ __CPROVER_assume(0 <= _rand && _rand <= RAND_M</assert.h></stdlib.h></stdio.h>…

Postgres-XCの単一障害点であるgtmを多重化するmgtmを作ったので公表する。これはAPPIA版の改良でJGroupsを使っている。 2011年2月現在、最新版はver0.9.3〜0.9.4だが、mgtmはver0.9.2で動作する。もうすこしUI修正や動作を整えてから公開しようと思ったが、…

昨日、某懇親会で天文関係者と話す機会があり、なぜか一瞬フォーマルメソッドの話に。情報工学ってのはほんとにサイエンスなのかい？*1ってな流れから。 否定的な意見も少なくないフォーマルメソッドについて、注目している理由を書いてみる。 それ動くの? …

"CBMC"というモデル検査ツールの使い方を学ぶ。組込み分野では有名なツール。すでに開発終了したという人もいる*1が、最新版3.9は2010.12.19リリース。2010年には3.6,3.7,3.8,3.9と4バージョンリリースなので、アクティビティが落ちているようにはみえない。…