VSTTE Competition参加記録

id:yoshihiro503さんに誘われて、VSTTE Competitionというソフトウェア検証コンテストに参加しました。
「検証ツールに特に制限はないぜ」と書かれていたのでCoqを使いました。

競技プログラミンングに初めて参加しましたが、48時間ぶっとうしで同じ課題に取り組むのはとてもエキサイティングで楽しかったです。

参加メンバー

一日目

開始直前
  • yoshihiro503さんから"uiro,tebasaki,miso,..."と列挙された謎のメールが届く。 どうやらチーム名の候補だったらしいです。
  • yoshihiro503さんとSkypeで話しながらbitbucketの準備をしたりする。
  • 0:00からの開催に備えて仮眠をとる。
0:00ごろ
  • 問題が公開される。 https://sites.google.com/site/vstte2012/compet/problems
  • ざっと見た感じだとProblem2,Problem4,Problem5が関数型ぽっかったので、Problem2をボクが、Problem4をpirapiraさん、Problem5をyoshihro503さんが担当することにする。
  • 簡単かと思ったProblem2をよく読むと「停止性のない関数を定義しろ」と書いてあって、散々苦しむ。
3:00ごろ
  • なんとかProblem2の形式化をするも、証明がうまくいかないので諦める。
  • 「もう寝るー」とSkypeでつぶやくも、興奮しまくっててうまく寝れない。
  • しょうがないので、Problem3にとりかかる。
5:00ごろ
  • 新聞配達の人が来て、時間の進む速度にびびる。
  • なんとかProblem3の疑似コードをCoqに変更することができたので、さすがに寝る。

二日目

9:00ごろ
  • 起床。Problem3の続きにとりかかる。
  • 「FIFOであることを示せ」と言われて頭をかかえる。
  • Skypeで@keigoiさんに相談して「FIFOの公理を定義して、それを満すことを示せばいいんじゃね?」というアイデアをもらう。
13:00ごろ
  • Problem3がだいたい解ける。あとは細かい補題を示すだけ。
  • 五十嵐先生の講義を聞くために大学への移動する。
16:00ごろ
19:00ごろ
  • 問題にある疑似コードをそのままCoqに落すのは無理だね、という結論に至る。
  • 眠気が限界なのでラーメンを食べて帰宅。
  • ちょっと休憩してProblem1に取りかかる。
  • 疑似コードをそのまま扱うのは諦めているので、ループ+破壊的代入の疑似コードを再帰に書き直してCoqで定義する。
22:00ごろ
  • 翌日に備えて、早めに就寝。

三日目

8:00ごろ
  • 起床。Problem1の続きを始める。
  • 関数をCoqっぽくしてるので、特に問題なく進む。
13:00ごろ
  • Problem1証明終了。
  • メールチェックをするとpirapiraさんがProblem4をhirose_golfさんがProblem2を解き終わっていた。このひとたちすごい。
  • 残っているProblem5にとりかかる。
18:00ごろ
  • 何もすすまないまま夕方になる。
  • partake.in のために名駅に移動する。
20:00ごろ
  • [twitter:@bleis]さんと[twitter:@maeda_]さん、[twitter:@wof_moriguchi]さんとご飯と食べる。
  • 「お前のやっているのは競技証明であって、競技プログラミングではない」との中傷を受ける。 必死になってカリーハワード対応について説明したけど、理解してもらえなかった。
22:00ごろ
  • 帰宅。 Problem5を解くのを完全にあきらめる。
  • yoshihiro503さんと現状を確認して、投稿の準備を始める。
23:00
  • tarballを作ったりビルドスクリプトを書いたりして投稿。

感想

  • めちゃくちゃ楽しかった。次もぜひやりたい。
  • 他のメンバーの証明能力がハンパなくてびびる。
  • 夜って意外と短かい。