5000円ちょうどの買い物
形式手法とは、プログラムの決まりを、機械に全部の場合で調べさせる方法です。テストが見逃す誤りを、反例という1つの具体例にして見せてくれます。
ネットショップの送料無料は「合計5000円以上」と決まっています。プログラムが「5000円より大きい」と書いていると、5000円ちょうどの客だけが送料を取られます。3000円と8000円でテストしても、この誤りは見つかりません。
このレッスンのゴール
メモ
テストが示すことと、証明が示すことを、言い分けられる。
重要な言葉
| ことば | いみ | れい |
|---|---|---|
| テスト | 入力を1つ選び、結果を見ること | 3000円で試す |
| 証明 | 全部の場合で成り立つと、示すこと | |
| 反例 | 主張が間違いだと示す、1つの場合 | n = 5000 |
| 境界値 | 決まりが切り替わる、境目の値 | 5000 |
| 形式手法 | 決まりを機械に調べさせる方法 | |
| 全数調査 | 全部の場合を、1つずつ試すこと |
学生が入力するセルは、このプレビューでは空白です。
テストは試した場合しか見ない
テストは、入力を選んで、結果が正しいかを見る方法です。広く使われていますが、見るのは試した場合だけです。
決まりが「合計5000円以上」なら、境目は5000円です。プログラムの比べ方が1つずれると、その1点だけが間違います。そこを試さなければ、テストは全部通ります。
決まりとプログラムの比較
| 合計（円） | 決まり: 5000円以上 | プログラム: 5000円より大きい | 一致する？ |
|---|---|---|---|
| 3000 | 送料無料でない | 送料無料でない | はい |
| 4999 | 送料無料でない | 送料無料でない | はい |
| 5000 | 送料無料 | 送料無料でない | いいえ |
| 5001 | 送料無料 | 送料無料 | はい |
| 8000 | 送料無料 | 送料無料 | はい |
学生が入力するセルは、このプレビューでは空白です。
ラボの端末で確かめる
このレッスンはラボ formal-lab で進めます。Z3、SPIN、TLA+、Alloy の入った、自分専用の Ubuntu のマシンです。レッスンのバーから起動すると、Run ボタンのコマンドが、その端末に打ち込まれます。
まず、5000円ちょうどで2つの比べ方を試します。次に、3000円と8000円で試します。
ちょうど5000円を比べる
python3 -c "print(5000 > 5000, 5000 >= 5000)"ここでは表示のみで、実行されません。無料アカウントを作成すると、実行ボタンで自分のラボのターミナルに入力できます。
3000円と8000円を比べる
python3 -c "print(3000 > 5000, 3000 >= 5000, 8000 > 5000, 8000 >= 5000)"ここでは表示のみで、実行されません。無料アカウントを作成すると、実行ボタンで自分のラボのターミナルに入力できます。
範囲が小さければ全部を試せる
金額を0円から20000円までに限れば、20001通りです。機械なら一瞬で全部を試せます。これが全数調査です。
次のコマンドは、決まりとプログラムの答えが食い違う金額を数えます。「5000円以上」と「5000円より大きい」を、20001通りの全部で比べます。
食い違う金額を数える
python3 -c "print(len([n for n in range(0, 20001) if (n > 5000) != (n >= 5000)]))"ここでは表示のみで、実行されません。無料アカウントを作成すると、実行ボタンで自分のラボのターミナルに入力できます。
無限の場合もソルバーが調べる
整数は無限にあるので、全部を1つずつ試せません。ソルバーは、条件を式として扱い、全部の整数についての答えを出します。
Z3 に、整数 n で、2つの比べ方の答えが食い違うものがあるかを尋ねます。あれば sat と、その例を出します。なければ unsat と答えます。式の書き方は、次のレッスンで学びます。
Z3に全部の整数を尋ねる
echo '(declare-const n Int) (assert (not (= (> n 5000) (>= n 5000)))) (check-sat) (get-model)' | z3 -inここでは表示のみで、実行されません。無料アカウントを作成すると、実行ボタンで自分のラボのターミナルに入力できます。
よくある間違い
注意
テストが全部通ったから、プログラムは正しい、と思いがちです。通ったのは、試した場合だけです。試さなかった場合のことは、何も分かりません。「全部の場合で正しい」と言えるのは、証明だけです。
テストと証明の違い
| 見るところ | テスト | 証明（形式手法） |
|---|---|---|
| 見る範囲 | 試した場合だけ | 全部の場合 |
| 成功したとき | 試した場合は正しい | 決まりがいつも成り立つ |
| 失敗したとき | 誤りがあると分かる | 反例が1つ出る |
| 弱いところ | 試さない場合を見逃す | 決まりの書き方が悪いと無意味 |
学生が入力するセルは、このプレビューでは空白です。
証明は決まりの書き方しだい
証明が保証するのは、書いた決まりが成り立つことだけです。決まりが間違っていれば、証明も間違った答えを保証します。
たとえば「送料無料は5000円より大きいとき」と決まりに書けば、プログラムは証明を通ります。だから、決まりは人が読んで確かめます。反例は、決まりを直す手がかりにもなります。
さらに挑戦: 境目を探す
課題が通ったら、fare_by_code の70を69に変えて、もう一度 Run しましょう。見逃した場合の数は、どう変わるでしょうか。
次に、境目の前後を必ず試すテストのリストを自分で作ります。年齢64、65、69、70を入れると、いくつの誤りを見つけられるか考えましょう。