TypeScriptで形式的証明・直和型編 ～ じゃんけんゲーム最強トーナメント - falsandtruのメモ帳TypeScriptで形式的証明を取り入れたプログラミングを実践します。 形式的証明とは、仕様またはモデルが数理論理学的に正しいものであり実装可能であることの形式手法による証明です。 本稿では形式手法のうち、型システムを利用した軽量形式手法による形式的証明を扱います。 この記事はTypeScript アドベントカレンダー2015 1日目の記事です。 TypeScriptアドベントカレンダー2015！！ 去年あれだけいた戦士たちはどこへ行ったのか… さて、形式的証明を実感するために1つのコードモジュールを作ってみましょう。 じゃんけんの結果をグー・チョキ・パーの3つの型を使って型推論だけで計算し、不正な入力を実行前に検出する、形式的妥当性の証明されたコードモジュールです。 まず前提となるグー・チョキ・パーの3つの型を作ります。 class Gu { private identity; } c
