VSTTE 2012 Software Verification Competition というソフトウェア検証のコンペがあった。参加はオープンで、問題文もPDFで配布されている。 id:yoshihiro503 がチームtebasakiというチームでがんばっていた。僕はCoqに慣れていなかったのでチームに入るの…

分離論理は、ヒープ領域に関する論理結合子をもつ論理体系だ。ホーア論理の拡張であり、ヒープを使うプログラムの仕様を書いたり検証したりといったことに使える。 具体的には、 A ∧ B (AかつB) によく似た、 A ** B という論理結合子が追加されている。これ…

第三回ProofCafeが開催されました。CPDTの Inductive Types の前半を読みました。個人的には injective タクティックを使ったことがなかったので次から積極的に使おうと思いました。

ProofCafe の第二回が名古屋・栄の「どえりゃあ」で開催されました。 前回の記事はこちら 私は今回は出席できず。残念です。 資料とか http://coq.g.hatena.ne.jp/yoshihiro503/20100517/p1 より転載。 資料(HTML): http://adam.chlipala.net/cpdt/html/toc.…

名古屋・栄のお洒落レストラン「どえりゃあ」で、第一回 ProofCafe が開催されました。 ProofCafe は、コンピュータプログラムの安全性に関する定理証明に興味を持つ方々の集いです。 記念すべき 第一回目は Coqという定理証明支援系について id:yoshihiro50…

参考：http://d.hatena.ne.jp/yoshihiro503/20100119#p1証明すげー。 あと、幅優先探索で見つけたパスを無限ストリームで並べているのを見てこれは面白いと思った。枝刈り付きBFSとゴールの発見手続きを独立に書けているのか。なるほど！ ストリームを使った…

無限ストリームの型はCoInductiveという構文で宣言された余帰納的な型である。 無限ストリームはCoFixpointという余帰納的な関数(?)を作る構文で定義する。Fixpointは最小不動点(Coqなら「いつか必ず止まる」)だがCoFixpointは最大不動点(止まらない、無限?)…

fixタクティックについて。 ふつう、Coqの証明モードで構造帰納法を回したい場合は inductionタクティックを使いますが、 fix は、帰納法のためのよりプリミティブなタクティックのようです(項の場合分けをやらない)． This tactic is a primitive tactic to…

下の記事では， Definition dual_dec : forall (u1:sesstyp) (u2:sesstyp), {dual u1 u2}+{~dual u1 u2}. という関数を，Coqの証明モードで作りました．ところが証明モードで作ったプログラムは極めて複雑でイマイチ効率のほどがよくわかりません (Coqで Pri…

すごくどうでもいい証明です．．Coqを触るのは2年ぶりくらいだろうか… めちゃくちゃ非効率なことをやっていそうなので，皆さんのツッコミをお待ちしています． 前提 セッション型の双対とは，受信の双対が送信，送信の双対が受信という感じで決まっています…

ググれば出てきそうな気もしますが、がんばってみました。しかしあえなく轟沈。(証明どころか関数さえ書けない始末…情けない。)Coqではちゃんと停止する関数しか書けないです。これは再帰が書けないという事ではなく、再帰にはDefinitionの代わりにFixpoint…