形式手法とテスト駆動開発の違いについての主観メモ
多分そこまで外してはないと思うが,まあ門外漢だから全然違うことを行っている可能性もある
全然違う気がしてきた
参考にしないでほしい
発端
それはそうと、軽量な形式手法たる型システム含む形式手法は記号の世界の中での正気はちゃんと証明してくれるが、人間様が頭を捻って作られた、自然言語で書かれた仕様とやらは一体何の正気を保証してくれるんだろう
の文意からこの記事の題は得られないと思うが,まああそれはそれとして…
余談だが,これはひごろおれが論理学について思っている
論理学の正しさは何によって担保されているのか?
例えば,論理学についてのあらゆる事実を「ならば/したがって」などの言葉で示すことは一体どういうことなのか?に近い気がする
余談終わり
テスト駆動開発
概要
1. 仕様をもとに,今書きたいプログラムが満たすべき/通るべきテストを予め書く.
2. テストが通るようにプログラムを書く
テストの必然性の疑わしさ
テストは,これはプログラムを書く人その人であったり,あるいはテスト部門(QA部門?)の人が書く.
ここではこのテストを書く人が究極的に信頼できる人間であって,つぎを満たすテストケース$ Tが得られるとしよう,
テスト$ Tが通る$ \implies仕様を満たす($ \impliesはならばを表す.)
したがって,あるプログラムがそのテスト$ Tを通るなら,そのプログラムは仕様を満たすことになる.
ところが,究極的に信頼できる人間なるものは一般に存在しない.
すなわち,一般的には,あるテスト$ Tがあったとしても本当にその仕様を満たしているかは怪しいケースが存在する.
テスト$ Tが通る$ \implies仕様を満たす?
テストの十分性の疑わしさ
次のようなテスト$ T_iをすべて$ T_1,\dots,T_n列挙することはできるか?
仕様を満たす$ \impliesテストケース$ T_iを通る
もちろんあらゆる状態について無限に考えられるならこれは常に真であるが,現実的にはそうではない
あるいは成約を強めて次のことを考える.
次のようなテスト$ T_iを過不足無くすべて$ T_1,\dots,T_n列挙することはできるか?
仕様を満たす$ \impliesテストケース$ T_iを通る
総括
以上の議論より,我々としては次のことを考えたい.
次を満たすテストケース$ T_1,\dots,T_nを過不足無くすべて列挙したい.
テストケース$ T_iを通る$ \iff仕様を満たす
出来ないのか?
これを過はさておき,不足無くについて列挙するという試みが形式手法である
形式手法
究極的に信頼できる人間というのは存在しないが,究極的に信頼できるシステムなるものは存在して
それは数学や論理と呼ばれる
数学や論理を用いて,
テスト$ Tが通る$ \implies仕様を満たす
は厳密に「そうです!」と言えるようになる
仕様を満たす$ \impliesテストケース$ T_iを通る
ようなテストは$ T_1,\dots,T_nです!と言えるようになる
実世界では,言語を制約したりして,
ある記述をすると勝手にテストが事実上通っているみたいなことになる
例えば,a: Nat, b: Nat, c: Natだったとして(ここではNatを自然数として用いる)
c = a + bという式について型検査が行われたとき,
1. =の左辺の型がNatである
2. 1より,右側の項a + bの型もNatでなければならない
これは規則であり,なぜ?と言われてもそうだからとしか言えない.
2': テスト$ T_1「a + bの型は自然数でなければならない」が得られる.
テストをすべて列挙すると$ T_1(だけ)だった.では$ T_1は通っているのか?
1. 型Natの項同士の+演算結果は必ずNatである
これは公理であり,やはりどうして?と言われてもそうだからとしか言えない
2. aとbの型はNatである
3. よって$ T_1は通る.
というのを型検査では裏で実質的にやっていることに等しい
もっと複雑な型になると当然$ T_1,T_2,\dotsと増える