反例とは何か

現場から上がってくる報告で、いちばん困るのはこれです。

「たまに止まる」

再現手順はありません。ログはありますが、止まった前後が見えるだけです。装置は目の前で普通に動いている。何十回動かしても止まらない。それでも報告は上がってきていて、対策は書かなければならない。

このとき本当に欲しいのは、原因の名前ではありません。その順番です。何が起きて、次に何が起きたら、あの状態になるのか。それさえ分かれば、あとは大した仕事ではありません。

私たちが慣れているエラーは、経路を教えない

現場でエラーが手元に届く形は、だいたい二種類です。

ひとつは現場報告。「たまに止まる」「稀にアラームが出る」。事象は分かるが、経路が分からない。

もうひとつはテストの失敗。「assertion failed」。どの条件が、どの行で破れたかは分かる。しかし、なぜそこに到達したのかは分からない。テストが与えた入力から先は、自分で追うことになります。

どちらも、壊れた結果を教えてくれます。壊れるまでの道は教えてくれません。

設計を検証するというのは、ここが違います。設計に「扉が開いている間、可動部は動作していない」と書いて、それが本当に成り立つかを機械的に調べさせる。成り立たない場合に返ってくるのは、「成り立ちません」という一行ではありません。成り立たなくなる事象列が、順番に並んで返ってきます。これを反例と呼びます。

反例は、自動生成された再現手順です。

反例を一本、歩いてみる

教科書的な装置を考えます。搬送アームと Z軸、それに扉のインターロックを持つ、ありふれた構成です。

安全条件はひとつ。

扉が開いている間、可動部は動作していない。

これを検証にかけると、たとえばこういう列が返ってきます。

1. 初期状態: 扉=閉, Z軸=上昇端, 搬送=待機, インターロック=解除
2. 操作者が扉開ボタンを押す        → 扉=開放中(機械的に動き始める)
3. 上位が搬送開始を指令            → 搬送=動作中
4. 扉センサが開放を検知            → 扉=開, インターロック要求を発行
5. インターロックが停止を要求      → 搬送=減速中

違反: ステップ 4 の時点で 扉=開 かつ 搬送=動作中
      安全条件「扉が開いている間、可動部は動作していない」が破れる

読むべきところは、ステップ 2 と 4 の間です。

扉開ボタンが押されてから、扉センサが開放を検知するまでに、隙があります。設計上は「扉開 → インターロック → 停止」と一本に見えていました。しかし実際には、ボタンと検知は別の事象で、その間に上位からの指令が入り込める。反例は、その隙を通る手順を、具体的に一本示しています。

ここから先は、いつもの設計作業です。ボタン押下の時点でインターロック要求を出すのか。上位の搬送開始指令に扉状態の条件を付けるのか。停止に要する時間を含めて安全条件を書き直すのか。どれを選ぶかは設計判断ですが、何を議論すべきかは、もう手元にあります。

「設計の問題か、実装の問題か」が、消える

装置のデバッグで高くつくのは、直す時間ではありません。どこが悪いのかを突き止める時間です。そして、その最初の一歩はいつもこれです ——

「これは設計の問題か、実装の問題か」

反例は、この問いを飛ばします。反例が示しているのは実装のバグではありません。設計が、その手順を許しているという事実です。コードを一行も見ない段階で、実機に触れないまま、それが確定します。

「どこかがおかしい」と「この順番で起きるとおかしい」の差が、デバッグ何週間分です。

レビューできる、ということ

反例のいちばん実務的な性質は、たぶんこれです。人間が読めます。

返ってくるのは、証明の内部でも、ツール固有の記号でもありません。設計で使っている語彙 —— 信号、状態、遷移 —— が並んだ列です。だから設計レビューにそのまま持ち込めます。スクリーンに出して、上から順になぞって、「ここで搬送が動き始める」「ここで検知が来る」と説明できる。

これは「ツールが問題があると言っています、信じてください」とは、まったく別の話です。反例は主張ではなく、手順です。手順なら、その場にいる全員で確かめられます。反例が妥当かどうかを判断するのに、検証の中身を理解する必要はありません。装置を理解していれば足ります。

そして、一度手に入れた事象列は、そのままテストケースになります。実機ができたら、この順で操作して確かめればいい。修正したあとの回帰シナリオとしても残せます。反例は、その場限りの指摘ではなく、資産として残る形をしています。

反例が、設計ではなくモデルを指すとき

正直に書いておきます。

反例を読んで「この手順は実機では起きない」と思うことがあります。よくあります。そして、その直感はしばしば正しい。

原因はだいたい二つです。

ひとつは、安全条件の書き方が違っていた。「扉が開いている間」の「開」を、ボタン押下のつもりで書いたのか、センサ検知のつもりで書いたのか。曖昧なまま書くと、意図しない読み方の列が出てきます。

もうひとつは、モデルが緩すぎた。実機では機械的に同時に起こり得ない二つの事象を、モデル上は独立に起こせるようにしてしまった。すると、現実には存在しない手順が反例として出てきます。

どちらも失敗ではありません。どちらの場合も、自分が設計を正確に書けていなかったことが分かった、ということです。「開とは何か」を曖昧にしたまま何年も回してきた設計書は、珍しくありません。反例は、その曖昧さを具体的な手順の形で突きつけてきます。

ただし、これも正直に言っておく必要があります。反例を読むのは技能です。 最初のうちは、設計の誤りとモデルの誤りの区別に時間がかかります。数本読めば慣れます。慣れるまでは、慣れるまでの時間がかかります。

有限の列と、終わらないループ

補足を一つ。

反例の形は、確かめたい性質によって二種類あります。

「悪いことが起きない」タイプの条件 —— 扉が開いている間に可動部が動かない、二軸が同時に干渉領域へ入らない —— が破れるときは、悪い状態に至る有限の事象列が返ってきます。上の例がこれです。

「良いことがいつか起きる」タイプの条件 —— 原点復帰を指令したら必ず原点に着く、非常停止からは必ず復帰できる —— が破れるときは、その良いことが起きないまま回り続けるループが返ってきます。二つの状態を行き来して、いつまでも原点に着かない。装置で言えば、ハングです。

どちらも読み方は同じです。上から順に、事象を追う。

次に読むもの

反例が返ってくるのは、テストとは違う調べ方をしているからです。テストは選んだ手順を試し、設計検証は手順の全体を調べる。その違いは テストと形式手法は、何が違うのか で扱います。

そもそも、なぜ装置ソフトウェアでは実機に頼るしかなかったのか。その構造は なぜ装置ソフトウェアは、V字モデルの右半分を実行できないのか にあります。