型による契約プログラミング
ソフトウェアエンジニアの暮らしは処理失敗との戦い
しかし実用的なソフトウェアは現実を扱うため、多種多様な失敗と遭遇しうる
Error? Defect? Fault? Failure?
簡単に「失敗」と言っているが、意外とその範囲は曖昧
DBに接続できなかった
期待している仕様を破ってしまった
ユーザが不正な値を入力した
さまざまな規格の定義を紐解くと・・・
まとめると・・・
エラー(error)
人的ななんらかのミスに起因した不一致
DBのパスワードを間違えた
ユーザが異常なメールアドレスを入力した
注文個数に負値が入力された
欠陥(defect)
仕様や意図をシステムが達成できていないこと
パスワードは10文字以上である必要があるのに、8文字のパスワードを受け入れてしまった
絵文字は1文字としてカウントしたいのに、数文字分でカウントされてしまっていた
処理に失敗した場合は返金しなければならないのに、返金できていなかった
障害(Fault)
人的エラーもシステム上の欠陥もないが、システムが機能を遂行できない状態
クラウド上のDBに接続しようとしたが、ネットワークが疎通しない
ディスクがフルで、データを書き込めない
それでも対応すべきであると仕様に書かれているならそれは欠陥になりうる
仕様にないけれど仕様を達成できていない状態になっているという状態
故障(Failure)
障害が起こる、つまり障害の状態になること
堅牢なコードとは
なるべく上掲のエラー、欠陥、障害によってシステムがクラッシュしたり、データが不整合になることを避けたい
コーディングのレイヤーではどうすればいいのか?
仕様設計のレベルとかハードウェア実装のレベルの問題もあるが、ここでは立ち入れない
t-wada氏(2)によれば、以下の段階で失敗への対応を考えていく
予防的プログラミング
モジュールに渡ってきたものについて考える
典型的には、モジュールとは関数で、渡ってきたものとは引数
予防的プログラミングでは、渡ってきたものを信用しない
ユーザの入力を信頼しないように、関数の引数も信用せずにバリデーションする
想定していない異常な値、異常な状態が入っている可能性があるから
誤りやすいインターフェイス、そして責務の引き受けすぎという、エラーや欠陥の元を排除するという思想
攻撃的プログラミング
攻撃的プログラミングでは、異常な状態を検出した時点でモジュールをクラッシュさせる
ありえないデータが渡ってきた時点でできることはただ一つしかないはず
クラッシュさせる
アクターモデルをとるErlang、Elixir、Akka/Pekkoはこの思想
気楽にクラッシュさせるが全体としては動いている、という状態にする
予防的プログラミングと対立するわけではない(はず)
契約プログラミング
ある意味、予防的プログラミングと攻撃的プログラミングの合わせ技のような存在
おかしな値がやってきた→事前条件違反なのでクラッシュ
ありえない状態になった→事後条件違反になりうるのでクラッシュ
じゃあ堅牢ではないコードとは
すくなくともビジネス上の仕様を破りうるコードは堅牢ではない
契約プログラミング
プログラムの1コンポーネントに事前条件と事後条件という契約を持たせる考え方
わたくしこのコンポーネントは、事前条件を満たしさえすれば、事後条件を確約いたします、という契約を行っているとみなす
この考え方によりコンポーネントの責務が明確になり、バグを埋め込みにくい構造を作れる
どうやってやるのかは言語機能に依存する
D言語には専用の機能がある
inとoutで入力パラメータと関数の返値の契約を形式化することができます。
関数呼び出し時と返すときに動的にチェックが走り、違反していたら契約違反なのでクラッシュさせる
型とは許される値の集合である
型とは契約である
型による契約プログラミング
windymelt.icon はこれを推したい
参考文献