Skip to content
2017年8月4日 / masterq

コミケ92 金曜日 東た11bでの同人誌に記事を書きました

c92-cover

コミックマーケット92 金曜日 東た11b参照透明な海を守る会というサークルで「簡約!? λカ娘 10」という同人誌が頒布されるらしいのです。その中で2つの記事を書きました。

1つ目は「Coq ダンジョン : 底抜けの壺の夢」という証明できない命題も証明できるCoqのタクティックを作ってしまおうというチョイネタです。CoqはタクティックがズルしてもGallinaの型検査ではじかれるから安心ですね!

2つ目は「静的コード解析はいいぞ!」というソースコードの検証手法の概要紹介です。特にVeriFastという解析ツールを使う意義を初心者にもわかりやすく導入したつもりです。短かい記事ですが。最近はVeriFastのような製品品質を静的な解析によって向上させる手法に個人的に興味があり、「静的コード解析の会」などというイベントを開催していて、次回は2017/09/23(土)に開催される予定です。

僕以外の記事についても(理解できる範囲で)解説してみます。

「モナドとひも」は@myuon_myonさんの記事で、主にモナドを圏論の図式ではない紐を使った図を描くことで理解を促進するこころみの紹介です。僕個人は日頃ヒューリスティックなブロック図を描いてしまいがちなので、形式的な図の描き方には興味がわきました。

「矢澤にこ先輩と一緒にモナドモナド!」は@public_ai000yaさんの記事で、「モナド上のモナド」について解説しています。本記事は圏論の知識が前提とされて個人的にはショック死しました。。。特にモナド合成とモナドモナドとの関連で今混乱しています。。。@public_ai000yaさんはコミケ当日ブースで売り子をしていただけるようなので直接質問するといいかもしれないですね!

「IST(Internal Set Theory) 入門 (後編)」は@dif_engineさんの記事で、超準解析のための内的集合論の入門記事の後編です。この記事の前編は「簡約!? λカ娘 9」に掲載されています。いきなり後編から読むのは辛いので、9巻も一緒に買うといいですね!9巻では無限に小さい数について考え、述語論理の導入から初学者を高階な数学の世界に持ち上げてくれます。僕も読み直さねば。。。

「VeriFastチュートリアル」は@eldeshさんの翻訳記事で、原文はこちらです。僕も少しだけ翻訳手伝いました。またこの翻訳はオンラインから全文を読むこともできます。VeriFastは先にも紹介した静的コード解析のツールの1つで、C言語やJavaコード中のコメントに特殊な注釈を設計者が書くことで、関数の事前条件/事後条件やポインタの安全な使用などをコードの実行時ではなく静的な検査によって網羅的に検証してくれます。Coverityなどの静的コード解析ツールと異なり、左記の注釈を人力でコードに追記する必要がありますが、(ある条件下では)エラーの見逃しや誤検出が起きないのが良い点だと思います。この正確な検証はVeriFastが分離論理という理論基盤の上に構築されていることに由来しています。

上記同人誌の一部のページは立ち読みできるので、気になったら是非サークルブースにおこしいただけたら幸福です。

広告

コメントを残す

以下に詳細を記入するか、アイコンをクリックしてログインしてください。

WordPress.com ロゴ

WordPress.com アカウントを使ってコメントしています。 ログアウト / 変更 )

Twitter 画像

Twitter アカウントを使ってコメントしています。 ログアウト / 変更 )

Facebook の写真

Facebook アカウントを使ってコメントしています。 ログアウト / 変更 )

Google+ フォト

Google+ アカウントを使ってコメントしています。 ログアウト / 変更 )

%s と連携中

%d人のブロガーが「いいね」をつけました。