Dev Study
← 何を作るかを言葉にする
レッスン 2 / 10·約 9 分·第21期 何を作るかを言葉にする

要件は世界に、仕様は機械との境目に書く

リクエストがアプリケーションに届くまで
  1. ブラウザURL入力
  2. DNS名前→IP
  3. ルータ経路選択
  4. ロードバランサ振り分け
  5. Nginx受け口
  6. アプリ処理今ここ
  7. DB保存

このコースの芯は、書かなかったことは消えずに残り、実装した誰かが黙って決める、ということです。今回は依頼文を3種類の文に分け、書かれなかったことがどこに残るかを見ます。

まず結論

要件は、機械をつないだあとの世界がどうあってほしいかを書いた文です。仕様は、それを機械が見られる出来事と起こせる出来事だけで書き直した文です。

両者の隙間は「世界はこうなっている」という前提が埋めます(S, K ⊢ R)。前提は書かなくても消えません。書かなければ、実装した誰かが黙って置きます。

? 読む前に予測

Zave と Jackson が論文で使う、動物園の入口の回転式ゲートの例です。ゲートを制御する機械が、自分で起こせる出来事はどれでしょうか。

当てることが目的ではありません。外した予測ほど記憶に残るので、直感で選んでください。

抽象原理

依頼文を3種類の文に分ける

何を作ってほしいかを伝える文を、このコースでは依頼文と呼びます。ここからは依頼文を3種類の文に分けます。分け方は Pamela Zave と Michael Jackson の論文「Four Dark Corners of Requirements Engineering」から借ります。以下、頁は著者の原稿(1996年7月16日付)のものです。

論文は §6.1(26頁)で、文を2つの「法」に分けます。

A statement (assertion, property) in the indicative mood describes the environment as it would be without or in spite of the machine.

A statement (assertion, property) in the optative mood describes the environment as we would like it to be because of the machine.

どちらも機械ではなく環境(世界)についての文です。違いは、世界が「どうであるか」か「どうあってほしいか」です。この教材では前者を事実の文、後者を願望の文と呼びます。

  • 要件(R): 願望の文。依頼した人が世界に望むこと
  • 仕様(S): 願望の文のうち、直接実装できるもの
  • 前提(K): 事実の文。この開発に関係する、世界についての知識

§5(20頁)は3つの関係を1行に書きます。

S and K together must be sufficient to guarantee that the requirements are satisfied: S, K ⊢ R

仕様と前提が合わさって、要件が満たされることを保証しなければならない。⊢ は、論文が §6.3 で A proof shows that: に続けて同じ式を置くとおり、「左から右が証明できる」と読めます。

同じ §5 は、仕様が何のためにあるかも書いています。

S can be given to a software-development team, which can implement it successfully without recourse to any additional information.

仕様は、ほかの情報に頼らずに実装できるものとして渡されます。教材の言い方では、仕様に書かれていないことは、実装した側が自分の手元で埋めます。

要件・仕様・前提の関係(S, K ⊢ R)
仕様 S機械が見る・起こす出来事だけで書く
前提 K世界はこうなっている(事実の文)
合わせると証明できる
要件 R世界がこうあってほしい(願望の文)
  • ・S だけでは R に届かない。届かない分を K が埋める
  • ・K が書かれていなくても、証明に必要な分は誰かが仮定している
具体実物

動物園の回転式ゲート

論文は §2(4頁)で動物園の入口の回転式ゲートを導入し、§4.1(12〜14頁)で詳しく扱います。出来事は次のとおりです。

回転式ゲートの出来事(§4.1 の記述を表にしたもの)表
出来事 起こす側 機械と共有
pay 支払う 環境 する
push 回転棒を押す 環境 する
enter 通り抜ける 環境 しない
lock / unlock 機械 (機械が起こす)

一番大事な要件は、入場の累計が支払いの累計を超えないこと(G5)です。縛っているのは enter、つまり機械が見ることも起こすこともできない出来事です。この要件はそのままでは仕様になりません。

§5.1(21頁)は、ここを前提で埋めます。回転棒は押すと入場が交互に起き、押すのが先(G1)。ロック中は押せない(G4)。どちらも回転棒の作りについての事実の文です。この2つなどを使って、ロックと解除をいつ起こすかという仕様(G6・G7)から要件を導きます。

同じ節は、見落としやすい前提をもう1つ挙げます。

Finally, we also need domain knowledge giving us a lower bound on the elapsed time between two consecutive pushes (because if pushes can follow each other arbitrarily closely, then the machine must be infinitely fast).

