はじめに

みなさん形式手法をご存知でしょうか？
名前くらいは聞いたことあるけどいまいち何かわからないという方が多いのではないでしょうか。

その通りです。形式手法はアカデミアではそれなりに研究されているものの、
一般の（特にWeb系）ソフトウェア開発者が携わることはなかなかないのではないかと思います。

~~この記事ではソフトウェア開発に形式手法が導入されないのはなぜなのかを考察します。~~
この記事ではアジャイルソフトウェア開発において形式手法を導入する際のハードルについて考察します。

追記

本記事について、「形式手法は流行っていない」というのは正確ではないのではないかという指摘をいただきました。組み込み系や社会インフラ系等バグを絶対に出せないシステム開発では形式手法がよく使われているそうです。

ちょっと古いデータですが活用事例です。

誤解を招く紹介となっていたことをお詫びします。

さらに追記

kubo39さんより、形式手法の事例を２点紹介していただきました。（リンク)

どちらもとても興味深い試みでしたので簡単な要約とともに紹介させていただきます。

独自の仕様記述言語KMLを作成し、形式言語で書かれた設計から自然言語の設計書を生成するツールを開発
形式的な論理式に日本語の仕様を付記することで出力された設計書の可読性を高めている

Go言語のプログラムの安全性を定理証明支援系Isabelleで証明
Isabelleでプログラムとその証明を書き、証明済みプログラムをGoプログラムに変換

形式手法とは

ソフトウェア工学の道具としての形式手法によると以下のように説明されています。

形式手法は、システム、特に、ソフトウェアの開発法であって、数理論理学に基づく科学的な裏付けを持つ。明確で厳密な意味を持つ言語を用いて設計対象を表現することにより、設計記述の正しさを系統的に示すことが可能になる。したがって、開発したシステム、あるいは、ソフトウェアが高い信頼性を持つことを保証することができる。

すこし抽象的な説明ですね。形式手法は具体的な開発手法を指すわけではなく、さまざまな形があります。
ソフトウェア開発で実用レベルで用いることができる形式手法として本記事では　モデル検査とプログラム検証を扱います。

モデル検査

モデル検査はシステムの設計を形式言語で記述し、その性質を機械的に検査する手法のことを指します。
通常のシステム設計では自然言語で仕様書を書いたり、必要に応じてUML図を書いたりする¹でしょう。

例えば以下のようなラーメン注文システムを考えます。

ユーザが注文したいラーメンの種類とトッピングを選択する
ユーザが注文内容と合計金額を確認する
ユーザが決済処理を行う
システムがユーザに整理番号を通知する。同時に店舗に注文内容を通知する。
店頭でユーザが店員に整理番号を伝え、ラーメンを受け取る

このシステムの画面遷移を形式言語でモデル化すると以下のような状態遷移システムで表現できます。²

モデル検査ではこのような状態遷移システムに対して、
『決済を行う前は何度でもラーメンを選び直せる』『ラーメンが未指定の注文は発生しない』といった性質が成り立つかを解析することができます。

モデル検査を使うとシステム設計時に仕様バグを検出でき、より洗練された設計を作ることができます。

よく使われるツール

利用事例

プログラム検証

プログラム検証は実装したプログラムが期待する仕様を満たしているかを機械的に判定する手法のことを指します。
大きく分けると以下の３種類に分かれます。

Extended Static Checking (ESC): プログラムのアノテーションやコメントに仕様を記述し、静的に検証
Programming by Contract (PbC): プログラムのアノテーションやコメントに仕様を記述し、実行時に仕様違反があれば例外を投げて検査（厳密には検証手法ではないです）
Theorem Proving (TP): 定理証明支援系を使って証明付きのプログラムを書き、使いたい言語のコードに抽出

実用的なツール（言語）

OpenJML（ESC/PbC)
F* (ESC/TP)
LiquidHaskell (ESC)
Spec# (ESC/PbC)
D言語 (PbC)
Coq (TP)
Agda (TP)
Idris (TP)

適用事例

日本語でいい感じの資料は見つけられませんでした。

誰か教えてください

なぜ流行っていないのか

アジャイル開発とCI/CDの発展

形式手法の売り文句は設計段階や実装段階でバグを見つけることで、バグ修正のコストを下げるというものです。これは「設計」→「実装」→「テスト」の工程がはっきりと分かれているウォーターフォール開発モデルを前提にしています。

しかしながら、現代のソフトウェア開発ではアジャイル開発モデルが主流になってきています。
アジャイル開発では「設計」→「実装」→「テスト」のサイクルを細かい単位でまわし、ソフトウェアを動かしたまま少しずつ作り上げていきます。
さらにテスト駆動開発を採用している場合、ユニットテストを常に回しながら開発を進めるため、形式手法を用いなくとも実装段階で多くのバグを潰すことができるようになりました。

