テスト要件を抽出するために、Alloy が役立たないだろうか？
要件の自動抽出やテスト仕様書の生成、さらには自動テストといった高望みをすると大変になるので、さほど手間をかけずにひとりでもできる範囲で考えよう。
その範囲でツールを使うだけなら、チームに断る必要も広める必要もなく、好きなボールペンを使うのと同じレベルのはずだ。

あるべき姿を理解する

設計・開発そのものに関わらずテストを専門で行ってくれる方々（大変お世話になっております）は、まず「あるべき姿」を理解して、「本当にそうなっているか」をどう確かめるか考える（のだろう）。
＃本当は設計から関わっていただく方がいいのだが、それはまた別の話

不備があるかもしれない仕様書（と言うのは控えめな表現で、実際には大量の不備や不整合、記述の観点不足があるのが普通だろう）が入手できるはずなので、それとヒアリングを元にあるべき姿を組み立てていく。
その作業は、実のところ上流設計そのものだ。
設計時点との違いは、いったんモノができている以上、入手できる情報の確度が高いことくらいだろう。しかしその情報も、テストしてみないと疑わしい。

理解するためにモデルを描く

十分でない情報からあるべき姿（モデル）を組み立てるのは、設計の最初の段階で行うべきことであり、モデル発見器 Alloy の得意分野でもある。
残念ながら開発側の実情では最初に十分モデルを練れることは少なく、開発中に新たにわかった要件を組み込むため歪んだモデルが実装されている場合も多い。
スキルレベルや理解度の異なる担当者がたくさん関わることで、グダグダな設計・実装になっているかもしれない。
しかし、テストをする人にそんな事情は関係ない。もちろんユーザーにとっても。
なので、あるべき姿を理解するため、怪しい挙動が起きる可能性のある部分を発見するため、モデルを書いてみよう。
仕様書に書いてあることと、書いていないことへの理解が深まるはずだ。

ログイン処理を理解する

今回の記事は、テストフレームをつくってみたにインスパイアされて書いている。
ざっと読ませていただいたところでいったん内容は忘れ、「さてログイン処理って何だろう」というところに立ち戻ってモデル化してみる。

1. サービスを利用する

まず、何者かによって提供されるサービスと、それを利用する者がいる。

sig Service {}
sig User {
    using: set Service
}

run { some using }

実行すると、Alloy は図として例を示してくれる。

うん、同時にいくつかのサービスを利用することや、複数ユーザーの同時利用もあるよね。
ひとつのドキュメントを複数人が同時に編集できるサービスもある。

2. ログインって？

サービス提供者が何らかの理由でユーザーを識別するための仕組みだ。
識別することで会員制を実現したり、その人にひもづけたドキュメントやサービス設定を利用できるようにできる。
利用者名+パスワードとか、機器登録や指紋認証とか、識別する手段は色々考えられるが具体的なことは割愛する。

sig Service {
    knownId: set Id
}
sig User {
    id: Id,
    using: set Service
}
enum Id { U1,U2,U3,U4 }

