モデル検査器をつくる〜Goで実装して学ぶ形式手法〜：Dodgson Labs

ただツールを使うだけの形式手法から、君の手でつくる形式手法へ。Go 言語でモデル検査器を実装しながら学ぼう！ 形式手法 (formal methods) は計算機システムを何らかの数学的な対象によって記述し、その性質について理論的な保証を得る手法の総称である。通常、プログラムの開発時に行われる単体テストと比較すると記述コストは高くなるが、その代わりに保証できる内容は数学的な裏付けに基づいており、テストケースの抜けや漏れが発生しない。そのため、分散システムなどの複雑な挙動の設計や、医療・航空宇宙など極めて高い信頼性が求められる場合に威力を発揮する手法である。形式手法には大きく分けて定理証明 (theorem proving) とモデル検査 (model checking) があるが、書名が示す通り、本書ではモデル検査を扱う。 他に類を見ない本書の特徴として、Go言語を用いて実際に読者自身の手