また、CI/CDの発展により高頻度のデプロイが可能になりました。サーバサイドならば１日複数回のデプロイが可能になり、クライアントアプリでも１週間に一度程度はデプロイができるようになりました。

そのため、クリティカルなバグ以外はデプロイ後にバグが発覚してもすぐに修正して再デプロイできればそれほど問題ないという考え方になり、逆に、開発リードタイムを長くする手法は敬遠されるようになりました。形式手法を用いると設計や実装にどうしても工数がかかるため導入には慎重にならざるを得ません。

形式手法を用いてもバグは０にならない

形式手法を用いると数学的にプログラムにバグがないことを証明できるとされています。
しかし、そのためには　システム全体を数学の言葉で表現できなければなりません。
現実のシステムは複雑で全体を形式的に記述することは不可能であり、実際に形式手法が保証できるのは用いる手法で表現可能な範囲に限られます。

さらに問題を難しくするのは、形式手法を適用できる部分と適用できない部分をうまく分離できないという点です。プログラム検証を実際のシステムに導入しようとすると

証明のついた安全なコード
外部ライブラリやAPI呼び出し等、ブラックボックスとして扱う他ないコード
既存の未証明の大量のコード

が複雑に絡み合ったものになります。このようなシステムで形式手法が一体何を保証してくれるのかは極めて非自明となり、形式手法を用いているのにバグがなくならないということになります。

設計と実装の乖離

モデル検査を用いると設計の正しさを調べることはできますが、実装が設計通りになっていることを保証するのは開発者の責務です。
特にアジャイル開発では頻繁に機能の追加や実装の修正を行います。それは仕様変更が頻繁に起きるということを意味します。

度重なる仕様変更の中で設計書を仕様変更に常に追随させるのはなかなか困難です。
いずれ設計と現在の実装の間にはズレが生じ、そのズレは徐々に大きくなります。
実際の実装を反映していない設計の正しさをいくらモデル検査を使って保証したところで無意味です。

何を検証すべきかわからない

プログラム検証ツールをただ導入しただけだと、開発者は何を検証すべきかわからず、効果的に使うことはできません。

例として、ラーメンの料金を計算するJavaプログラムの仕様を考えましょう。

public class Ramen {
  /**
   * @return 単価（円）。0以上2,000以下
   */
  int getPrice() {...}
}

public class Topping {
  /**
   * @return 単価（円）。0以上200以下
   */
  int getPrice() {...}  
}

public static final int KAEDAMA_UNIT_PRICE = 100;

/**
 * ラーメンの合計料金を返します。
 * @param ramen 注文したラーメン(NonNull)
 * @param toppings トッピングのリスト（Nullable)。長さは10以下
 * @param kaedamaCount 替え玉の回数。0以上5以下
 * @return ラーメンの合計金額（円）。0以上10,000未満
 */
public int price(Ramen ramen, List<Topping> toppings, int kaedamaCount) {

  int price = 0;
  // ラーメンの単価を加算
  price += ramen.getPrice();

  if( toppings != null ) {
    // トッピングは安い順に二つまで無料
    toppings.sort();

    for( int i = 2; i < toppings.length(); i++ ) {
      // トッピングの単価を加算
      price += toppings.get(i).getPrice();
    }
  }

  // 替え玉の数
  price += kaedamaCount * KAEDAMA_UNIT_PRICE;
  return price;
}

priceメソッドをプログラム検証で解析する場合、大きく二つの方法があります。

厳密な検証

一つ目の方法では、ビジネスロジックそのものを検証します。すなわち入力に対する出力が１通りになるように仕様を書きます。
この場合、プログラムには実装バグがないことが保証されるため、ユニットテストは不要となります。

しかしながら、複雑な仕様を形式的に書き下して証明をつけるのには相当の工数がかかりますし、形式的に書かれた仕様とプログラムの実装がほぼ同じになるために、仕様が正しいことを確信できないという問題もあります。

緩い検証

２つめの方法では、プログラムが異常な振る舞いをしないかを検証します。「異常な振る舞い」とは

実行時エラーが発生する
メソッドを引数にドメイン的に不正な値を渡す。
返り値がドメイン的に不正な値となる

ことを意味します。上記のロジックの例では

NullPointerExceptionやIndexOutOfBoundsExceptionが発生する
合計料金が負の値や10,000以上になる

となるでしょう。

この場合はビジネスロジックが正しいことは保証されないので別途ユニットテストで動作確認をする必要があります。しかし、仕様を書き下すのにかかる工数は比較的少なく、また大部分を自動的に検証することができます。

このように、形式手法で何を担保するのかを明確にせずに導入すると
開発者は複雑な仕様を検証しようとして必要以上の工数をかけてしまったり、
逆に、緩すぎる仕様を検証したためにバグを見逃してしまうといったことが起こります。

