OCamlコードをCoqで検証できる "CFML" で 証明コンペに挑戦 (未完) - keigoiの日記
VSTTE 2012 Software Verification Competition というソフトウェア検証のコンペがあった。参加はオープンで、問題文もPDFで配布されている。 id:yoshihiro503 がチームtebasakiというチームでがんばっていた。僕はCoqに慣れていなかったのでチームに入るのは見送った（というかチームの人数上限4人で入れなかった）。 仕事や出張の片手間でやっていたので、結局一問も検証できなかったけど、楽しかった。 検証にはCFMLというツールを勉強しながら使った。 これを使えば OCaml のソースコードを Coq で検証できる。 それも ref型による破壊的代入つきの手続き的なOCamlを含む。 そして Coqと違い、プログラムは停止しなくてもいい。 つまり、CFMLを使えば、 手続き型プログラムを、ホーア論理+分離論理(のようなもの;後述)を使って
Language.C (cont.) - flexible array member(C99) を サイズ0の配列(GNU C互換)に変換 - keigoiの日記
jhcが生成した手元のコードを gcc 2.95でコンパイルするにはもうひとつ障害があった． JHCはサンクを以下の構造体で管理するようだ： typedef struct node { fptr_t head; sptr_t rest[]; } A_MAYALIAS node_t; typedef struct dnode { what_t what; sptr_t rest[]; } A_MAYALIAS dnode_t; ここで、 rest[] は flexible array member とよばれ、そのままだと(おおむね)サイズ0の配列として扱われる．この構造体を使うには、malloc(sizeof(node_t)+ほげほげ)のようにして、rest分の領域を確保する． これのp.103, 6.7.2.1節の16に載ってます： http://www.open-std.org/JTC1
メモリアロケーションとコンテキストスイッチの関係 - keigoiの日記
OCamlのコンテキストスイッチのタイミングを調べた。 OCaml では OSネイティブのスレッド (pthread) を使える。 しかし、OCamlのランタイム内で同時に走るネイティブスレッドは1本だけ、という制限がある。OCamlはスレッドセーフなGCを備えていないためだ。 スレッドはプログラムを構造化して書くために使うツールと割り切ろう、ということらしい。 OCamlの(シングルスレッドの)高いパフォーマンスの代償だろうか。 いずれコンカレントGCはサポートされるだろうと期待するけれど*1、待ってられないので現在の話を考えよう。 動機 ： スレッドのコンテキストスイッチの頻度 OCamlで書いたバイナリとCやJavaを協調動作させるとき、この1スレッド制限がどう効いてくるのかすこし気になっている．たとえば 1つのスレッドが OCaml側で走っているときに C to OCaml のコー
Coqで分離論理(separation logic) - keigoiの日記
分離論理は、ヒープ領域に関する論理結合子をもつ論理体系だ。ホーア論理の拡張であり、ヒープを使うプログラムの仕様を書いたり検証したりといったことに使える。 具体的には、 A ∧ B (AかつB) によく似た、 A ** B という論理結合子が追加されている。これは Aで言及しているポインタと、 Bで言及しているポインタが指しているヒープ領域が、分離されている(≒エイリアシングがない)ことをいっている。 Affeldtさんが、Coqで分離論理を書いて、しかもそれを公開してくださっている。 http://staff.aist.go.jp/reynald.affeldt/seplog/ C言語で書かれたOSのヒープマネージャや、SmartMIPSのアセンブラで書かれた暗号プリミティブの検証をCoqでやっている。 こういったことを自分でも触れるようになりたいので、ICFEM2006のソースを写経して
OCaml toplevel on Android : マジカルなラクダをAndroidで飼おう - keigoiの日記
Androidで動作するOCamlインタプリタ OCaml toplevel on Android を Android Market に公開しました。 OCamlのトップレベル(インタプリタ)をAndroid上で操作できます。 enjoy! 仕組み OCamlトップレベルはネイティブ実行されます(OCamlバイトコード+libcamlrun.a)が、AndroidのアプリはJava VM(dalvikvm)上で動作するため、両者のブリッジが必要でした。 いくつかの方法があり、一部は先日書きましたが、今回の OCaml toplevel on Androidはこのなかのどれでもない、最もイージーな方法を使っています…。 それは 「あるスレッドでocamlトップレベルをバイトコード実行し、標準入出力を介してAndroidアプリのメインスレッドと通信する」という方法です。 stdoutを入力とし
OCamlベースのAndroidアプリに向けて - keigoiの日記
O'Caml on Android というパッチを作っている． 柔軟かつ信頼性の高いOCamlでAndroidのアプリを書くのが目標だ． ここ2ヶ月ほどocamljs (OCamlからJavaScriptへのコンパイラ) を使っていて、OCamlの信頼感と柔軟性にとても満足したので，ではAndroidでもOCamlだ、とばかりに開発を再開している． iPhoneやiPadのObjective-Cと違い，AndroidではJavaの型の扱いやJVMとの相互作用が必要でありなかなか厄介だ． しかしiPhoneではいくつかの開発 事例もあるのでAndroidでもそれなりに有効ではないかと信じている．がんばりたい． OCamlを使う利点 もはや自分の中では言い古した感があるのだけど，念のため列挙してみる． 信頼性 OCamlには null値がない．このため NullPointerException
ビットとview pattern - keigoiの日記
小ネタ。 ビットパターンをHaskellでパターンマッチできたらいいよね、ということでview patternを使ってみた。 {-# LANGUAGE ViewPatterns #-} import Data.Bits -- | ビット。 I は 1, O は 0 data B = I | O deriving Show -- | 8ビット。 左がMSB, 右がLSB data Byte = B B B B B B B B B deriving Show bool2b :: Bool -> B bool2b True = I; bool2b False = O bit' :: Bits a => Int -> a -> B bit' i b = bool2b $ testBit b i -- | view patternで使う関数 bit8 :: Bits a => a -> Byte b
Haskell厨を6年やってる俺がOCamlを仕事で2ヶ月使ってみた - keigoiの日記
Haskell Advent Calendar jp 2010のためのエントリです（17日目）． 6日目の id:camlspotterさんの 経験15年のOCaml ユーザーが Haskell を仕事で半年使ってみた に対するカウンター（になってるかどうか分からないですが）みたいな感じです． 近くて遠い隣人：HaskellとOCaml OCamlはHaskellと違って副作用があり，更にHM型推論をもつためプログラマは本質的な部分の記述に注力しつつ，コードのチューニングもできる． つまり働くHaskellプログラマがシリアスなソフトウェアを書く時に使えるほとんど唯一の選択肢だ．しかし，同じ静的型付けの関数型言語でありながら，OCamlとHaskellの見た目はかなり異なる． この記事では， HaskellプログラマがOCamlを使い始めると，どういうトラップにハマるかを書く． なかでも，
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
