2020年1月に入社し、SWETの仕様分析サポートチームに加わったtakasek（@takasek）です。
仕様分析サポートチームでは、社内のプロダクト開発に対する形式手法の活用可能性を模索しています。当ブログでも、継続的に形式手法に関する情報発信をしています（形式手法 カテゴリーの記事一覧）。
この記事では、加入3か月を経てようやく形式手法の輪郭が掴めてきた私の視点から、学習前後での理解の変化について振り返ります。想定読者として学習前の私と近い属性——すなわちコンピュータサイエンスや数学の専門教育を受けておらず、主に現場での実務と自習に頼ってきたソフトウェアエンジニアを想定しています。
形式手法を学ぶ前の認識と疑問
ソフトウェアエンジニアとしての私の一番の興味関心は設計手法です。設計は、なんらかの解決したい問題に対して、ある一面を切り取った構造（モデル）を与え、そのモデルを解決の機構に落とし込む行為といえます。 その興味の延長線上で、よりアカデミックな裏付けのあるアプローチが取れると聞いて興味を持って形式手法を学び始めた私ですが、形式手法の概要を知った段階での認識・疑問は次のようなものでした。
そもそも「形式」「形式手法」の正体が掴めていない
形式手法というのはテストよりも抽象的に、網羅的に問題を発見できるらしい。
なるほど、たしかにテストの7原則によれば「テストは欠陥があることは示せるが、欠陥がないことは示せない」。その弱点をカバーできるとしたら形式手法はすごい。ただ理屈がよくわからない。書かれていないものは書かれていないのだから見つけようがないのでは？
形式手法は数理論理学に基づいているという説明もある。わからない。普段のプログラムだってif文を書くぞ。何が違うんだ。形式化されているのが違う？ なるほど……なるほど？ そもそも形式化って何だ？ プログラムのコードは機械が読むためのものだが、それは形式化じゃないのか？ やっぱりわからない。普通のプログラミングと形式手法を隔てるものは何なんだ？
形式手法の分野の違いがわからず混乱する
形式手法の分野には主に「形式仕様記述」「モデル検査」「形式検証（定理証明）」があるらしい。
しかし字面から違いがよくわからない。形式仕様記述は記述するだけで検査や検証をしないのか？ 仕様とモデルの違いは？ 検査と証明・検証の違いは？ 混乱する。しかも各分野の中にもツールがたくさんあるようだ。なんでそんなにたくさんあるんだ。統一してほしい。
数学をちゃんと学ぶ必要があるらしいが、本当か？
そりゃ何事も学ぶほうがいいのはわかる。たとえば仕様記述テクニック「Promotion」の紹介 - DeNA Testing Blogには以下のような記述が登場する。
存在量化子というやつだ。なるほど。こういう概念が登場したときに数式が理解できないとたしかに困りそうだ。でも、そういうテクニックだけをピンポイントに使う形でカバーできないのだろうか？
これまで触れてきたプログラム言語の型付けでも、存在型（existential）や全称型（generics）が登場する。基礎から理論を理解できるならもちろん良いが、とりあえず表面だけでもなんとかごまかしごまかし使うことができている。
形式手法も実はごまかしでいける部分が存在するのでは？ 要求レベルを上げていったらきりがないじゃないか。「学ばないと太刀打ちできない」というような言い回しは不当にハードルを上げているだけでは？ それとも形式手法の場合には決定的に「数学を学ばないと太刀打ちできない」ような事情があるのだろうか？
実際どこまで役に立つのだろうか
正直、知的好奇心に駆られて転職しちゃったところがあり、実際にプロダクト開発の現場で汎用的に適用できるイメージは具体的に湧いていない。
「形式手法の実践ポータル」に事例がまとめられているが、大層なプロジェクトばかりだ。現状、普通の開発現場で形式手法が流行っている様子はない。ということは、適用範囲がけっこう限られるのでは？ どれくらい汎用性のある技術なんだろうか？
今の理解
このような疑問を持ちながら3か月の学習と実践を重ねていった結果、現在は以下のような理解に辿り着きました。
「形式」は証明のためのスタートライン
私の当初の「プログラムのコードだって形式化されているのでは？」という疑問は正解です。普段プログラマが使うプログラム言語は形式言語です。利用可能な文字集合、文法のルールが規定されており、曖昧な構文を許さない言語です。
形式手法と普段のプログラムと違う点は数理論理学に基づく点だと言われます。だから網羅性があり、テストでは発見できないような欠陥も発見できる。……よくわかりませんね。何が違うのでしょうか。
実は誰でも同様のアイデアを昔習ったことがあるはずです。私も中学数学の復習をしたら分かりました。証明です。
三平方の定理を考えてみましょう。a,bの二辺と長さcの斜辺からなる直角三角形においてa2+b2=c2が成り立つという定理です。
この結果を確認したいとき、プログラマが慣れているユニットテストでは具体的なケースを列挙するしかありません。 {a:3, b:4, c:5} のとき成り立つ、 {a:5, b:12, c:13} のとき成り立つ……といったように。Property Based Testingであれば大量のランダムな入力を与えることも可能ですが、どこまでいっても有限個の試行の繰り返しです。
しかし証明なら、個別のケースではなく任意の無限の直角三角形について定理が成り立つことを示せます。中学数学の証明では、直角三角形の図に補助線を引くなどの作業を通じて、すでに明らかな定義を変形させて定理を導きました。
中高の数学の範囲を離れると、次のように言えます。無条件に正しいと見なせる命題を公理といいます。公理に繰り返し推論規則を適用していくと定理を導出できます。その論理の筋道をつけるのが証明です。
形式手法の話に戻ります。形式手法とは「このシステムは正しい」と言えるようにするための手法です1。言い換えると、命題「このシステムは正しい」を証明するのが形式手法のゴールです。そして数学的な意味で証明可能にするためには、漠然とした「正しい」を数理論理学の世界に持ち込まなくてはなりません。
自然言語で書かれたシステムの仕様には曖昧さがあり、機械的な推論規則の適用もできません。それでは証明などできません。形式言語を使って論理式として仕様を表現することが、形式手法のスタートラインです。
形式手法の分野は多岐にわたり、また横断的である
システムの正しさを証明するのが形式手法のゴールだと述べました。形式手法の分野の違いは、その筋道のつけかたの違いです。
形式手法の多くは次のような二側面を持ちます。
- システムのある性質を表現する仕様を形式的に記述し、
- なんらかのツールを通じて検査・検証にかけ、結果を出力する
この前者および後者のバリエーションがさまざまな形式手法の違いです。
まず対象のシステムとは何かを考えてみましょう。システムと一言で言っても、入力と出力が1対1で対応するシステムと、異常がない限り動き続けてイベントを待ち受けるシステムは別物です。複雑な内部状態と条件分岐を持つゲームも、独立動作し協調しあう分散システムも「システム」です。
システムの中でも、検証すべき性質はひとつではありません。性質に応じて出力の形は変わります。
- 仕様を詳細な設計に落としたとき、不正な挙動が混入していないことを確認したい
- システムを構成する複数のコンポーネントの関係について、可能なパターンをグラフィカルに図示したい
- 具体的なシナリオに沿って、状態遷移をシミュレーションしたい
- 並行システムの挙動を合成して、不具合が起こりうるケースを網羅的に検知したい
- 複雑な証明の途中式を自動的に補完しながら巨大な証明を完成させたい
こういった異なる目的を、同一の手法・ツールでは達成できません。
形式化のベースとなる論理体系も一様ではありません。たとえばアルゴリズムが仕様を満たしていることを検証したければ、その事前条件・事後条件をHoare論理を使って記述します。システムの長いライフサイクルにおける性質を検査したいときには「いずれtrueになることがある」「常にtrueのまま」といった時相論理を使った表現を使うこともできます。他にも検証したい性質に応じて、門外漢には想像もつかないほど多様な論理体系が存在するようです。
ただし強力な表現ができるほどよいというわけではありません。必要十分な表現力があればよいのです。記述の自由度と解析の簡単さはトレードオフです。無用に記述が複雑すぎると理解しづらくなり、仕様記述に矛盾や不整合がないことの検証（verification）のみならず「その仕様は本当に問題の解決の形として妥当か」の確認（validation）に支障が出ます。またシステムの全状態をモデルとして表現して網羅探索するモデル検査では、詳細すぎるモデルは状態爆発により現実的な時間内での検査が難しくなります。重要なのは適切な抽象度での仕様記述・モデリングです。時には表現力を制限し簡単な記述を可能にしたDSL（ドメイン特化言語）が有効な解決策になります。
ソフトウェア工学の道具としての形式手法では、形式手法とは何かという問いに、次のような説明で答えています。
数理論理学に基づく言語ならびに証明技法などからなる基礎理論を持つことに加えて、設計手法、ドメイン知識、などが関係する総合的な技術2
形式手法と一言で言おうとしても輪郭が掴みづらいのは、そういった総合的な側面が影響しているのでしょう。
先述したとおり形式手法には「形式仕様記述」「モデル検査」「形式検証」があると言われますが、3つの分野を排他的なものとして考えると混乱します。モデル検査であろうと形式検証であろうと仕様記述は必要です。たとえば代表的な形式検証のツール（定理証明系）であるCoqの記述言語Gallinaも、明確に「仕様記述言語」だと説明されています3。
今私たちが取り組んでいるプロジェクトでも、目的までのロードマップには3分野いずれの技術も必要になっており、いくつもの手法を組み合わせて活用しています。何かひとつのツールを触って理解した気になるのではなく、問題に対して適切な抽象度とツールを選ぶために見識を広げていかなければならないと思います。
形式手法にとって数学は基礎的な語彙である
形式手法のツールには、難しい理論を知らずとも扱えるようにデザインされているものもあります。たとえば当ブログのDeNA TechCon 2020の発表についての記事で述べたように、仕様分析サポートチームでは当初「視覚的なフィードバックを得られるので初学者に易しい」という理由でAlloyを採用しました。ツール上でフィードバックを得ながら試行錯誤していたらなんかうまいこと目的達成できた、という体験も悪くはないでしょう。
しかし形式手法に正面切って向き合うなら、表層だけ撫でる態度はむしろ効率を損ないます。先に述べたように、あるシステムの仕様を適切に記述し性質を検証・検査可能にするためには、どのみち形式仕様記述を避けて通れません。モデル検査は「ボタン一発の検証法4」とは呼ばれますが、そのモデリングのためには抽象化技術が必要ですし、検査結果を読むにあたっても論理学の理解がないとしばしば誤った解釈をしてしまうそうです。数理論理学は形式手法での読み書きを支える基礎的な語彙となります。
そして論理学は、概念の積み上げで成立しています。注意深く足を進めないとすぐ転んでしまいます。例をいくつかご覧に入れましょう。
述語という単語を耳にしたとき、論理学の素養がない人は「主語でない文節」と理解することが多いでしょう。すると論理学での「変数を含み、変数に具体的な値を代入することによって真偽が定まる叙述5」という理解ができなくなります。
当記事でも何度も言及している性質は、数理論理学の世界では「変数が1つの述語」です。あなたのイメージと合致していたでしょうか？ この理解は普段の日本語やオブジェクト指向に慣れ親しんだプログラマからは距離があります。
ときには普段のプログラミングでの考え方が邪魔をすることすらあります。形式仕様記述にもいくつかのアプローチがありますが、私が現在取り組んでいる仕様記述は状態に注目するモデル規範と呼ばれる方法なので、その話をしましょう。
ここで状態というのは「局所状態の掛け合わせとして立ち現れた、システム全体のグローバルな状態」です。プログラマは普段、グローバルな状態は悪だと考えているものです。なるべく状態を局所に留め、モジュール内の状態は隠蔽するよう、半ば教条主義的に訓練されています。なのでグローバルな状態という存在を受け入れるには、私にとってはかなりの発想の転換が必要でした。
モデル規範の形式仕様記述では、すべての状態の集合から特定の状態を取り上げ、状態どうしの関係を記述することになります。この手順を飲み込むまでにも時間を要しました。普段プログラマは多かれ少なかれパフォーマンスを気にしながらコードを書いています。もし集合（Set）に数万の要素が入ると言われたら、ぎょっとしてアルゴリズムを考え直すことが多いでしょう。グローバルな状態の集合は、天文学的な要素数をものともしません6。そういうものを扱う数学的な発想に、私は最初大きく戸惑いました。
「すべての状態」があらかじめ存在しているという前提を受け入れると、パラダイムが大きく変わります。事前状態・事後状態の関係は pred hoge(s, s') のように記述します7。日頃プログラマとして慣らされているような「事前状態を具体的な引数として受け取り、加工して事後状態を返す」関数ではなく、時間経過を伴わない静的な記述だというのがポイントです8。
このように形式手法を学ぶ中ではしばしば、日常用語と異なっていたり、これまでのプログラミングの延長で捉えられない概念に遭遇します。既存の枠組みに引き寄せて歪んだ理解に辿り着かないよう、注意深くならなければいけません。
定評のある数学の教科書はどれも、まず単純な定義から始め、定義済みの確かなものを積み上げると新たな概念が獲得されるように書かれています。私のような現場でのアドホックな学習で育ってきた人間は、基礎を積み上げていくアカデミックな手続きをおろそかにしがちです。最初から数学やってる人には丁寧な手続きが常識なのかもしれませんが、少なくとも私はそういう足腰が弱ってることを自覚しないとすべてが始まりませんでした。
問題を分割統治するのはプログラミングでも散々やってきたはずだし、場合分けして分割統治、各個撃破というのは中学高校の証明で習ってるはずなのに、大人になると忘れちゃうし身についてないんですよね。不思議ですね。
形式手法は役に立つ！
かつて形式手法は、システムのすべての性質を壮大な論理体系で表現し、厳密な仕様がそのまま動くプログラムへと詳細化される世界（Correctness by Construction）を夢見ていました。しかしそれは壮大すぎて難しく、今世紀に入ってからは実用性を意識する Formal method Light が主流となったそうです9。
プログラマが日常的に頼っている型システムも「型システム入門」によれば「最も確立された軽量形式手法」10です。当初の私の認識「普通の開発現場で形式手法が流行っている様子はない」なんてとんでもない勘違いでした。もう当たり前のように、形式手法はソフトウェアエンジニアリングの世界に溶け込んでいるのでした。
デザイン電卓として
かつてモバイルアプリエンジニアとして携わった案件でも、今と同様の知識があれば形式手法の実践を検討しただろうと思える局面が何度かあります。
私があるとき設計・実装したのは、端末のオンメモリ・サーバ通信・永続化層・さらにアプリバージョンのアップデートといった複数の状態が非同期に絡み合う複雑な機能でした。人数と時間をかけて何度も仕様をチェックし設計しましたが、やはり多くの細かいミスが出ました。テストを書いても「本当にこれですべて確認できるのか」「テスト自体が間違っているのでは」という不安がつきまとい、実際その不安は大いに的中しました。転ばぬ先の杖として不正なデータを差し戻す処理を随所に入れたりもしましたが、本当にそれが必要なガードだったのか、もしくは無用に仕様を複雑にしただけなのかは今でも分かりません。
今の自分が当時に戻ったら、この案件に限って形式仕様記述してモデル検査にかけよう！ と提案することでしょう。モデルが正しく振る舞うことを早期に検査できれば安心して開発を進めることができます。目的を絞ればそこまでの導入コストはかからず、十分ペイするはずです。
このように、大がかりにではなくアドホックな形で形式手法を用いるアプローチは「デザイン電卓」と形容されるそうです11。形式手法に対しての大仰なイメージを払拭してくれる素敵な表現だと思います。
仕様の妥当性確認として
メリットは、ツールによる正当性（correctness）の検査（verification）だけではありません。形式的に仕様記述すること自体が「その仕様は本当に問題の解決の形として妥当か」の確認（validation）となります。
普段のソフトウェア開発業務で仕様書を読み書きするとき、条件の不明瞭さや期待結果の曖昧さ、項目どうしのつながりに不安を覚えることはないでしょうか。私はありました。自然言語の表現力に絶望して、おもむろに擬似コードを書き始めることもありました。頭の中ではなんとなくうまくいきそうなのに、条件の漏れやブレによって適切な仕様化に失敗することはよくあります。そんなとき、形式言語は仕様の妥当性を厳密に確認するための、まさに言語として役立ちます。
先日のDeNA TechConでの発表では、この側面について詳細に解説しています。予備知識がなくともわかりやすい発表になっていますので、是非あわせてご覧ください。
DeNA TechCon 2020で「仕様起因の手戻りを減らして開発効率アップを目指すチャレンジ」という発表をしました（録画・スライドあり） - DeNA Testing Blog
より積極的な適用として
ソフトウェア開発のプロセスは、ある入力を別の形へと変換して出力する作業の繰り返しといえます。変換の中で混入した誤りが、後で致命的なバグに成長します。形式手法を活用すれば、そんなときに前後の入出力、あるいは別の変換を経た複数の成果物が同じ意味だと保証できるのです。これは非常に汎用的かつ強力なアイデアです。一度習得した技術が開発プロセスの至る所で使えるというのは、夢が広がりますよね。
私たち仕様分析サポートチームはそのような考えのもと、積極的に形式手法の活用局面を探っています。
おまけの副産物
形式手法の土台には多くの数学的背景が横たわっています。これはコンピュータサイエンスの土台でもあります。つまり形式手法を学べば必然的に、プログラミングの深い理解にも繋がります。
たとえば契約による設計は「オブジェクト指向入門」12でバートランド・メイヤーが唱えた概念ですが、その由来がHoare論理にあるのだと理解できました。
また、私はSwiftコンパイラ好きが集まるわいわいswiftc - connpassというイベントが好きでよく顔を出しています。そこでは発表のたびに「SwiftコードのコンパイルにはAST→Sema→IR→…というフェーズがあって」という説明が頻出します。この説明も「単にそういう手続きだ」というだけでなく「統語論と意味論を分けているのだな」と理論上の納得を得られるようになりました。
いろいろな技術領域を闇雲につまみ食いしていた私にとっては、バラバラだった知識に連続性がもたらされ、とても良い学びの機会となっています。
まとめ
人間はいい加減な存在です。自然言語の世界はなんとなく動いているように見えても、あちこちに誤魔化しや綻びがあります。たとえば「または」が排他的選言と両立的選言のどちらを示すかは文脈によるとか、「1日おき」の意味が曖昧だとか。でも我々は意識しないと曖昧さに気づけないものです。そんなあやふやな論理を扱う人間だから、一度日常の世界を離れて数理論理学の力を借りる必要があります。
形式手法は強力で信頼できる論理体系に支えられており、それでいて多種多様です。場合によっては親しみやすくもあり、思ったよりも汎用的な技術領域に感じられます。
そんな形式手法についての、今時点での理解について書き連ねてみました。私と同じように形式手法に対しての疑問を感じていた方への道しるべになれば幸いです。
今後もSWETでは形式手法の実用性を見極める研究を続け、アウトプットしていきます。よろしくお願いします。
-
「ソフトウェア工学の道具としての形式手法」 p2 https://www.nii.ac.jp/TechReports/public_html/07-007J.pdf↩
-
「ソフトウェア工学の道具としての形式手法」 p2 https://www.nii.ac.jp/TechReports/public_html/07-007J.pdf↩
-
The Gallina specification language — Coq 8.11.0 documentation https://coq.inria.fr/refman/language/gallina-specification-language.html↩
-
「ソフトウェア工学の道具としての形式手法」 p12 https://www.nii.ac.jp/TechReports/public_html/07-007J.pdf↩
-
「ソフトウェア科学基礎」p12 https://www.amazon.co.jp/dp/4764903555↩
-
記述上無限を扱えるという話であって、網羅的にパスを辿るモデル検査時にはパフォーマンス考慮が必要なことはあります。↩
-
具体的な記述の感触を掴みたい方は、仕様記述テクニック「Promotion」の紹介 - DeNA Testing Blogもご参照ください。↩
-
条件によっては「事前状態を引数として受け取り、加工して事後状態を返す」書き方に変換可能なことはあります。↩
-
「ソフトウェア工学の道具としての形式手法」 p4 https://www.nii.ac.jp/TechReports/public_html/07-007J.pdf↩
-
「型システム入門」p1 https://www.amazon.co.jp/dp/B07CBB69SS↩
-
「ソフトウェア工学の道具としての形式手法」 p13 https://www.nii.ac.jp/TechReports/public_html/07-007J.pdf↩
-
「オブジェクト指向入門 第2版 原則・コンセプト」 11章 https://www.amazon.co.jp/dp/4798111112↩
