2011-01-01から1年間の記事一覧
概要 Javaプログラムに専用の記法で満たすべき条件を形式的に記述し、それをCoqの問題に変換して手動で証明する。この記事はCompetitive Programming Advent Calendar 2011およびTheorem Proving Advent Calendar 2011の12日目の担当記事である。 用意するも…
目的 これに続く記事において、Krakatoa+Why3で証明を行うため。 想定環境 Ubuntu 11.10 (oneiric ocelot) なお、筆者の環境はamd64。 関連パッケージの準備 余計なのも書いてるかも。 $ sudo apt-get install build-essential devscripts dh-ocaml ocaml-no…
07/20 荷物整理 パソコン…一台あれば十分だが、二台持っていった。 衣服…下着は毎日替える。他は適度に使い回し。 書籍…「計算困難問題に対するアルゴリズム理論」を暇つぶし用に。また、競技中は紙の辞書を使用できるので、念のため持参した。(ただし、普通…
2011年7月22日から29日にかけて、IOI2011 (詳細は後述) がタイで開催されます。 以下の4名が日本代表として参加します。 村井 翔悟 (開成) 原 将己 (筑駒) ←自分です 今西 健介 (八千代松陰) 城下 慎也 (灘) 以下では、IOIに関してひと通り説明したあと、今…
IOI概要 国際情報オリンピックは、問題を効率よく解くアルゴリズムに対する洞察力を競うためのプログラミングコンテストであり、数学・生物・化学・物理と並ぶ国際科学オリンピックの一つであると同時に、数あるプログラミングコンテストのうちの1つでもあり…
まえがき 僕のいる地域は東京の隣にある多摩ニュータウンという地域で、地震の被害については交通機関のマヒ以外は無事でした。震災にあっている人のために出来ることは限られているので、はてな経由で200ポイントだけ寄付したのち、元の生活に戻ろうという…
Wikipediaにはすごい数の○○言語版があります。 Wikipedia:全言語版の統計 - Wikipediaによると現在279言語ですって！その中でも目を引くものがいくつかあったので紹介します。 エスペラント http://eo.wikipedia.org/ http://eo.wikipedia.org/:image:small …
こんにちは。今回は誰得感の否めないSELinuxエントリです。しかも独学なのでかなり眉唾物です。SELinuxのポリシーをスクラッチで書くのが目的です。既存のポリシーを運用する話ではないです。環境はDebian squeezeです。 SELinuxとは SELinuxは、Linuxにおい…
ネタを思いついたので実装してみました。As priority_queue broken, we tried implementing Dijkstra using RMQ. — Gistオーダーは変わりません。既にRMQの実装が手元にあるのであれば、こっちの実装方法のほうが楽ということもあるかもしれないとだけ言って…
情報オリンピックに参加した皆さんこんにちは。僕はqnighyです。一応すごい人です。予選で終わってしまった人も、本選で終わってしまった人も、これから合宿に行けるという人もいると思いますが、これ以降も競技プログラミングに精進したい！という人のため…
20+20+20+6+20japljの呪詛によって4番がエンバグしました。詳細はあとで調べます。
出来事 学校でゼミをやってから代々木に直接行った。 いつもの面子との再会と、きゅうりperyaudo組との遭遇。 Practiceはほとんどやらずにずっと駄弁っていた ちなみに今回はVimではなくEmacsを使うことにした 名刺はPractice中に配りまくった。しかし、40枚…
バレンタインチョコ欲しい！ 欲しいプレゼントは… BPS バトルプログラマーシラセ ( DVD2枚組 )出版社/メーカー: スターチャイルド発売日: 2004/03/24メディア: DVD購入: 3人 クリック: 157回この商品を含むブログ (25件) を見る 他の人からのプレゼントもお…
Java バージョンを調べるAPI。 public void printVersion() { System.out.println(System.getProperty("java.version")); } 上記を実行して調べた結果、1.5.0_08でした。 JavaÌo[WðvOÅmF·é(Java}X^[) C++ プリプロセッサマクロで…
大量の入出力データを扱う課題を解く際に，入出力の処理に cin, cout ストリームを使用した C++ プログ ラムは scanf, printf 関数を使用した同等のプログラムに比べてとても遅くなることに注意してほしい．よっ て，cin / cout ストリームを使用しているの…
MacBook Air 11インチ別に要らない！
