プロパティベーステストといえば、ツールの使い方以前にそもそもプロパティを見つけるのが意外と難しい。そこで Alloy で記述された形式仕様を参考にしてみた。
はじめに
以前の投稿で、Kent Beck の『Test Driven Development: By Example』の Money サンプルを題材にプロパティベーステスト（以下PBT）をやってみたことがある。その時は、Money オブジェクトの性質／法則／プロパティを、テストコーディングしながらその都度考えて進めていた。
そこでも感じたが、PBT と言っても、サンプルデータ生成器の仕組みや用法以前に、そもそもプロパティを見つけること自体が、Money サンプルのようなシンプルなテスト対象ですら意外とむずかしい。思うに、モデルの仕様をその性質（プロパティ）の検証も含めて事前にまとめた上で、その仕様を満たす「最もシンプルな設計」のために TDD を用いるような段取りが良いのではなかろうか。
そこで今回は、モデル検査とテストコーディングを分けて考えて、検査済みの所与のモデルがある前提でそれに基づいてPBTを進めてみたい。モデルの題材は『 抽象によるソフトウェア設計−Alloyではじめる形式手法 (以下、Alloy 本)』第二章の、アドレス帳サンプル を使ってみる。
実践
アドレス帳サンプルは、上述の Alloy本に載っている架空のアドレス帳の仕様で、形式仕様記述言語 Alloy1 で記述されている（Alloy ソース）。本の中では、述語やファクトやアサーション を少しずつ追加しながら、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 コード の assert 文はそのままプロパティと解釈できる。
-
delUndoesAdd:
delは、addによる変更を元に戻す。ただしaddで追加されるNameが、Bookに未登録である場合に限る。 -
addIdempotent: 同じ
NameとTargetの組み合わせでaddを繰り返し適用しても、2回目以降、結果は変わらない。 -
lookupYields:
Bookがすでに保持しているNameについてlookupすると、少なくとも一つのTargetが得られる。
また、ある時点で制約を満たしている Book に対して、どんな操作を適用しても制約が破れないという不変条件も、プロパティと考えられる。つまり任意の操作を任意回適用しても、全て成功して不変条件を維持するか、さもなくば失敗するかのどちらかとなることが期待される。これも PBT でテストしたい。
以下、これらの仕様を Scala コードに起こしてみる。PBT 側は、ScalaCheck を利用する。
型の実装
Targetの階層は素直に 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 のようなライブラリを用いて、以下のように型で表現できるが、ここでは簡単のため単なる String 型とした。
type NonEmptyString = Refined[String, NonEmpty]
sealed trait Target { val value: NonEmptyString }
...
Bookは以下のように定義した。Alias も Group も少なくとも一つの Target に関連づけられるので NonEmptyList を使っている。
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つずつと少数にとどめた。
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つの制約のテストコードを含むため少し複雑になる。
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 はプロダクトコード側で実装した(ソースには含めたが、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]とした。
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 リストからの削除か、または関連付け自体の削除かのいずれかになる。
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は与えられた名前から辿れる住所を全てあつめる再帰コードを書いた。このメソッドは特に気にすべき制約はない。
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
}
プロパティの実装
ここからいよいよ、上で定義したサンプルジェネレータを使ってプロパティを記述する。
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 すると、必ず成功するという意味になる。
property("add succeeds on empty book") =
forAll(genName, genTarget) { (n, t) =>
n == t || Book.empty.add(n, t).isRight
}
最後の 「Book に対してどんな操作列を適用しても、循環参照は生じない」という不変条件の保持のプロパティは以下のようになる。
property("invariants keep") =
forAll(genBook, genOperationList) { (b, os) =>
os.foldLeft(b.asRight[String])(_ flatMap _.apply).forall(Book.isValid)
}
ここで Operation は Book への任意の操作を表す型で、genOperation は Operation のランダムなリストを生成するジェネレータである。
Operation は以下のように実装した。単なる関数でも動くことは動くが、テスト失敗時のメッセージをわかりやすくするためケースクラスとした。
case class Operation(f: Book => ErrorOrBook, display: String) {
def apply(b: Book): ErrorOrBook = f(b)
override def toString: String = display
}
任意の操作列を生成する genOperation は以下のように実装した。
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
- ソース
所感
プロパティ導出とTDDは分けた方が良さげ
-
「はじめに」にも書いたように、整合性の取れた仕様を定義することと、その仕様を満たす最もシンプルな実装を考えることは、やはりかなり異質な作業に思える。
-
ICONIX 界隈で提唱されている DDT：Design-Driven Testing でも、TDD の問題として、入力に用いるユーザーストーリーそのものや、そこから導出するモデル自体は検証されていないことが指摘されていた3。今回試したように、モデルはモデルでテストコーディングとは別に、専用の手法やツールで開発・検証しておくことで、仕様／モデルと TDD の両方の品質を高めることにつながる気がする。ただし形式仕様記述言語やツールを使いこなすスキルは当然必要になる。
-
ごく小さなステップで Red-Green-Refactor を繰り返す TDD の作法には、いまここ に集中するというメンタル面の効果もあったが、プロパティの考察/検証を事前作業として切り出すと TDD に専念して効率を高める上でも効果があると思う。
特殊解から一般解への切り替えが重要
-
JUnit 普及期に日本での先駆者だった故石井勝氏の記事に、コーディングにおける特殊解と一般解の考え方が提示されていて、プロダクトコードでは一般解を扱うのに対して、テストコードではもっぱら特殊解を扱うべきと主張されていた。ただしプロパティベースとなるとテストでも一般解（あるいは一般的に成立する性質）を扱うことになるので、従来の UnitTest/TDD/BDD に慣れた人には意識の切り替えが必要になると思う。
-
同様の事が、SlideShare の『An introduction to property based testing 』でも、"special case" と"property" の違いとして触れられていたが、入門者向けスライドということもあってか、用いられていたプロパティは単純な加法群としての性質だけだった。自明でないプロパティの発見は、やはり難所になると思う。
Discipline も活用できる
- モデルがすでに知られた代数的法則を満たすことが事前にわかっていれば、cats 等の圏論ライブラリに含まれる型クラスのインスタンスを実装することで Discipline を使った検証もできる。以前書いたこの記事では、期間やアクセス権の包含関係を代数で言う半順序(cats の
Partialorder)として捉えて Discipline テストを実装した。またこの記事では、アミダクジが群の公理を満たすことを、同様に Discipline でテストしている。