【デブサミ2020】セッションレポート：13-F-6 「厳密な共通言語」としての形式手法

形式手法なんもわからん

登壇：チェシャ猫さん

形式手法というものを聞いたことはある。でも、なんもわからん。
概念として、自分の考え方とあってそうな気がする。でも、なんもわからん。

このセッションを通して「完全に理解した」になれるだろうか。

システムの仕様と曖昧性

チェスのルール：ポーンは最前列に到達した際クイーン・ビショップ・ルーク・ナイトのいずれかになることができる
ここには穴がある。「同じ色」の制限と「なることができる」という曖昧さ。

 Max(x, y)も、正しくは「小さくないほうを返す」

その分野の人には自明であることが文書化されない

仕様を理解した「つもり」の思い込み
最初に思いついたものからはなかなか脱却できない

TCCパターン
・Tryフェイズ
・Confirm/Cancelフェイズ
　・全員がOKならConfirm
　・そうでないならCancel
このTCCにも曖昧な部分がある
保証したい仕様はなにか？アルゴリズム外の環境との相互作用は?

イメージの限界による曖昧性の発生

どんなに小さいパーツの中にも曖昧さがあるということがよくわかる。
そして、ということは大きなシステムが内包する曖昧さたるや、である。

こういった曖昧さはテストで拾うことが期待されやすい
しかし、テストを実施するより前に複雑さを扱いうる「言葉」が必要だ

形式手法とツールの概要

形式手法

数学的に表現できる方法論
実装がなくとも仕様や設計の段階で検証できる
厳密な記述を強制し「イメージの外」の余地を残さない

モデル検査

システムがとりうる状態を列挙して探索する
有限個を対象とし、自動化できる

定理証明

数学的な証明をプログラムとして表現する
無限個を対象とできる

TLA＋

モデル検査系のツール
採用事例　AWS DynamoDB, S3など

LampLighterの例

PlusCalによる生成
生のTLA+を書くのは人間には辛い
このツールならコードっぽく書ける
組織への導入コストも下がる

モデリングを通した仕様の明確化

コンポーネントごとに記述し、合成はTLA+に任せる

条件分岐の記述

\A \E など、記述が数学的

保証したい仕様の意味
・トランザクションとしての一貫性
・一連の手続きが完了する保証

安全性と活性

Safety 何か悪いことが「おこらない」ことを要求
Liveness 何か良いことが「おこる」ことを要求

時相論理(Temporal Logic)

[]A:  現時点以降常にAが成り立つ
<>A: 現時点以降いつかはAが成り立つ

この時相論理を使って、「一連の振る舞い」が検査可能とのこと。
曖昧性をなくすために有効な手法だ、というのがわかってきた。途中まで「ここまで書くならもうコードでいいじゃん」という気持ちがあったが、振る舞いについての検査はとても難しい。そこを表現できる形式手法、強力なのでは。

環境と相互作用する複雑な挙動の解析

テストでエラーになってくれることで、考慮できていない・間違って認識していた前提を発見できる
こういう実行フローを頭の中で構築することは難しい。
TLA+は異常系を予め記述し、全探索で仕様にあわない記述を発見してくれる

まとめ

「まさかそんな手があったとは」が曖昧性
自然言語で表現すると、どうしても曖昧さは織り込まれる
形式手法で数学的に記述すると、厳密に表現できる
より複雑な状況における解析を自動化できる

異常系を網羅することは、確かに難しい。本番で予期せぬ組み合わせからインシデントが発生することはあるし、そこへの対策としてはアジリティを上げレジリエンスを向上させることくらいだった。しかし、形式手法による検査を用いると、今よりも予期せぬ事象の事前検知ができるのでは?という期待感をもった。

形式言語、完全に理解した