形式手法は開発者体験を悪化させる

形式手法を使うとエラーを早い段階で見つけることができるため、開発者体験(DX)が向上するように思えます。
しかし、実際には素朴に導入するとDXはむしろ悪化します。以下のような点に注意しなければなりません。

False alarm

プログラム自動検証手法は健全ですが完全ではありません。³
したがって実際には問題がないのにアノテーションが不足しているために検証に失敗すること（False alarm）があります。

False alarmは開発者を苛立たせます。以下のシチュエーションを想像してみてください。

あなたのチームでとある開発者とコードレビューを行うプロセスを導入することになりました。
その開発者はコードについて詳しくないので、至る所で「このコードが正しいことを説明してください」
と求めてきます。稀にその質問に答えることでバグが発覚することはあるのですが、大半はただその開発者が理解不足なだけです。

あなたはその開発者と一緒に仕事をしたいでしょうか？

せっかく形式手法を導入しても、False Alarmのために無駄な仕事が増えるという印象をもたれると、すぐに使われなくなります。

リファクタリングを疎外する

形式手法で検証済みのコードを修正する場合、その証明をやり直す必要があります。そのため、そのコードをリファクタリングしようと思っても、証明をやり直す工数がないため、リファクタリングできない事態が発生します。
一般にリファクタリングできないコードは保守性が低いため嫌われます。

ビルドが遅くなる

静的にさまざまな性質を検証しようとするとどうしても時間がかかります。
ビルド時間が長くなると、エンジニアの生産性が顕著に悪化します。

言語のロックイン

これは本質的な問題ではないですが、現状のプログラム検証ツールは限られた言語やバージョンでしか対応していません。たとえばOpenJMLはJava8でしか使えません。検証ツールがないために言語の変更やバージョンアップができないのは困ります。

どうすれば流行るか

さて、形式手法をソフトウェア開発に導入することの難しさは理解してもらえたかと思います。
そこでどのような要件を満たせばソフトウェア開発に導入できるかをまとめます。

銀の弾丸を目指すな

形式手法のコミュニティではその手法の検証能力の高さやその表現力が重要視されます。

しかし、そのような万能な手法は実際には証明の工数や実行時間の観点からほとんど動きません。
表現能力や検証能力を限定し、何を検証できるのか明確でちゃんと動く手法の方が使い勝手が良いでしょう。
例えば、Nullポインタ解析に限定する、扱える仕様をPresburger算術に限定するなど。

テストと和解せよ

形式手法はよくテスト手法と比較されます。特に形式手法の研究者の中にはテストのことを「有限のケースでしか保証できない不完全な手法」と見なしている人もいます。
実際にはテスト手法（特にユニットテスト）は偉大な発明であり、形式手法で置き換えられるものではありません。互いの性質を理解して効果的に使用することが重要です。

テストが適している
- 各ユニットのロジックの確認
- E2Eの動作確認
形式手法が適している
- 抽象的なライブラリのコードの検証
- 仕様バグの検出
- デッドロックやデータレース等、確率的に発生する不具合の防止
- モジュールを結合した時の不整合の検出

DXを重視せよ

上記のように形式手法はテストを置き換えるものではありません。
形式手法を導入すると開発プロセスが増えることになるため、開発の足かせにならないように注意する必要があります。
例えばつぎのような工夫が考えられるでしょう。

時間のかかる解析はCIでのみ走らせる or 差分解析を行う
健全な静的解析にこだわらず、未検証のコードの存在を前提とした漸進的手法を用いる
本当に修正すべきエラーのみを開発者に通知する
アノテーションは最小限にとどめる
設計と実装の乖離をテストで検出する or 実装から設計を抽出する

実は流行っている

さて、流行る形式手法の条件はざっくりいうと以下の３点にまとめられます。

検証力・表現力は限定されているがちゃんと動く
テストと相補的である
DXを向上させる

じつはこのような条件を満たしている形式手法が既にあります。

それは「型システム」と呼ばれています。

特にTypeScriptやRustでは型の強さと型推論のバランスの取れた型システムが採用されており、
流行っていることは疑いの余地はないでしょう。

実は形式手法はAIと同じように実用的になった時点で別の名前がつく言葉なのかもしれません。

UML図も一種の形式手法だとする見方もありますが、設計図を機械的に解析できないのでこの記事では形式手法ではないとします。 ↩
この図はイメージです。実際のツールをつかって生成されたものではありません。 ↩
健全性は検証結果が「仕様を満たす」だった場合、実際に任意の入力に対して仕様を満たすという性質です。完全性は「仕様を満たす」プログラムを常に正しく検証できるという性質です。健全かつ完全なプログラム検証手法は存在しないことが知られています。 ↩

形式手法はなぜ流行っていないのか