連続して押される間隔に下限がある、という前提です。依頼文にまず書かれない種類の文ですが、無ければ証明が閉じません。

✓ ここまでの確認

回転式ゲートの要件「入場の累計は支払いの累計を超えない」について、論文の組み立てに合うのはどれですか。

抽象原理

前提は、書かなくても消えない

回転式ゲートの前提は、ハードウェアの作りとして実際に成り立っていました。では前提が書かれていないとき、何が起きるでしょうか。

証明に要る前提は、書かれていなくても要ります。仕様どおりに作った人は、要件が満たされるのは前提が正しいときだけという形の正しさしか持っていません。第16期の「テストダブルは、相手についての仮定を書き込んだもの」で見た、モックの緑が言えるのは「仮定が正しければ動く」まで、と同じ形です。違いは、前提が書かれていなければ、その仮定を置いたのが誰かも残らないことです。

具体実物

倉庫の在庫の数

§3.3(10頁)の倉庫では、在庫を管理する機械が入荷と出荷の報告から棚の中身の記録を持ちます。

However, due to theft, breakage, mishandling, update delays, clerical errors, and other misfortunes, it is extremely likely that the quantity actually present in a warehouse bin at a particular time is not exactly the same as the quantity indicated by the machine’s model.

「報告どおりに棚の数が動く」という前提は、ここでは成り立ちません。§5.2(23〜24頁)は、要件を棚の実際の数(quantity-in-bin)で書くと仕様へ落とせない、と述べます。機械が共有する出来事から実際の数を計算する手段がないからです。

Probably the requirements will be stated in terms of expected-quantity-in-bin, which is a defined term representing the best implementable estimate of quantity-in-bin.

前提が成り立たないとき、論文が変えるのは仕様ではなく要件の書き方です。実際の数を願うのをやめ、機械が実装できる見積もりの数で願い直します。

✓ ここまでの確認

倉庫の在庫の例で、「棚にある実際の数」を使って書いた要件について、論文はどう述べていますか。

⇄ 2つを見比べる
具体例 A

回転式ゲート(前提が成り立つ)

入場は機械から見えませんが、押すと入場が交互に起きる・ロック中は押せない、という回転棒の作りが前提として成り立ちます。ロックの規則という仕様から、要件が証明できます。

具体例 B

倉庫の在庫(前提が成り立たない)

棚の実際の数は機械から見えず、盗難や記入の誤りで記録とずれます。報告どおりに棚が動くという前提が無いので、要件を見積もりの数で書き直すことになります。

同じ S, K ⊢ R の形なのに、片方は仕様で済み、片方は要件を書き直しました。分かれ目はどこでしょうか。

機械が見られない出来事や数を、機械が見られるものへつなぐ文がそれぞれ何かを探してください。

この章のまとめ

  • 要件・仕様・前提は、どれも世界についての文。要件と仕様は願望の文、前提は事実の文。
  • 仕様は、機械が見られる出来事と起こせる出来事だけで書いた、直接実装できる願望。
  • S, K ⊢ R(著者の原稿20頁)。仕様だけでは要件に届かず、前提が埋める。
  • 前提は書かなくても消えない。書かなければ、置いた人が記録に残らない。
  • 前提が成り立たないとき、論文は要件の書き方を変える(倉庫の在庫)。
  • §3 冒頭の「インタフェースで観測できるもの」は出発点であって結論ではない。

自分の現場で確かめる

読んだだけでは身につきません。手元の環境で実際に見てみてください。

理解度チェック

読んだ直後は「分かった」と感じやすいものです。実際に解いて確かめてください。

問題 1 / 3正解: 0

この論文の用語で「前提」(domain knowledge / assumption)とはどういう文ですか。

用語集(5語)
要件 (requirement)
機械をつないだ結果、世界がどうあってほしいかを述べた文。論文の記号は R。機械が見られない出来事について書いてよい。
仕様 (specification)
願望を述べた文のうち、直接実装できるもの。論文の記号は S。機械と共有する出来事と、機械が起こす出来事だけで書く。
前提 (domain knowledge / assumption)
機械があってもなくても世界がどうであるかを述べた文。論文の記号は K。仕様から要件を導くときの橋になる。
願望の文 / 事実の文 (optative / indicative)
論文の中心の対。文法の「法」から取った語で、前者は世界がどうあってほしいか、後者は世界がどうであるかを述べる。
共有される出来事 (shared action)
環境の中で起き、機械も関わる出来事。回転式ゲートでは支払いと押すは共有、入場は共有されない。