TEFに燃料投げたら秋山さんが答えてくれた

Kenichiro Ota @oota_ken

まあ、定理証明は正直難しくてよくわかんないんだけどなw

あきやま🍠 @akiyama924

@kyon_mm それは「テスト戦略，テスト分析でカテゴライズ」が前提になっていますよね。私が言っているのはテスト対象ソフトウェアのできあがってくる過程が先にあって、ある程度それを意識して活動する方がベターと思うのでカテゴライズが先なのです。色々なやり方があってよいと思いますが。

あきやま🍠 @akiyama924

@oota_ken はい。命題と関数の対応（証明）は取れると思います。でも、命題（＝形式仕様）が間違っている場合と、実時間に証明が終わるのかという話がありますよね。

きょん＠アジャイルコーチ、システムアーキテクト @kyon_mm

@akiyama924 なるほど。その場合だと単体/結合というカテゴライズがやはりやりやすいのでしょうか？先の主張の根底にあるのは「単体テストとかってテンプレートをつくっちゃうとそれに合わせたテストになっちゃうのが問題で、毎回適切なカテゴライズしよう」っていう意識があります。

Kenichiro Ota @oota_ken

@akiyama924 僕はまだ定理証明のことをほんのちょっとしかわかってないのですが、命題自体があやまっていることつまり仕様自体が誤っていることたとえば仕様間に矛盾があることなどを定理証明機は発見してくれます。ここが面白いところです。

Kenichiro Ota @oota_ken

@akiyama924 で、実時間の問題はもちろんあると思います。デスので、現状は限られた命題して無理でしょう。が、実時間の問題はテストの方がむしろ課題を抱えているわけで。

Kenichiro Ota @oota_ken

が、定理証明ツールで実時間内に解けないような問題はそもそも実装してもそれに対するテストは実時間内に終わらない気がする。NP完全とかそこらへんの話からすると。

あきやま🍠 @akiyama924

@kyon_mm にしさんも同じようなことを仰っていますね。私は、「ソフトウェア開発（コーディング）のフェーズに合わせて考えるべき」と書いた通り、それが単体を出しにくいものであったら違うフェーズにしたほうが良いです。開発の切りがよいところってありますよね？それに合わせるわけです。

あきやま🍠 @akiyama924

@oota_ken はい。定理証明機を否定するつもりは全くありません。使いどころではどんどん使って欲しいです（だから、SQiP研究会でも形式手法分科会始めました！）。実時間の問題はテストの方かなぁ？？そんなことはないと思うけれど。

Kenichiro Ota @oota_ken

@akiyama924 集合を集合のまま扱えることでサンプリングによる発散を避けるというのが定理証明機の1つの目標だったようです。自然数の集合とかをそのまま扱えれば、少なくともテストよりは組み合わせ爆発を防げるはずと。でも、それも命題によるのかもしれません。

きょん＠アジャイルコーチ、システムアーキテクト @kyon_mm

@akiyama924 コードがある程度統合された段階でないとテストが出来ないものが出る(単体レベルだとモックテストになる)から、それらを結合テストと名付けてやるって言う感じですか？

あきやま🍠 @akiyama924

@kyon_mm コードを書く前にTDDでテストコードを書く、一つのクラスの関数が一通りそろったらクラスに対するテストコードを書く、全てのコードはそろっていないんだけど、機能を確認できるようになってきたら単体テストを行う。開発済みコードが増えるにしたがってテスト範囲を広げていく。

あきやま🍠 @akiyama924

@kyon_mm もちろん、今ツイートしたのは、たとえばの例です。

あきやま🍠 @akiyama924

@oota_ken うーん。それは、関数レベルの証明なんじゃないですかね？　詳しくないのでよく分かっていないのですが。

きょん＠アジャイルコーチ、システムアーキテクト @kyon_mm

@akiyama924 なるほど。となると、コードの成長に合わせてテストをすべきというのが根底にあって、それらは言語やフレームワークによっても変わってくるからそのたびに考える。って感じでしょうか？どちらかというとシステムアーキテクチャによってテストレベルが変わるイメージ？

かわにし @tosikawa

@oota_ken なので、ある意味、感みたいなものによる絞り込みが必要になりますよね。もしくは近似解を求めるようなヒューリスティックな手法ですかね。

あきやま🍠 @akiyama924

@kyon_mm はい。前半はそんなイメージです。言語やフレームワークによって変わってきますが、言語やフレームワークはそうそう（一つのプロダクトでは）変わらないので毎回考えることはないです。システムアーキテクチャより前の、開発戦略＋テスト戦略で考えるイメージです。

きょん＠アジャイルコーチ、システムアーキテクト @kyon_mm

@akiyama924 なるほどー。なんとなく理解できました。ありがとうございます！

かわにし @tosikawa

きょんさんのTEFの自己紹介から始まった一連のTwitterでの話がまとまっていないのが悔やまれる。

きょん＠アジャイルコーチ、システムアーキテクト @kyon_mm

@tosikawa Togetterにまとめておきます。