TypeScriptで形式的証明を取り入れたプログラミングを実践します。
形式的証明とは、仕様またはモデルが数理論理学的に正しいものであり実装可能であることの形式手法による証明です。 本稿では形式手法のうち、型システムを利用した軽量形式手法による形式的証明を扱います。
この記事はTypeScript アドベントカレンダー2015 1日目の記事です。
TypeScriptアドベントカレンダー2015！！
去年あれだけいた戦士たちはどこへ行ったのか…
さて、形式的証明を実感するために1つのコードモジュールを作ってみましょう。
じゃんけんの結果をグー・チョキ・パーの3つの型を使って型推論だけで計算し、不正な入力を実行前に検出する、形式的妥当性の証明されたコードモジュールです。
まず前提となるグー・チョキ・パーの3つの型を作ります。
class Gu {
private identity;
}
class Choki {
private identity;
}
class Pa {
private identity;
}
TypeScriptの型は構造的部分型だから型を区別できないと思っていましたか？ TypeScriptには型を一意に識別する方法も用意されており、構造的部分型と公称的部分型の両方をサポートしています。
アクセシビリティ修飾子にprivateまたはprotectedを指定するとそのメンバーが他で定義された同名のメンバーに代入できない一意な識別子となります。
これによりTypeScriptでも公称型または公称的部分型である任意の代数的データ型とその直和型を作ることができるのです（数学的には共通部分のない型同士に限られますが実用上は気にする必要はないでしょう）。
また、TypeScriptのUnion typesは直和型そのものではありませんが直和型としての使い方もできるのでTypeScriptでも直和型の概念に基づいたプログラミングが可能です。
次にグーとチョキならグーが勝つといった論理（規則・仕様）を作ります。
interface Rule<T, U> {
(a: T, b: U): T;
(b: U, a: T): T;
}
interface Fight<T, U, V> extends Rule<T, U>, Rule<U, V>, Rule<V, T> {
}
var fight: Fight<Gu, Choki, Pa> = (a: Options, b: Options): any => void 0;
type Options = Gu|Choki|Pa;
最後にこれらの仕様の妥当性確認を行うバリデーションコードを書いて正しく機能しているか確認します。
<Gu>fight(new Gu, new Choki); <Pa>fight(new Gu, new Pa); ...
これで完成です。さっそく試してみましょう。
var correctWinner: Gu = fight(new Gu, new Choki); var incorrectWinner: Choki|Pa = fight(new Gu, new Choki); // type error
ちゃんと動いてますね。型だけで結果を得られるので問題によってはアルゴリズムを実装せずに正しい答えを得ることすら可能です。
var winner: Gu = fight(new Gu, new Choki) || new Gu;
型を見てから結果をハードコーディング余裕でした。テストでカンニングして途中計算を書かずに答えだけ書くようなものですね。
でもこれだけではつまらないのでもっとサイズを大きくしてみましょう。じゃんけんトーナメントを開催してみます。
グー・チョキ・パーの各インスタンスが個々の選手（の最初の手）となります。選手を区別したい場合はコンストラクタが初期化パラメータを受け取るようにして選手名などで選手を区別できるようにしましょう。このように実体を区別する必要があるときはさっきのようなずるはできません。
// 2回戦
fight(
fight(new Gu, new Choki),
fight(new Choki, new Pa)
); // Gu
// 3回戦
fight(
fight(
fight(new Gu, new Choki),
fight(new Choki, new Pa)
),
fight(
fight(new Gu, new Pa),
fight(new Choki, new Gu)
)
); // Pa
問題なくトーナメントが成立することが証明されていますね。
とはいえ…
fight(
fight(new Gu, new Pa),
fight(new Pa, new Gu)
); // type error
Oops! エラーになりました。ドローになり勝ち負けが決まらない場合を考慮していなかったのです。
形式的証明を行っても非網羅的定義までフォローしてくれるとは限りません。Haskellなど一部のプログラミング言語は定義の網羅性を検証してくれますが状態遷移がすべての組み合わせにおいて破綻なく循環することまでは検証してくれません。形式的証明用の言語やツールであればおおむね網羅的な検証を実施する機能を備えていますが、通常のプログラミング言語の型システムを利用するだけではそうした本格的な検証までは行えないのです。あくまでソースコード中で具体的に示された組み合わせの中での検証となり、入力する型を誤った実装や実装不可能な仕様やモデルを作らないための検証です。また、いずれにしても根本的定義ミスには無力なので過信は禁物です。
しかし、トーナメントに欠陥があり成立しないことは事前に判明しました。それも実装アルゴリズムに関係なく、テストケースの範囲外であってもです（形式的に正しいことを確認する妥当性確認は行いましたが、実装の正しさを検証する、通常のテストに該当する正当性検証は行っていません。なにしろ実装が空ですから。）。トーナメント中に発覚して興行を中止せざるをえなくなり、大ブーイングを浴びながら出資者からの法的責任追及と集団訴訟に怯えるよりよほどましです。これこそが形式手法と形式的証明の威力です。この欠陥の判明を受けてトーナメントを成立させるためにトーナメントが不成立となる組み合わせを認めないか、ドローの解決方法を定義するかは主催者しだいです。
以上のように、このケースでは形式的証明を導入したことで大きな成果を上げることができました。定義と運用の範囲内で動作可能であることが数理論理学的に証明され、逆に不可能である場合はそれを検出してコンパイルの段階で型エラーとして出力し、期待通り正しく機能したわけです。
宣言的で簡潔な型による抽象化された検証と証明は、アルゴリズムの実装可能性という尺度からソースコード上の仕様ないしモデルの評価を可能にし*1、手続き的になりやすく複雑な実装アルゴリズムの部分的テストよりも高水準な信頼性の指標となります*2。
静的型付き言語は静的型により動的型付き言語よりも早い段階で実装の正しさを検査して品質と信頼性を高めてきましたが、形式的証明はさらに早く、実装前の段階で抽象化された仕様やモデルを検証しているのです。
このように形式的証明はコードの品質と信頼性の向上に大きく役立つものです。毎年新しいフレームワークを覚えては使い捨てるより形式手法を1つ覚えるほうがよほどにスキルとコード品質が向上します。形式的証明はこのさき10年でも20年でも生きつづける安定した技術分野です。みなさんもぜひ使ってみてください。
TypeScriptアドベントカレンダー2015、次回は交差型を使って型に状態を動的に付与する形式的証明（交差型編）です。お楽しみに。
本稿に掲載したコードは以下のリンク先で形式的動作を確認できます。
