Alloyによる形式仕様をプロパティベースでテストしてみた

プロパティベーステストといえば、ツールの使い方以前にそもそもプロパティを見つけるのが意外と難しい。そこで Alloy で記述された形式仕様を参考にしてみた。

## はじめに

[以前の投稿](https://qiita.com/yasuabe2613/items/e13c76a1469bd8176bcf)で、Kent Beck の『[Test Driven Development: By Example](https://www.amazon.co.jp/Test-Driven-Development-Addison-Wesley-Signature/dp/0321146530)』の Money サンプルを題材にプロパティベーステスト（以下**PBT**）をやってみたことがある。その時は、Money オブジェクトの性質／法則／プロパティを、テストコーディングしながらその都度考えて進めていた。

そこでも感じたが、PBT と言っても、サンプルデータ生成器の仕組みや用法以前に、そもそもプロパティを見つけること自体が、Money サンプルのようなシンプルなテスト対象ですら意外とむずかしい。思うに、モデルの仕様をその性質（プロパティ）の検証も含めて事前にまとめた上で、その仕様を満たす「最もシンプルな設計」のために TDD を用いるような段取りが良いのではなかろうか。

そこで今回は、モデル検査とテストコーディングを分けて考えて、検査済みの所与のモデルがある前提でそれに基づいてPBTを進めてみたい。モデルの題材は『 [抽象によるソフトウェア設計−Alloyではじめる形式手法](http://alloytools.org/book.html) (以下、Alloy 本)』第二章の、**アドレス帳サンプル** を使ってみる。

## 実践
アドレス帳サンプルは、上述の Alloy本に載っている架空のアドレス帳の仕様で、形式仕様記述言語 Alloy[^1] で記述されている（[Alloy ソース](https://github.com/AlloyTools/org.alloytools.alloy/blob/master/org.alloytools.alloy.extra/extra/models/book/chapter2/addressBook3d.als)）。本の中では、**述語**や**ファクト**や**アサーション** を少しずつ追加しながら、GUI の Alloy ツールを使って反例を発見したりしつつ、矛盾や漏れのない最終版仕様を定義しているが、この辺りのノリは TDD によく似たところがあって面白い。

以下のコーディングではこのアドレス帳仕様を Scala で実装してみる。

### アドレス帳の仕様

Alloy による形式仕様から型、制約、操作、プロパティを読み取って、ふつうの日本語で箇条書きすると、以下のようになる。

#### 型について
- ターゲット `Target` は、住所 `Addr` か、名前 `Name` かのいずれかである。
- `Name` は、別名 `Alias`か、グループ `Group` かのいずれかである。
- アドレス帳 `Book`は、`Name`のセット `names` を持つ。
- `Book`は、`names` の各要素を一つ以上の`Target`に関連付ける、写像 `addr` を持つ。

```
Target
　├─ Addr
　└─ Name
　　　　├─ Alias // Book 内で一つの Target に関連付けられる
　　　　└─ Group // Book 内で一つ以上の Target に関連付けられる
```

#### 制約について
- `addr` の循環参照は禁止。つまり `names` のある要素に `addr` を再帰的に適用しても、それ自身にたどり着いてはいけない。
- `Alias` に関連付けられる `Target` は高々一つまで。

#### 操作について
- `add` は、`Name` と `Target` の関連付けを `Book` に追加する。
- `del` は、`Name` と `Target` の関連付けを `Book` から削除する。
- `lookup` は、指定の `Name` から到達可能な `Addr` の集合を得る。

#### プロパティについて
[Alloy コード](https://github.com/AlloyTools/org.alloytools.alloy/blob/master/org.alloytools.alloy.extra/extra/models/book/chapter2/addressBook3d.als) の `assert` 文はそのままプロパティと解釈できる。

- **delUndoesAdd**: `del` は、`add` による変更を元に戻す。ただし `add` で追加される `Name` が、`Book` に未登録である場合に限る。
- **addIdempotent**: 同じ `Name` と `Target` の組み合わせで `add` を繰り返し適用しても、2回目以降、結果は変わらない。
- **lookupYields**: `Book` がすでに保持している `Name` について `lookup` すると、少なくとも一つの `Target` が得られる。

また、ある時点で制約を満たしている `Book` に対して、どんな操作を適用しても制約が破れないという不変条件も、プロパティと考えられる。つまり任意の操作を任意回適用しても、全て成功して不変条件を維持するか、さもなくば失敗するかのどちらかとなることが期待される。これも PBT でテストしたい。

以下、これらの仕様を Scala コードに起こしてみる。PBT 側は、ScalaCheck を利用する。

### 型の実装
`Target`の階層は素直に Scala に置き換えた。

```scala
sealed trait Target { val value: String }
sealed trait Name  extends Target
case class Addr(value:  String) extends Target
case class Alias(value: String) extends Name
case class Group(value: String) extends Name
```
仕様にはないが値を文字列として持たせている。若干余談になるが、通常こうした値に付与される非空文字という制約は、[refined](https://github.com/fthomas/refined) のようなライブラリを用いて、以下のように**型で表現**できるが、ここでは簡単のため単なる `String` 型とした。

```scala
type NonEmptyString = Refined[String, NonEmpty]
sealed trait Target { val value: NonEmptyString }
...
```

`Book`は以下のように定義した。`Alias` も `Group` も少なくとも一つの `Target` に関連づけられるので `NonEmptyList` を使っている。

```scala
type SomeTargets = NonEmptyList[Target]
type BookAssoc   = Map[Name, SomeTargets]
...
case class Book(assoc: BookAssoc) {
  def names:                 Set[Name]           = assoc.keySet
  def addresses(name: Name): Option[SomeTargets] = assoc.get(name)
  ...
```

この実装では、`Name` から `Target` への関連付けをもっぱら `Book` が管理しているが、設計の選択肢として、`Alias` や `Group` 自身が `Target` への関連付けを持つ方式も考えられる。例えば `case class Alias(name: Name, target: Target)` や `case class Group(name: Name, targets: SomeTargets)` といった実装もできたが、ここでは Alloy のコードになるべく近い形で表現した。

### 制約の実装
上述の通りアドレス帳仕様には、循環参照がないことと、`Alias` は唯一の `Target` を指すという制約=不変条件がある。
これらについて、「どんな操作を `Book` に施しても制約を破らない」というプロダクトコード側と、「条件を満たさないサンプルオブジェクトを生成しない」というジェネレータ側の、両面で実装する必要がある。前者については操作の実装として後述するとして、まずジェネレータについて解説する。

#### ターゲット階層のジェネレーター
ターゲットの階層のジェネレータは、型の階層をそのまま反映する形で実装できる。Alloy 本でいう**小スコープ仮説**[^2]を採用して、住所、エイリアス、グループのサンプル数をそれぞれ3つずつと少数にとどめた。

```scala
val genAddr:  Gen[Addr]  = Gen.oneOf("A1", "A2", "A3") map Addr
val genAlias: Gen[Alias] = Gen.oneOf("N1", "N2", "N3") map Alias
val genGroup: Gen[Group] = Gen.oneOf("G1", "G2", "G3") map Group

val genName:   Gen[Name]   = Gen.oneOf(genAlias, genGroup)
val genTarget: Gen[Target] = Gen.oneOf(genAddr, genAlias, genGroup)

def genSomeTargets(max: Int): Gen[SomeTargets] = for {
  m <- Gen.chooseNum(1, max)
  h <- genTarget
  t <- Gen.listOfN(m - 1, genTarget)
} yield NonEmptyList(h, t)
```

#### アドレス帳のジェネレータ
`Book` オブジェクトのサンプルジェネレータは、先述の2つの制約のテストコードを含むため少し複雑になる。

```scala
val genBook: Gen[Book] = {
  val genAssoc = for {
    len    <- Gen.chooseNum(0, 3)
    names  <- Gen.listOfN(len, genName)
    tuples <- names.map {
      case a: Alias => genSomeTargets(1).map((a, _)) // Aliasを複数の Targetに関連づけない
      case g: Group => genSomeTargets(3).map((g, _))
    }.sequence[Gen, (Name, SomeTargets)]
  } yield tuples.toMap
  genAssoc retryUntil Book.isValidMap map Book.apply // 循環参照を持つBookを作らない
}
```
0〜3個の`Name`のそれぞれに、1〜3個のターゲットのリストを関連付けて、`Book`サンプルを生成している。循環参照を検出するメソッド `isValidMap` はプロダクトコード側で実装した([ソース](https://gist.github.com/yasuabe/b49a7073c186201bd6f99afd28a17694)には含めたが、PBTとはあまり関係がないので割愛)。

### 操作の実装
`add`、`del`、`lookup`の実装では、関連付けの編集に加えて上記の制約も考慮する。

#### add メソッド
追加の挙動は、`n: Name` が `Alias`の場合は単純な「置換または追加」、`Group` の場合は既存の関連付けがもしあれば、その `Target`リストへの `t: Target` の追加、なければ `t` への関連の新規追加となる。

ただし、現状の `Book` が持っている `Name -> Target` の関連付けと、入力として得た `Name`と`Target` の組み合わせ次第では、循環参照が生じる場合もある。このため結果の型として、失敗を表す `String` と、成功時の新規 `Book` のいずれにもなりうることを表して、`type ErrorOrBook = Either[String, Book]`とした。

```scala
  def add(n: Name, t: Target): ErrorOrBook = {
    val targets = n match {
      case _: Alias => one(t)
      case _: Group => assoc.get(n).fold(one(t))(ts => (t :: ts).distinct)
    }
    val updated = assoc.updated(n, targets)
    Either.cond(isValidMap(updated), Book(updated), "circular reference")
  }
```
ちなみにこのサンプルコードを書いていたとき、最初 `Group` の case 句の `distinct` を書き忘れていたが、追加のべき等性のプロパティ `addIdempotent` がテスト失敗したので、すぐに気づけた。

#### del メソッド
削除の挙動は、`n: Name` が `Alias` の場合には常に関連付けの削除、`Group`の場合は既存の `Target`リストの状態によって `Target` リストからの削除か、または関連付け自体の削除かのいずれかになる。

```scala
  def del(n: Name, t: Target): Book = Book {
    n match {
      case _: Alias => assoc - n
      case _: Group => assoc.get(n).fold(assoc) {
        _ filter (_ != t) match {
          case Nil => assoc - n
          case th :: tt => assoc.updated(n, NonEmptyList(th, tt))
        }
      }
    }
  }
```

#### lookup メソッド
`lookup`は与えられた名前から辿れる住所を全てあつめる再帰コードを書いた。このメソッドは特に気にすべき制約はない。

```scala
  def lookup(n: Name): Set[Addr] = assoc.get(n).fold(Set.empty[Addr]) {
    _.map {
      case addr: Addr => Set(addr)
      case name: Name => lookup(name)
    }.toList.toSet.flatten
  }
```

### プロパティの実装
ここからいよいよ、上で定義したサンプルジェネレータを使ってプロパティを記述する。

```scala
  property("del undoes add") =
    forAll(genBook, genName, genTarget) { (b, n, t) =>
      b.addresses(n).nonEmpty || b.add(n, t).map(_.del(n, t)).forall(b == _)
    }
  property("add idempotent") =
    forAll(genBook, genName, genTarget) { (b0, n, t) =>
      (for {
        b1 <- b0.add(n, t)
        b2 <- b1.add(n, t)
      } yield b1 == b2).forall(identity)
    }
  property("lookup yields") =
    forAll(genBook) { b =>
      b.names.forall(b.addresses(_).nonEmpty)
    }
```
Alloy の `assert` を、ほぼそのまま Scala コードに書き下したが、`add` の失敗を考慮している点が少し違っていて、"*del undoes add*" と"*add idempotent*" は、メソッド`add`が成功したときのみプロパティの成立を確かめている。

ただし、これでは `add` が常に `Left` を返すような実装ミスの場合にも、プロパティが成立してしまうので、以下の様な補助的なプロパティを付け加えた。空の `Book` に任意の `n: Name`, `t: Target` の組(ただし n != t)を `add` すると、必ず成功するという意味になる。

```scala
  property("add succeeds on empty book") =
    forAll(genName, genTarget) { (n, t) =>
      n == t || Book.empty.add(n, t).isRight
    }
```

最後の 「`Book` に対してどんな操作列を適用しても、循環参照は生じない」という不変条件の保持のプロパティは以下のようになる。

```scala
  property("invariants keep") =
    forAll(genBook, genOperationList) { (b, os) =>
      os.foldLeft(b.asRight[String])(_ flatMap _.apply).forall(Book.isValid)
    }
```
ここで `Operation` は `Book` への任意の操作を表す型で、`genOperation` は `Operation` のランダムなリストを生成するジェネレータである。

`Operation` は以下のように実装した。単なる関数でも動くことは動くが、テスト失敗時のメッセージをわかりやすくするためケースクラスとした。

```scala
  case class Operation(f: Book => ErrorOrBook, display: String) {
    def apply(b: Book): ErrorOrBook = f(b)
    override def toString: String   = display
  }
```
任意の操作列を生成する `genOperation` は以下のように実装した。

```scala
  val genOperationList: Gen[List[Operation]] = {
    val genOperation = for {
      n <- genName
      t <- genTarget
      o <- Gen.oneOf(
        Operation(b => b.add(n, t),        s"add($n, $t)"),
        Operation(b => Right(b.del(n, t)), s"del($n, $t)"))
    } yield o
    Gen.chooseNum(0, 5) flatMap { m => Gen.listOfN(m, genOperation) }
  }
```
`del` は値域が `Either` ではなく生の `Book` なので、`Right` にラップしてから `Operation` コンストラクタに与えている。

これで、制約が表現できた。

### 結果
下記のようにテストが成功する。

```
+ Book Spec.del undoes add: OK, passed 100 tests.
+ Book Spec.add idempotent: OK, passed 100 tests.
+ Book Spec.lookup yields: OK, passed 100 tests.
+ Book Spec.add succeeds for empty book: OK, passed 100 tests.
+ Book Spec.add yields no circular reference: OK, passed 100 tests.

Process finished with exit code 0
```

- cats のバージョンは 1.5.0、scalacheckのバージョンは 1.13.5
- [ソース](https://gist.github.com/yasuabe/b49a7073c186201bd6f99afd28a17694)

## 所感
#### プロパティ導出とTDDは分けた方が良さげ
- 「はじめに」にも書いたように、整合性の取れた仕様を定義することと、その仕様を満たす最もシンプルな実装を考えることは、やはりかなり異質な作業に思える。

- ICONIX 界隈で提唱されている DDT：Design-Driven Testing でも、TDD の問題として、入力に用いるユーザーストーリーそのものや、そこから導出するモデル自体は検証されていないことが指摘されていた[^3]。今回試したように、モデルはモデルでテストコーディングとは別に、専用の手法やツールで開発・検証しておくことで、仕様／モデルと TDD の両方の品質を高めることにつながる気がする。ただし形式仕様記述言語やツールを使いこなすスキルは当然必要になる。

- ごく小さなステップで Red-Green-Refactor を繰り返す TDD の作法には、**いまここ** に集中するというメンタル面の効果もあったが、プロパティの考察/検証を事前作業として切り出すと TDD に専念して効率を高める上でも効果があると思う。

#### 特殊解から一般解への切り替えが重要
- JUnit 普及期に日本での先駆者だった[故石井勝氏の記事](http://objectclub.jp/community/memorial/homepage3.nifty.com/masarl/article/junit/programming-style-guide.html)に、コーディングにおける特殊解と一般解の考え方が提示されていて、プロダクトコードでは**一般解**を扱うのに対して、テストコードではもっぱら**特殊解**を扱うべきと主張されていた。ただしプロパティベースとなるとテストでも一般解（あるいは一般的に成立する性質）を扱うことになるので、従来の UnitTest/TDD/BDD に慣れた人には意識の切り替えが必要になると思う。

- 同様の事が、SlideShare の『[An introduction to property based testing ](https://www.slideshare.net/ScottWlaschin/an-introduction-to-property-based-testing)』でも、"special case" と"property" の違いとして触れられていたが、入門者向けスライドということもあってか、用いられていたプロパティは単純な加法群としての性質だけだった。自明でないプロパティの発見は、やはり難所になると思う。

#### Discipline も活用できる
- モデルがすでに知られた代数的法則を満たすことが事前にわかっていれば、cats 等の圏論ライブラリに含まれる型クラスのインスタンスを実装することで Discipline を使った検証もできる。以前書いた[この記事](https://qiita.com/yasuabe2613/items/fd9a8961b0301d4d64f5)では、期間やアクセス権の包含関係を代数で言う**半順序**(cats の`Partialorder`)として捉えて Discipline テストを実装した。また[この記事](https://qiita.com/yasuabe2613/private/c5e95e9e36079ec14ee2)では、アミダクジが群の公理を満たすことを、同様に Discipline でテストしている。


[^1]: Alloy とは形式仕様記述言語の一つで、GUI の Alloyツールとして一式提供されているもの。
[^2]: サンプルデータの定義域中のごく小さな範囲で、実用的にはほとんどの反例や不具合を捕捉できるという仮説。
[^3]: XP から AcceptanceTest を残したまま UnitTest だけ切り離したことの弊害として。