#技術書典 16 で Go を使って #自作モデル検査器をつくる本を頒布します

こんにちは、チェシャ猫です。

今回、技術書典 16 にて、新刊『モデル検査器をつくる〜Goで実装して学ぶ形式手法〜』を頒布します。

どんな本？

ただツールを使うだけの形式手法から、君の手でつくる形式手法へ。Go 言語でモデル検査器を実装しながら学ぼう！

書名の通り、Go でモデル検査器を実装する本です。Pramo 言語と名づけた本書オリジナルのモデリング言語を定義し、その可視化器と検査器を作成します。

Pramo 言語は、ある種のマルチスレッドをサポートするプログラミング言語であり、Go の埋め込み DSL として記述されます。例えば有名な「食事する哲学者」は以下のように実装されます。

func badPhilosopher(name procName,
    right, left lockName, hold varName) process {

    return Process(name,
        For(
            Case(Lock(left),
                Assign(hold, Add(Var(hold), Int(1))),
            ),
            Case(Lock(right),
                Assign(hold, Add(Var(hold), Int(1))),
            ),
            Case(When(Eq(Var(hold), Int(2))),
                // eating
                Assign(hold, Int(0)),
                Unlock(left),
                Unlock(right),
            ),
        ),
    )
}

よく知られている通り、哲学者が二人以上いる場合、お互いに相手が持っているフォークが空くのを待ち続けることでデッドロックが発生します。そこで、デッドロックが発生するのはどのような状況か、あるいはどう変更したら回避できるのか、といった問題について、プログラムを実際に実行するのではなく、生じうるすべてのタイミングの可能性に対して網羅的にチェックすることを考えます。これがモデル検査であり、本書であなたが実装する Pramo 言語です。

ちなみに、これは本の中には書いていないのですが、Pramo 言語の元ネタになっているのはモデル検査器 SPIN で使用される Promela 言語です。Promela 言語は Dijkstra による Guarded Command がベースとなっており、本書の Pramo 言語も同様ですが、Pramo は Promela の機能をいくつか落として簡略化し、その代わりに Go の DSL として自由度が高い記述できるようにしました。

各章の概要は以下の通りです。まず第一章では、Pramo 言語の構文と意味論を定義します。次の第二章では、モデル検査に使用される Kripke モデルの概念を紹介した上で、Pramo 言語の記述から Kripke モデルへの変換を行い、いくつかの仕様の検査を実際に試してみます。最後に第三章では、よりモデル検査らしい話題として、CTL（Computational Tree Logic、計算木論理）による仕様記述とその検査アルゴリズムを取り上げます。いずれも、実装する過程で動作する完全なソースコードを掲載しています。

読んでみて、もし面白かったとか参考になったなどポジティブな感想を持っていただいた方は、是非 X（旧 Twitter）でハッシュタグ #自作モデル検査器 をつけて投稿してくださると幸いです。形式手法とモデル検査、盛り上げていきましょう！

値段は？

「電子版のみ」もしくは「電子版 + 紙版セット」の二つのコースがあります。「紙版のみ」は技術書典のレギュレーション上ありませんのでご注意ください。特に、電子版を入手しようとして両方ダブって買うことがないように注意しましょう。電子版は常についてきます。

電子版のみ：1,000 円
電子版 + 紙版セット：1,200 円

どこに行けば買える？

オフライン会場での直販と、オンライン会場での通販があります。

オフライン会場

オフラインイベントは以下の通りに開催されます。

日時：2024 年 5 月 26 日（日）11:00〜 17:00
場所：池袋サンシャインシティ展示ホールD（文化会館ビル 2 F）
サークル配置：あ08（入り口すぐ、右手側）

techbookfest.org

入場は無料ですが、事前に入場整理券の発行が必要です。整理券は時間帯ごとに発行されており、25 日現在 12:00 までの枠は売り切れていますが、13:00 以降はまだ残りがあるようです。

また、会計には技術書典公式の「かんたん後払いアプリ」が必要です。現金の取り扱いはありませんのでご注意ください。

#技術書典にはQRコードを読み込んで本を購入できる「かんたん後払い」という公式アプリがあります。開催直前になると混み合ってSMS認証にかなり時間がかかります。ぜひ来場前にご準備ください。

📕iOS版📕https://t.co/hfujubSEPa
📗Android版📗https://t.co/tUzhfJIDlW
— 技術書典公式アカウント (@techbookfest) 2024年5月21日

オンライン会場

オンラインマーケットは以下の通りに開催されます。

日時：2024 年 5 月 25 日（土）10:00 頃〜 2024 年 6 月 9 日（日）23:59 頃

techbookfest.org

なお、オンラインマーケットでも「電子版のみ」「電子版 + 紙版セット」の両方が購入可能で、価格もオフラインイベント会場と同じです。ただし、オペレーションの都合上、印刷所への発注は会期終了後にまとめて行うため、手元に紙版の本が届くのは 6 月末以降になります。もし少しでも早く紙版が読みたい場合は、オフラインイベントに参加しましょう。

まとめ

以上、技術書典 16 の新刊『モデル検査器をつくる〜Goで実装して学ぶ形式手法〜』の頒布情報でした。読んだら #自作モデル検査器 でよろしく！

チェシャ猫の消滅定理

数学にプログラミング、素敵なもの何もかも。