形式手法の実務への第一歩
今回は、前回で形式手法が、使用とか要求を日本語ではなくて、決まった書き方とか解釈のルールがある数学の言葉で書いて、
人によって解釈がぶれないようにして、性質を証明できるっていうようにする道具みたいなことが、ざっくりわかった気になったんですけど、
あと、ちなみに道具ってところが個人的に一番重要なところかなと思いましたね。 そうですね。
形式手法に関して。
形式手法は道具とか考え方とかに近いもので、どういう時に使うかっていうと、とにかく網羅的にきっちり検査しきりたいって時に使う道具ですね。
従来の開発だと、テストって、例えば1たす1が2であることを確かめるときって、1たす1って入れて、それが2だったよねってエキスペクトとかで見る、アサートとかで見るって感じですよね。
っていう風にいくつかのサンプルを試すことで、自分たちが作ってるものが合ってるらしいってことをやる、的当てみたいなことをやったわけですよね。
なんですけど、形式手法はその的全部を試す、そういう風な考え方を持っているっていうので、とにかく網羅的にきっちり試したい時にやりたい道具って感じですね。
従来の開発のテストだと、いくつかのサンプルだけ、しかも特定の有限なサンプルだけ試して、それでOKかどうか確認していた、点で確認していたのを形式手法の場合はもうちょっと広げて面で確認できるみたいな検査
手法っていうことですよね。
おっしゃる通りです。
そういった形式手法なんですけど、使ってみたいなって考えた時にですね、目標としては実務で、普通にウェブサービスとかを開発するような実務で、仕様を形式手法でかけるようになりたいなっていうことになった時に、
まず何から始めたらいいんだろうって全くわかんないんですよね。
ちょっと今日ここを聞いてみたいなと思います。
わかりました。まず私が最初の一歩としてお勧めするのは、プロパティベースドテスティングって呼ばれている、ちょっと従来のテストの延長線上にあるところから話をしていこうと思います。
Property-Based Testingと性質の発見
このプロパティベースドテスティングっていうのは従来のテストと何が違うかっていうと、従来のテストっていうのは先ほど言った通り、いくつかのサンプルを選んできて、それが合っているかどうかを試す、エグザ
ンプルベースドテストっていう風に呼ばれているのが従来のテストです。
これエグザンプルって言ってるのが1たす1イコール2だと、1と1っていうのが2になるよねっていうエグザンプルを選んできてるっていうところから来てる名前です。
これに対してプロパティベースドテスティングっていうのは、この入力1たす1って部分を機械が作ってくれます。いっぱい大量に100個とか1000個とか作ってくれます。
すごい。
それでテストを回してくれるので、1個や2個のエグザンプルベースドテストを書くよりも、圧倒的に多くのテストケースを試すことができるっていう方法なんですね。
さっきの例だと、いっぱい点を打つみたいなイメージですかね。
いっぱい点を打つってイメージです。本当にその通りです。
ここでみんなプロパティベースドテスティングを書けばいいじゃんって思ったかもしれないんですけど、実は難しい壁が立ちはだかるんですね。
これちょっと考えてみて欲しいんですけど、さっき足し算の例を出しました。1たす1イコール2って出しましたよね。
はい。
xたすyっていう風になって、要するにxの中に何らか機械が生成した数字が入って、yの中にも何らか機械が生成した数字が入る。
xたすyってこれ何を検査したらいいですか?大量に。xとyに何が入るかわからないわけですよ。
無限ですよね。
無限ですよね。だからアサートに何をかけますかっていう。
単純にxプラスyを隠してないんじゃないかと思っちゃいます。
そうするとxプラスyイコールxプラスyになって、それは何立つのかバグってもわかんないわみたいな感じになるじゃないですか。
意味ないですよね。
意味なくなっちゃう。だからここで考え方の転換が必要になったのがわかると思います。
エグザンプーベースドテストだと具体的なものを使えていたので、これはこうなるよってこと、人間がいくつか選んでくることができたんですけど、
プロパティベースドテスティングになると入力と出力を使って何とかうまいこと何立つ関係っていうのを見つけなきゃいけない。
性質を見つけなきゃいけないんですね。
具体的な入力と具体的な入力に依存してはいけないということです。
例えばどんなものがあるかっていうのをいくつか例を挙げてみましょう。
まずはxプラスyはyプラスxと同じはずですね。
そうですね。数学的にはそうですね。
ひっくり返したら同じですよね。これがまず1つのルール。
他にも例えばxに1足したら絶対違うはずですよね。
絶対違うはずですね。
xと0を足しても絶対同じになるはずですよね。
同じはず。
っていうふうなことをどんどん試していくんです。
なるほど。ルールを抽出していくっていうことですよね。
絶対的なルール、この関数においてのルールを抽出してそれをリストアップしていくみたいなイメージですかね。
そういうイメージです。
これすると確かになるほどいっぱいの例を試すことができるなって感じしますね。
機械がいっぱい入力を作って、xプラスyがyプラスx。
ひっくり返っても大丈夫だねっていうふうにしたりするってことをいっぱい試せば
確かにだんだんと間違ってるのはわかりますよね。
明らかにxとyとはひっくり返しても間違ってるから明らかに間違ってるっていうのがわかるようになってくる。
こういう性質をいっぱい感じがらめにしていくと
徐々に1プラス1が浮き彫りになっていく。xプラスyが浮き彫りになっていくってことをやることができる。
これがプロパティベーストテスティングの考え方です。
すごく難しそうだなと思っちゃいましたね。
ルールを抽出するっていうのが抽象的。
今の話だったらxプラスyっていう簡単な式なのでわかりやすいんですけど
じゃあ実際の関数とかでそういうのをどう書くんだろうっていうのは
ルールを抽出するってすごく難しい抽象的だなと思っちゃったんですけど。
実はこの性質って穴があることもあるんですよ。
例えば性質でxプラスyとかひっくり返したりした時に
いくらこういう風な性質を試したとしても
実は1プラス1が3になっちゃったりしても見分けられないってことありそうですよね。
例えばさっきの話だと1プラスxは違う数字になるって言ってるんですけど
1プラス1が3になっても違う数字になってますからOKですよね。取っちゃう。
っていう風に本来はこれちょっとやっぱ違うんだけどっていうのとかがくぐり抜けてきちゃう時があるんですよ。
じゃあこのくぐり抜けてくるってことをいかになくす性質を考えるか。
FizzBuzzで考えるジェネレーターと反例
ここが形式処方の入門になってきます。
なるほど。本当に証明みたいな感じの考え方的に。
この範例が出てきたからその範例に対する対応をどうするのかっていうのをルールで考えて
じゃあこういうルールを入れたらこの範例は大丈夫になりましたねみたいなことをやっていくってことです。
1プラス1みたいな足し算の場合、実はこれが結構難しい例になっちゃうんで
もうちょっと簡単な例から最初出発しましょう。
まずフィズバズ、よく私がフィズバズ出しますね。
1の時は1、3の時はフィズ、5の時はバズ、15の時はフィズバズが変えるっていうのがフィズバズ関数ですね。
このフィズバズ関数をプロパティベーストテスティングこれからしていきます。
そしたらどうするかっていうと
まずは私だったら3の倍数だけ作る君っていうのを作ってですね
これをフィズバズ関数に入力します。
3だけだから全部フィズバズが返ってくる?
これで5と5と同じことを試せますね。
あとは3と5の両方の倍数である15をかけるっていうふうなことをすると
必ず3の倍数と5の倍数の両方の倍数になりますからフィズバズが返ってくるってことが期待できます。
ちなみに3の倍数だけだと5倍しちゃうとフィズバズになっちゃうので
それだけだとちょっとダメですね。5の倍数は弾かなきゃいけない。
5で割り切れないといいっていうふうにしてあげる。
っていうふうに作られるものを絞り込んでいくと
うまいこと性質を並べてミシィに作ることができる。
ミシィって漏れなく、かぶりなくっていうのを作ることができて
これができた時使用をちゃんと記述できたってことなんですよ。
フィズバズの場合は3の時がフィズ、5の時がバズで
3と5の倍数の時がフィズバズっていう仕様を表現できた。
正確に言うと3の倍数かつ5の倍数ではないっていうのがつかないと
どっち?ってなっちゃうんで。
確かに。
これがつくとフィズバズの仕様になるんですね。
っていうふうに自分が意図したものっていうのを正確に
どんな関係とか今言ったのは
成績、値を作る部分、成績って言うんですけど
これジェネレーターって言うんですけど
このジェネレーターを工夫してあげると
うまくバリッドなものだけ、正しいものだけを作ることができて
その正しいものを入れると単純な性質が浮かび上がってくるってことがよくあるんですよ。
なのでこういうものとかを使って
徐々にどういう風に性質を書いたら
こいつは間違いなく寸分のクルーもないっていう性質のパターン
BGに書けるかってこれが
形式書のすごく大事な部分の一つです。
なるほど。一番ベースになる考え方というか。
そのメソッド、その関数、その何らかの仕組みが
どういう性質で仕様を構成しているか
みたいなところを考えるってところなんですね。
ちなみにさっきのフィズバズの話でちょっと気になったのが
3の倍数の時にフィズが変わりますと
5の倍数の時にバズが変わります。
もう1個3と5の倍数でフィズバズが変わります。
これ今3つ用意したじゃないですか。
この3つの性質がフィズバズ関数にはあるよねっていう話かなと思うんですけど
これが3の倍数の時は変え入り値にフィズが入っている。
5の倍数の時にバズが入っているのを2個だけでも
表せられるんじゃないかなと思ったんですよ。
3個と2個どっちがいいんですか?
まず試行実験をしてみましょう。
私が今実装して間違ってフィズフィズっていうのを出すような
感想を作っちゃいました。
フィズフィズ。フィズじゃなくてフィズフィズです。
これはどうなりますか。2つがどう判定するかを考えてみましょう。
なるほど。僕が言った方の2個の場合は
5の倍数入ったらOKって言っちゃいますね。
フィズが入っていることを判定しちゃうので。
ゴミが入っちゃったって言い方をしますね。
ゴミが入っちゃうときはダメだと。
それが今のフィズフィズが返ってきたっていうのが
反例になるってことですね。
そうです。
つまり5の倍数の時かつ3の倍数じゃない時は
フィズ単体で返ってくるしかないってことですね。
そういうことですね。
あとはバズフィズとかやられてもわからなくなってますね。
フィズバズ期待しているのに。
そういう風になっちゃいます。
なのでこういうのはなるべく具体的にしていった方が
変なものがマッチする可能性を減らす方が
一般的には良い仕様になるって感じですね。
ちなみにさっきの例だったら
プロパティベースドテスティングだったら
一番最初はもしかしたらさっき自分が言った
フィズが入っているとかバズが入っている
っていうテストにするとするじゃないですか。
プロパティベースドテスティングの中で
機械的に入力をいっぱい生成して
それでテストするみたいなことをしたときに
さっき国明さんが言っていた
フィズフィズみたいなのが出てきちゃいましたと
っていう感じのことを通った上で
その後やっぱりフィズフィズが出てきちゃったから
間違えてたからこの性質をちゃんとルールにして
三つのルールにしましょう。
一番最初に三つのルールにしましょうっていう
過程をたどるっていうのが結構重要だったり。
まさにその通りなんです。
これが私が最初に形式手法は考え方の一つである
っていうふうに言ったのはまさにその通りで
これはどんなふうなことを表しているのかなってことを
深く考えていくと勝手に気づくんですよ。
いろんなことに。
そうなっていくとこうしなきゃこうしなきゃって
どんどんどんどんどういうふうに振る舞うべきかってことが
ちゃんとパターンとして記述できるようになってくる
ってことですね。
なるほど。
なるほどですね。
その考え方というか
一番最初は別にパターンが少なくて
本当に穴があってもいいから
そこをどんどん穴を埋めていきつつ
完璧なパターンにしていく。
でもそこまで行っても
多分完璧とはならないのかもしれないですよね。
プロパティベースのテスティングの場合は。
っていう考え方は重要ってことですね。
そういった進め方の。
そうです。
事前条件・事後条件と契約による設計
このジェネレーターを作るときっていうのは
すごくいろんなことに気をつけなきゃいけなくて
ジェネレーターがゴミを作っちゃいけないんですよ。
例えばさっきの話だと
マイナス1とかをジェネレーターが作ってきたら
何が起こるかっていうと悲惨なことが起きますね。
負の整数を入れてきたらダメだよね。
フィズバズ関数。
確かにフィズとかバズとか出てきちゃうんだけど
実装は多分典型的には
3で割って余りがないみたいなのを見るでしょうから
出てきちゃうんですけど
出てきちゃうんだけど
それは作っちゃダメなんで
ジェネレーターっていうのは
有効な値の範囲だけしか作らないようにする
っていうことがすごく大事なんです。
これがすごく大事で。
なるほど。
これは形式手法の世界だと
事前条件という言い方をします。
事前条件。
事前条件。
前提の範囲がないっていうことですよね。
そうです。
この事前条件を守らない入力に対しては
実装は何を返してもよいとするのが
形式手法の中でいうと
契約による設計とかって呼ばれてるような
その形式手法の流儀があって
その流儀の言ってることなんですね。
まずジェネレーターは
事前条件の中に入るものだけを作りなさい。
作りなさい。
それがまず。
その後に作った後
入力と出力の間でごちゃごちゃってやって
Fizzに最終的になるんですみたいなことを
作るわけですよね。
この部分を事後条件という言い方をします。
事後条件。
ちょっと難しいです。
入力と出力の間の関係。
入力に3が来たらFizzが返る。
15が来たらFizzバズが返る。
こういうふうな表みたいなのをイメージすることができて
この表っていうのが事後条件であたることですね。
さっきのプロパティベースドテスティングの話の
ルールのことですよね。
そうです。ルールのことです。
3が来たらFizzが返る。
というところが事後条件と言います。
これであなたは契約による設計をほぼ理解しました。
形式手法の部分ですね。
実はこの形式手法ってこういうふうに
網羅的にやった時に
いろんなものが抽象的になっちゃうんだけど
それをどう組み合わせたら
漏れなく定義したことになるかとか
ってことを考えているところなんですね。
事前条件、事後条件って急に言われるって難しく思えるけれども
従来のテストの延長線上にあるんですよ。
プロパティベースドテスティングをまずやると
この事前条件と事後条件って
間違いなく意識させられるはずなんですね。
これをくぐり抜けていくと
だんだんと
あ、ちょっと契約による設計がわかった
みたいなことが言えるかもしれない
っていうふうなところがあって
契約による設計がわかると
形式手法の中で言うと
法和論理って呼ばれている一派の一部を知ったことになるので
もうだいぶ張力な武器を手に入れたと言える。
なるほど。
ちなみに事前条件が満たしていないものに関しては
どんな値を返してもいいというか
どういう振る舞いをしてもいい
っていうのが形式手法の
大前提ルールみたいなものとしてあるって話だったんですけど
それをやっているのは
それが必要なのは
それがないと
そういったルールがないと
無限に発散してしまうからってことですか
有限に収めたいからってことですか
すごく鋭いですね
実は何で事前条件と事後条件を分けるかというと
まさに今おっしゃったように
無限ループとかっていうのの可能性を排除したいからなんです
実際この範囲では無限ループしてほしくない
みたいなのあるじゃないですか
フィズバスが無限ループしたら困るわけですよ
帰ってこなくなると困る
だから事後条件の中では
無限ループを基本的に許さないように書くですね
これを停止性って言い方をします
停止性
止まるよねっていう
この停止性は事前条件を満たす範囲で
基本的には言われていることですね
つまり事前条件を満たさないものは
無限ループしてもいいんですよ
無限ループしてもいい
最悪してもいいってことですね
なぜならそれは入力されないからってことですね
入力したらそいつの方が悪いってことです
そういう考え方を持っていて
この停止性と事後条件の部分
事後条件が合っていることを
部分正当性って言うんですけど
この2つをドライに記述するときに
両方とも同じ有効な値があるわけですよ
有効な入力がある
これを事前条件と呼ぶことにしている
っていう風な構成になっているので
ヘンテコさんのおっしゃった通り
無限ループとか収めたいからですかね
っていうのはまさにその通り
停止性っていうのを書きたいと
その部分正当性って
事後条件の部分と一緒に考えたいから
事前条件っていう風に括り出している
という風なのがまさにそのものです
なるほど理解できました
なんとなく理解できました
バリデータとWeb APIの事前条件
さらになんですけど
事前条件
現実のソフトウェアの開発のテストを
プロパティベーステストするときの話なんですけど
その事前条件を満たしているかどうかの
テストが必要そうだなと思っちゃったんです
つまりこれが入力のバリデーションみたいな話
なのかもしれないんですけど
そういったのが必要ですよね
まず原理原則に従って言うと
事前条件を満たさない入力に対しては
どう振る舞ってもいいので
エラーを投げてもいいんですよ
だから先頭にアサハトとか書いてもOKなんです
例えばフィズバーズ関数だと
0以下の入力いらないんで
0以下だったらアサハトで例外出す
みたいなことを書いてもOK
なぜなら事前条件に一致してないんで
無限ループ賞が例外になるようか
何回してもいい
だからそういうものを入れようって
これを防御的プログラミング
言い方をしますね
防衛的プログラミングとか防御的
だから事前条件に反したものは
もうエラーでさっそく弾いちゃうよ
その方がデバッグが楽だよって考え方が
防衛的プログラミングって考え方です
バリデーションの時に弾いてしまって
一番最初に早期リターンみたいな形で
返してしまおうねっていうような考え方
そうですね
設計的には
設計的にはそうです
ただちょっと難しいのは
バリデータっていうのの事前条件って
一体何だろうって考えるのは
すごくいい頭の体操になるんですけど
バリデータの事前条件
バリデータ
例えば三角形の三辺の数字を
入力する3,4,5みたいなの入れたりする
とかって入れたりすると
有効な三角形かどうかっていうのを返すような
バリデータを考えてあげましょう
はいはいはい
三角形にならないような
三辺を与えることもできるので
有効な三角形っていうのがある
適当なものをね
このバリデータの事前条件って何でしょう
これはすごく原理原則に従って考えると
何だろうって考えるのはすごく勉強になります
何でしょう
でもそれはあれですよねきっと
三角形の性質をちょっと読み解いてというか
ちゃんとやって
それに適するものが入って来なかったら
返してしまうみたいな
エラーとして返してしまうみたいな
そうですね
だけどよくよく考えたら
その時に例えば
1,1,10っていうのは
どうやっても三角形にならないんですけど
そうですね
10が長くて1と1を足しても
10にならないじゃないですか
だから
三角形がどうやっても繋がらないっていうのが
1,1,10とかなんですけど
この1,1,10とかっていうのが来た時に
エラーを返さないっていうケースは許されるか
ってことを考えてみるといいです
エラーを返さないことを許されるか
それは許されないんじゃないですか
ですよね
だからよく考えてみたら
あれ事前条件で落としていいものって何だっていうと
実はバリデータって事前条件は
全部落としちゃダメなんです
異常なものをエラーにしないといけない
なるほど
だからその性質によっては
やりたいことのルールによっては
バリデーションで全てを返してしまってはダメで
ちゃんと適するものだけは
素通ししないといけない
それもそうなんですけど
どっちかっていうと
バリデータの事前条件は
常にどんな入力でもウェルカムなんです
なるほど
理解しました
なぜかというと
事後条件でエラーにするか
それともOKにするかっていう判定をする
っていう部分なんで
実は
バリデータの性質上はそうですね
これすごく誤解されやすい
AIがすごくよく誤解してるんですけど
事前条件聞くと
エラーにする条件でしょって
みんな思っちゃうらしいんですけど
実はそうじゃないんですよ
例えばなんでそうじゃないかっていうと
例えば
HTTPのレストフルなAPIに
ゲットした時に
なかったら404返してほしいじゃないですか
返してほしい
なかったら作るとかってやった時に
ゲットしてない
じゃあポストするみたいな
作ったりすることありますよねって
そうなった時に
404返してこないと困るんですよ
403とか返されたら困る
ってことは
特定の振る舞いを期待していますね
ってことは
事前条件ではないってことなんですね
なるほど
それは事前条件ではなくて
ちゃんとした入力だから通して
404を返さないといけないという振る舞い
ルールなんですね
事後条件なんで
そういう事後条件だということなんですね
なるほど
そう考えると
事前条件って
難しいなって
思っちゃいますね
その範囲って
さっきの例だと
ゲットのリクエスト来た時の
事前条件って何だろうな
と思っちゃいます
でもゲットしか来ない
っていうことなのかもしれないですけど
もしかしたらメソッドに関しては
インターネットには基本的に悪意に
満ちているので
どんな入力で
停止しちゃったり無限ループしちゃったり
困るわけですよ
ドスが成立しちゃいますからね
だから基本的に
インターネットみたいな
悪意のるつぼに公開されているインターフェースは
事前条件は絶対にトゥルーです
トゥルーってのは良すぎ
どんな入力でも受け付ける
ってことです
無いってことですね
無限ループは許さんと
許したらドスになると
いうことになるので
これはウェブAPIのエンドポイントとか
事前条件はトゥルー
どんな入力も良しとする
ということなんですね
理解できました今の話で
普通にウェブサービス作る上で
どういう事前条件
実際の具体的な事前条件になるんだろうな
って考えたんですけど
そんな弾きたいもの無いよな
って思って
てかどんなものが来るか分からないから
どんなものが来るか分からないものに対して
ちゃんと適切なものを
返していくっていうのが事後条件
そういった振る舞いのルールになるはずなので
っていうことですよね
ソート関数に必要な比較の一貫性
逆に言うと事前条件って
どんな時に必要になるのっていうのが
すごく良い例があるので
それを紹介したいと思います
ソートする関数とかってよくありますね
ソート関数
ソートする関数によく順序はこれで付ける
みたいな感じの
順序を決める関数を
ついでに渡してあげることって
よくあるじゃないですか
ありますね
例えばこれはIDっていうプロパティで
ソートするんだとか
あとこれはIDじゃなくて
ネームっていうのでソートするんだとか
いろんなソートするパターンを
決めたい時があって
その時に都度ソート関数を
書くのが面倒くさいので
関数でこれはキーを比較する
IDを比較するとか
こういう風なやつを渡してあげることで
やる
じゃあこのIDって渡す関数が
バグっていって
例えば疑似乱数とかで
やったりとか
常にトゥルーを返すとかって
した時に
何が起こるかっていうのを
考えてみると良いと思います
どうなるんですかね
矛盾する回答を返すわけですね
そうすると
絶対出来上がる
ソートされた後の関数
めちゃくちゃになってますよね
しかも何ならバブルソートとか
みたいな
ちょっとソートのアルゴリズム
どれだというのは
ちょっと分からないですけど
無限ループすることも
あり得ると思います
並び替えていったら
こっちはこっちの方が大きいって
もう一回呼び出したら
こっちっていったら
あれあれってなって
無限ループする
基準がないからってことですよね
そうそうそう
っていう風になるってことがあって
これはつまり
事前条件で
ソートに与える関数っていうのは
一貫していることっていうのが
求められてるわけです
つまり
同じものを与えられたら
ちゃんとイコールだって判定するし
大きいものと小さいものが与えられたら
必ず大きい方を判定して返す
逆のパターン
同じものを与えられて
逆パターンで返したりしたら
ダメってことですね
確かに
ランダムではないってことですね
とか
あとは3つあった時に
片方が片方が大きいって言ってるのに
矛盾する組み合わせを
作ることができる
3つだと
小さい大きいとかして
もう片方が小さい大きいとか
ループするみたいな感じの
関係作ることできますよね
わかりますか
循環してしまう
循環してしまうような順序を
作ることができる
っていう風に作ったりすると
速攻でぶっ壊れる
破綻するわけですよ
とかっていう風な
相当関数の並び替えの部分のルールがあって
それは
ちゃんとした関数を与えた時だけ
相当関数を動くように作りたいわけですよ
この与えられた関数が
よしアサートしてやるぜっつって
アサートできるかって言われたら
できないんですよ
頑張ればできるんですけど
めちゃくちゃコスト高くて
難しいですね
普通にテストしようとすると
どうなる
言語的にサポートされてないと
結構難しいなっていう気がするんです
言語的にサポートされても
どう表現しているのか
わかんないですけど
アサートの中で
全部の組み合わせ試しますか
矛盾ないこと検査しますか
って言われたら
計算量がN以上になるんで
偉いことになるわけですよ
そうなると防衛的プログラミングできない
っていう結論になるんで
もう事前条件そんなものはもう知らん
入れたお前が悪い
っていう風にしたくなるってことなんですね
なるほど
てかそれしかないってことですか
それしかない
事前条件として
そう
っていうことです
ユーザー側がしっかりとした入力を
期待しているよっていうことを
やってるのがその事前条件
事前条件
このルール破ったら
お前は何が起こるかわからない
鼻から悪魔出るかもしれないからな
っていうのが事前条件です
なんだけど
インターネットとか
いろんな人が使う
しかも悪意
もしかしたらセキュリティ的な悪意
満ちた攻撃があるかもしれないものに関しては
事前条件なんてものは書けないので
そうですね
事前条件はないという
全て通すというような形になる
そういうことですね
その中のすごいちっちゃいメソッドとか
関数とかに関しては
事前条件を決めることで
ある範囲において
プロパティベースのテストをしつつ
ルールの性質
っていうのが決めていけるっていうこと
そういうことです
これで合わせ技をすると
少し頭の体操になるんですけど
非決定性と出力に許される範囲
エンドポイントで
さっきのソート関数みたいなの
考えてあげるわけですよ
ポストのところに
ソート関数を与えてあげる
別のペイロードを
ソートして返せって言われた時に
果て事前条件はどうするかと
なるわけですよ
それはぶっ壊せる
エンドポイント
エンドポイントなんで
その場合は
関数を渡さずに
IDとか
そういう絡むだけ指定したい
いいですね
それは一つのやつですね
ちなみに上手い逃げ道もあるんですよ
それは
無限ループはしないアルゴリズムを
選ぶことができると思います
クリックソートとかに
矛盾したやつを与えたとしても
無限ループあったりはしたりはしないんで
そういうふうな
まず絶対無限ループしない
ソート関数を選んでいく
っていうのが一個と
そしてその上で
もし変な
比較関数を入れられちゃった時は
どんな入力が出てきても
許すようにする
っていうふうな書き方をするんです
エリー
なるほど
エラーじゃないんだけど
何が返ってくるかわからないね
こういう事後条件にしちゃうと
実質的に弾くことができます
なるほど
リターンの型を
エリーにするってことですね
そういうことです
リターンの型をエリーにしちゃう
っていうふうに
事後条件を緩和することで
無限ループは許さず
しかし厳密な使用を
考えることができる
これは非決定性と呼ばれているもので
入力出力で許されるパターンって
一種類じゃないんですよ
1つだけじゃない
フィズ×関数が
フィズを返してくるのは
別にいいんですけど
例えば疑似乱数生成器とかって
ネクストを叩くたびに
出てくる数値が変わってくる
わけですよね
はい
こういうのを使用
どう書くか
疑似乱数生成器の使用は
非常に難しいんで
考え方だけなんですけど
1が返ってきても
2が返ってきても
ネクストを押した時には
だから
どれが返ってきても
okだとする
ということにするわけです
つまり
ネクストを叩いた時に
1から
ミントのマックスまで
全部が返ってきて良いとする
エニーですね
まさに
だけど例外にはならないよ
という感じの
使用にするわけですね
なるほど
ちゃんと結果は返ってくるけど
無限ループにはならないし
無限ループにはならない
結果が返ってこないということは
ないという
そうそう
事後条件にする
ということですね
本当は
実際は
例えばずっと1が出続けても
リターン1するようなやつも
そのテスト通っちゃうんで
疑似乱数生成器として
やばいやつも通っちゃうじゃないか
それは難しいところなんですけど
考え方としては
そんな感じということですね
でもこの2つを
もう理解すれば
ほぼ契約による設計は
理解できていると思いますね
なるほど
さっきの疑似乱数の
たぶん
例だからこそなんですけど
きっとあれですね
他の性質としては
返すフォーマットが
統一されているとか
そういったこともありそうです
そういった書き方もできます
UDIDだったりとか
そういうものは
きっちり決まったフォーマットで
返すもの
なんだけど
その中身については
エリーみたいな形になるみたいな
そう考えると
プロパティベーストテスティング
書けますよね
だから区切り文字が
ハイフンが何文字数字が
続いた後に区切り文字が来て
とかっていう風に
フォーマットを見てあげれば
UIDの生成器も
ちゃんとプロパティベーストテスティング
できるわけですよ
あとは
毎回
だいたい違くなるよね
みたいなテスト書くのは
これはちょっと難しいところですね
かぶっちゃうときあるかもしれないから
普通に回してたら
かぶっちゃうことがあるので
かぶることを保証しないテスト
は多分書いちゃいけないんですよ
フレッキになっちゃう
難しいですよね
それは難しくて
統計を使わないといけなくなるんです
100回動かして
だいたいこんなもんだったら
99%正しいと言えるだろう
みたいな言い方をするわけですね
という風に
ちょっと難しいところが出てくるんですけど
でも大雑把な概念としては
確率とか置いておいて
どんな入力に対して
どんな出力が許されるか
それを考えていくっていうのが
基本的に形式手法の考え方の一つであり
それはプロパティベーストテスティング
っていう道に繋がっていたということですね
なるほど
ちなみにちょっとこれは
形式手法というか
実務への接続と次回の定理証明支援系
プロパティベーストテスティングの話になっちゃうかもしれないんですけど
さっき言ってた
ジェネレーターを作って
それに対して
入力が返ってくるわけじゃないですか
対象の関数に対して
ジェネレーターを作って
そこから
入力のインプットが出てくると
そのジェネレーターを作るっていうのは
なんか
各テスティングフレームワークが
サポートしてたりするんですかね
基本的にはサポートしてくれます
イントってやるとイントの適当なやつが来て
列山なんちゃらとか言うと
それで絞り込んでくれるみたいな
とかっていうのが結構あるので
そんな感じで絞り込んでいきます
ある程度有名な
テスティングフレームワークだったら
プロパティベースなテストも
サポートしてたりするってことですね
じゃあそういった機能を使って
ジェネレーター作って
こういうテストをやっていくみたいな
っていう風にすると
テストの行動のところでは
振る舞いだけが抽象的に書かれていて
モーラ的な
若干モーラ的なところですかね
テストができるっていうことなんですね
ユニットテストに関しての
形式手法と形式手法のつながりは
こんな感じでほぼ万全だと思います
すごい理解できました
その考え方を発展させていくと
もっと形式手法の方に入っていく
別の領域の形式手法に
来たりしますね
例えば単体テストじゃなくて
エンドツーエンドテストとかを考えてあげると
また別の理論とかが出てくるんですよ
それは今回は
話し切ることはできないと思うので
拡大はするんですけど
他にも別のモデルとかが出てきて
それでも仕様をうまく表現できるような
数式とかが考えることができる
ということなんですね
今回で
まず第一歩目として
今まで自分たち
一般的なウィブエンジニアとかだったら
普通にやってきた
例えばレールズだったらあるスペック書いて
ユニットテスト書いて
みたいなところから一歩
形式手法にどうやっていくのかなって
すごく謎だったんですけど
それがプロパティベーステスティングで
考え方をちょっとずつ学んでいく
みたいなのは
かなり現実的なところだなと思います
何もわかんないと思うんで
一番最初は
その考え方を徐々に学んでいきつつ
じゃあ形式手法としてどうやって
書いていけばいいのかっていうところの
特化化になるようになりそうだな
って思いましたね
すごい学びになりました
他あったりしますかね
たぶん次の次回のところでは
もうちょっと踏み込んで形式手法
じゃあプロパティベーステスティング
やった上で
やった上でというかちょっと知識がある上で
どうやって形式手法を
やっていくのかみたいなところを聞けたらな
と思うんですけど
次回はその流れでいくと
定理証明支援系っていう
数学の定理とか
無限を扱える子がいて
そのツールを
使ってもっと
今プロパティベーステスティングが
いっぱいの点で指しているだけなんだ
まだメインじゃないんですよ
メインに持ち上げるためには定理証明支援系
っていうのを使うといいので
これを使った話になるんじゃないかな
と思います
無限を扱えるっていうのは
かっこいいんで
かっこいいなと思うので
聞いてみたいなと思います
じゃあ今回はここまでにしたいなと思います
もっと詳しく教えてください
ラジオ略してくわラジでは
スーパーエンジニアである国明さんに
一般エンジニアであるヘントコが
技術的な質問をしていく番組になってます
今後もいろんなこと聞いていけたらな
と思いますのでお聞きのプラットフォームで
高評価やフォローのほうをお願いします
またこんなこと聞いてほしいとかありましたら
コメントいただけると嬉しいです
感想もぜひお待ちしております
それでは今回もありがとうございました
ありがとうございました