run { #using > 1 }

IDを照合しないと意味ないよね、というところまででここは良しとして先に進もう。

3. ハード面からも考える

ハード面で考えると、サーバー、クライアント、ネットワークも抽出できるだろう。

enum Quality { Good, Poor }
abstract sig Node {
    net: lone Quality
}
sig Server extends Node {}
sig Client extends Node {
    connect: lone Server
}

run { some connect }

どちらかの回線品質が悪いときに何が起こるだろう？
悪いどころか切れてしまった場合は、正しく終われるだろうか？

4. ハードとソフトを組み合わせる

ハードとソフトの両方がないと始まらない。組み合わせよう。
サービスはサーバー上で提供され、ユーザーはクライアントデバイスを使ってサーバーに接続する。

// Hard
enum Quality { Good, Poor }
abstract sig Node {
    net: lone Quality
}
sig Server extends Node {
    service: set Service
}
sig Client extends Node {
    connect: lone Server
}

// Soft
sig Service {
    knownId: set Id
}
sig User {
    id: Id,
    device: Client,
    using: set Service
}
enum Id { U1,U2,U3,U4 }

run { (some using) && (some connect) } for 4

うん、device→connect→service とつながった先のサービスしか使いようがないよね。

5. 条件を追加する

そろそろサービスを使うために必要な条件を追加しよう。
以下をfactに書いた。

Client と Server はネットでつながっていなければならない
device→connect→service とつながっているサービスしか利用できない
サービスに登録されているユーザーしか利用できない

// Hard
enum Quality { Good, Poor }
abstract sig Node {
    net: lone Quality
}
sig Server extends Node {
    service: set Service
}
sig Client extends Node {
    connect: lone Server
}

// Soft
sig Service {
    knownId: set Id
}
sig User {
    id: Id,
    device: Client,
    using: set Service
}
enum Id { U1,U2,U3,U4 }

fact {
    some connect.univ.net   // Clientがネットにつながっている
    some univ.connect.net   // Serverがネットにつながっている
    using in device.connect.service // 使えるサービスは device→connect→service とつながっているものだけ
    all user:User | all service:user.using {  // ユーザーがサービスを使っているならば、
        user.id in service.knownId            // そのIDはサービスに登録されている
    }
}
run { (some using) && (some connect) } for 4

それらしい図が出るようになった。

[Next]ボタンで次々と図を出してもらいながら、その図が何を物語るのか考えることで、どうあるべきか理解が深まるだろう。
気が付いたことはメモしておくといい。

6. モデルを見てわかること

例えば上の図を見て、こんなことが想像できるだろう。

Service0 へのログインで同時に Service2 へもログインすべきか
Service2 へもログインしていたとしたら、Service0 のログアウトで Service2 からもログアウトすべきか、それで不都合はないか
サービス利用中に登録解除されることはないか

など。そういう図を見て思うことは、テスト要件に入る可能性がある。

また、Alloy コードの記述も境界条件の有力候補になる。

set, no, lone, one, some, all といった数に関する指定（濃度, 多重度, 限量子）
fact に書いた条件・制限

この先もあるが

ここに挙げたモデルには「ログイン処理」そのものは書いていない。ログインすることで何ができるようになるのかを考えるためのモデルだ。
ログインする処理を書いて、事前・事後で何が起きるべきか起きないべきかを考えることも Alloy でできる。
そうすれば「Service1 にログイン済みの User1 は、さらに Service1 にログインできるべきか」「PCとスマホではどうか」「ログイン処理中に回線が切れたら」などを考えられるだろう。

処理を考える上で、Alloy では書くのが難しい同時性や到達可能性の問題もある。
「複数人が同時にログインしようとしたら」「ひとりが同時に Service1 にログインしようとしたら」「Client1 で Service1 にログインしようとしながら Client2 で Service2 からログアウトしようとしたら」
そういうところまで踏み込むなら、Alloy 以外にも手を出すべきだろう。

また、「操作に対するリアクションは＊秒以内にあるか」「ログイン処理は＊秒以内に完了もしくは失敗するか」「その結果は＊秒以内にユーザーに伝わるか」といった品質要件もあるだろう。

しかしそこまで書くと手間がかかるし、モデルに書かなくてもいいのではないか？
図を見て想像できる範囲でおそらく「あるべき姿を理解する」目的は８割がた達成できているのではないか？
下手をするとすでに開発側の１担当者を上回る理解度に達しているかもしれない。

費用対効果を考えると、ツールを使うのはこのくらいで抑えて、あとは他の方法と組み合わせるのが良いのではないかと考える。

終わりに

今回はおおむね既知の「ログイン処理」を題材にしているので割とすんなり書けたわけだが、実際にはまだ何者かわからないソフト（ハード）を理解しようとモデリングする。
そして前述の開発側都合でグダグダな仕様書と実装が回ってくる恐れがある。
仕様書の詳細になるべく引きずられず、どんな意味を実現しようとしているかをモデル化するように心がけたい。
そうしてできたモデルの知識を持って仕様書を見直すと、きっと思ったのと違う仕様や言い回しが見つかるだろう。
そういうところは、テストにあたっても要注意だ。

＃どちらかと言うと、同じ方の発想や気づきはなぜ足りないのだろう？に近い記事になったような気がします。仕様から要求を考え直して、目に見える図にすることで発想しやすくするという。

Alloyで考えよう : テストするために仕様を理解したい