coqdocを使った

coqdocを初めて使ってみました。

はじめは company-coq のスタイルに合わせて見出しとか書いてましたが、なんとなく気が向いたので公式(documenting-coq-files-with-coqdoc )の方を確認してみたのでした。

目的はcoqスクリプトの(主にコメントの)整形スタイルを妥当なモノに統一することなので出力はどうでもいいんですが、…デフォルトはあまりかっこよくないですね :p

今のところ単一ファイルなのでコマンドは:

$ coqdoc --utf8 hoge.v

これだけ。

静的コード解析の会#9

(会場と日程を変更しました) #静的コード解析の会 第9回 - connpass に行ってきました。今回も何らかの発表は出来ず。
どこかで宣伝したらしく、前回から人数が大幅に増えて14~5人くらいの参加者でした。

参加者の傾向としては:

  • なぜかIsabelle使いが多い。
  • モデル検査勢が(人数的に)優勢。
  • 他は各々の好みでいろいろ。

といった感じでした。

RustでマルチスレッドWebサーバを作る例を写経

Final Project: Building a Multithreaded Web Server - The Rust Programming Languageを写経した。
標準ライブラリのみを使って簡単なマルチスレッドWebサーバを書く例。
スレッドプールを作ってacceptするたびに「htmlを応答する関数」をJobとしてチャンネルで配る。

最終的にちゃんと各Workerスレッドを終了させるところまで作る。

思ったよりかなり簡単に書けてしまった印象。設計がいいからだろうか?

ブログ引っ越し完了

滑り込みではてなダイアリーから引っ越し完了しました。
移行が簡単に出来るのは素晴らしいですね。

デザインはこれから横幅がいっぱいに使えるヤツをゆっくり探します。

歯が痛くて倒れていた

8月中旬頃、突然奥歯(の中の神経)に激痛が起こりました(結局明確な原因は不明)。
2週間くらいしてようやく普通の生活が出来るようになりました。あまりに酷い状態だったので書き留めておきます。


どんな状態だったかというと:

  • 常に痛い。何もして無くても神経が痛い。でも痛くてじっとしてもいられないので家の中を徘徊し続けた。ただし歩いても痛い。詰みじゃん。
  • 食べられない。4日間くらいお茶とポカリだけで生きていた。痛い以外の感情がないからか空腹感全くは感じない。今にして思うとちょっとやばいな。
  • 痛み止めが効いている間は大体普通の生活が出来る。ただし効果は4〜5時間で切れ、かつ1日3錠までなので、任意の9時間(24 - (5 * 3))はのたうち回ることが確定。朝4時から5時間くらいうろうろし続けるのは心折れそうだった。
  • 寝られない。痛いと寝られないんですね。初めて知りました。心配しなくても起きる方も痛み止めが切れる時刻にちゃんと起きます。人体って凄いね(^q^)。


他:
症状が出たのがコミケ直後だったので、会社でコミケで調子のってぶっ倒れたヤツみたいな扱いだったのが悲しかった。
原因はよく分からないから無関係という主張も出来ないんだけど…。

terraformのチュートリアルを読んだ

terraformのチュートリアルを一通り読んで実行した。

  • チュートリアルを実行するのに必要な知識が全てチュートリアル内にあり、かなり分かりよい
  • ほぼ写経で動く(1度AWSのよく分からないエラーが出たけど)
  • 記述が古い箇所がある(動きはする)
  • その時点でのconfiguration全体に自信が持てないことがある(remote backends(最後の節)は特に)

terraformの感想

便利そう。途中でエラーが出ても(何かを修正してやり直せば)設定通りの状態にしてくれる(はずな)ので安心感がある。

静的コード解析の会#6で発表してきた

静的コード解析の会#6VeriFastによる停止性検査について発表してきました。(資料作って徹夜してしまった…)



前回も同じテーマでしたが私の理解も資料も十分でなかったため(α)としてました。
が、今回の発表では多重集合、整礎関係、実際の処理系で検査できるコードについての説明まで入れることが出来たので、これで一通りの内容を盛り込めたと思います(ただしシーケンシャルなプログラムに限る…)。
参照している論文はModular termination verificationです。


(多分)怪しげな記述や展開のよく分からないページがありますが、がんばって作ったので興味がある人は是非眺めてみて下さい。
個人的なおすすめはStatic Recursionパターンの検証方法のあたり(資料の末尾の方)です。


会場からは、

  • 処理系が(もっと)がんばれ
  • 発表の構成が悪い(直接そうは言われてないけど)

という感じの反応が得られました…orz。

感想

これまで何度かVeriFastに関する発表をしてるし、(呑みながら)議論もしてきたので聴衆の理解度が高くて非常に楽しい発表になりました。ありがとうございました。

また、懇親会でマルチスレッドの扱いについて質問がありました。通常の(部分正当性の)検査では問題無くスレッドが扱えますが、停止性検査については全く把握できていないので基本的なアイディアだけでも押さえておきたいと思っています。
参照した論文のTR版にマルチスレッドに関する議論があるようです。