I tested the Alloy format specification on a property-based basis.
Speaking of property-based testing, it is surprisingly difficult to find properties in the first place before using the tool. So I consulted the format specification written in Alloy.
At first
In a previous post, I tried property-based testing (PBT) based on the Money sample from Kent Beck's Test Driven Development: By Example. At that time, I was thinking about the nature/laws/properties of the Money object each time while test-coding.
As I felt there, even with PBT, it is surprisingly difficult to find properties in the first place, even for simple test subjects such as Money samples, even before the mechanism and usage of the sample data generator. In my opinion, it would be better to summarize the specifications of the model in advance, including the verification of its properties (properties), and then use TDD for the "simplest design" that satisfies the specifications.
Therefore, this time, I would like to consider model inspection and test coding separately, and proceed with PBT based on the premise that there is a given model that has been inspected. For the subject of the model, try using the address book sample in Chapter 2 of "Software Design by Abstraction: A Formal Method Starting with Alloy (hereinafter referred to as "Alloy Book").
practice
The address book sample is a fictitious address book specification from the Alloy book described above, written in the format specification description language Alloy1 (Alloy source). In the book, we define a final specification without contradictions or omissions, adding predicates, facts, and assertions little by little, and using the GUI's Alloy tool to find counterexamples, but the nori around here is interesting because it is very similar to TDD.
The following coding will implement this address book specification in Scala.
Address Book Specifications
Reading types, constraints, operations, and properties from the Alloy format specification and bulleting them out in ordinary Japanese looks like this:
About Types
- The target
Target
is either an addressAddr
or a nameName
. Name
is either an aliasAlias
or a groupGroup
.- An address book
Book
has a setnames
ofName
. - A
Book
has a mapaddr
that associates each element of thenames
with one or moreTarget
.
Target
├─ Addr
└─ Name
├─ Alias // Book 内で一つの Target に関連付けられる
└─ Group // Book 内で一つ以上の Target に関連付けられる
About Constraints
- Circular references to
addr
are prohibited. In other words, if you recursively applyaddr
to an element ofnames
, you should not get to itself. Alias
can be associated with no more than oneTarget
.
About Operations
add
addsName
andTarget
associations to theBook
.del
removes the association betweenName
andTarget
from theBook
.- The
lookup
gets a set of reachableAddr
from the specifiedName
.
About Properties
The assert
statement in Alloy code can be interpreted as a property as is.
-
delUndoesAdd:
del
undo changes made byadd
. However, only if theName
added in theadd
is not registered in theBook
. -
addIdempotent: Repeated application of
add
with the sameName
andTarget
combination does not change the result after the second time. -
lookupYields:
lookup
aboutName
already held byBook
yields at least oneTarget
.
In addition, an invariant condition that the constraint cannot be broken no matter what operation is applied to a Book
that satisfies the constraint at a certain point in time is also considered a property. That is, even if any operation is applied arbitrarily, it is expected that it will either succeed and maintain the invariant, or else it will fail. I want to test this with PBT as well.
Let's transcribe these specifications into Scala code below. The PBT side uses ScalaCheck.
Type Implementation
The Target
hierarchy was simply replaced with 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
Although it is not in the specification, it has a value as a string. As a slight aside, the non-empty character constraints normally affixed to these values can be expressed in terms of types using libraries like refined, but for simplicity we have made them just String
types.
type NonEmptyString = Refined[String, NonEmpty]
sealed trait Target { val value: NonEmptyString }
...
Book
defined as follows: Both Alias
and Group
are associated with at least one Target
, so NonEmptyList
is used.
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)
...
In this implementation, the association from Name
to Target
is managed exclusively by Book
, but a possible design choice is to have the Alias
or Group
itself have an association to the Target
. For example, implementations such as case class Alias(name: Name, target: Target)
and case class Group(name: Name, targets: SomeTargets)
could have been made, but here they were expressed as close as possible to Alloy code.
Implementing Constraints
As mentioned above, the address book specification has the constraint = invariant that there are no circular references and that Alias
refers to only Target
.
These need to be implemented on both sides of the product code side, which says "No matter what operation is performed on the Book
, the constraint is not broken" and the generator side, which "does not generate sample objects that do not satisfy the conditions". As for the former, as will be described later as an implementation of the operation, the generator will be described first.
Target hierarchy generator
The generator of the target hierarchy can be implemented in a way that reflects the hierarchy of the type as it is. Alloy adopted the small-scope hypothesis2 in the book and kept the number of addresses, aliases, and groups to three samples.
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)
address book generator
The sample generator of Book
objects is a bit more complicated because it includes test code for the two constraints described above.
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を作らない
}
A list of 1 to 3 targets is associated with each of the 0-3 Name
to generate Book
samples. The method isValidMap
for detecting circular references was implemented in the product code (included in the source, but omitted because it has little to do with PBT).
Implementing Operations
add
, del
, and lookup
implementations also consider the above constraints in addition to editing associations.
add method
The additional behavior is a simple "replace or append" if the n: Name
is Alias
, an existing association in the case of Group
, adding a t: Target
to the list of Target
existing associations, if any, or adding a new association to the t
if not.
However, depending on the Name -> Target
association that the current Book
has and the combination of the Name
and Target
obtained as inputs, circular references may occur. For this reason, the result type is type ErrorOrBook = Either[String, Book]
, indicating that it can be either a String
representing failure or a new Book
at the time of success.
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")
}
By the way, when I was writing this sample code, I forgot to write the distinct
in the case clause of the Group
at first, but I noticed it immediately because the additional idempotent property addIdempotent
failed the test.
del method
The delete behavior is always to delete the association if the n: Name
is Alias
, or to remove the association from the Target
list or the association itself, depending on the state of the existing Target
list in the case of Group
.
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 Method
lookup
wrote a recursive code that would collect all the addresses that could be traced from a given name. This method has no particular constraints to worry about.
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
}
Implementing Properties
From here, it is time to describe the properties using the sample generator defined above.
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)
}
I wrote the Alloy assert
almost verbatim into Scala code, but the difference is that it takes into account the failure of the add
, and "del undoes add" and "add idempotent" verify that the property is valid only when the method add
succeeds.
However, in this case, even in the case of an implementation mistake in which add
always returns Left
, the property is established, so the following auxiliary properties have been added. add
any n: Name
, t: Target
tuple (but n != t) in an empty Book
means that you will always succeed.
property("add succeeds on empty book") =
forAll(genName, genTarget) { (n, t) =>
n == t || Book.empty.add(n, t).isRight
}
The property of the last invariant hold, "No matter what operation sequence is applied to the Book
, no circular reference occurs" is as follows:
property("invariants keep") =
forAll(genBook, genOperationList) { (b, os) =>
os.foldLeft(b.asRight[String])(_ flatMap _.apply).forall(Book.isValid)
}
where Operation
is a type that represents any operation on Book
, and genOperation
is a generator that generates a random list of Operation
.
Operation
implemented as follows: Even a simple function can work, but I made it a case class to make the message at the time of test failure easier to understand.
case class Operation(f: Book => ErrorOrBook, display: String) {
def apply(b: Book): ErrorOrBook = f(b)
override def toString: String = display
}
The genOperation
that generates arbitrary operation sequences is implemented as follows:
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) }
}
Since del
is raw Book
instead of Either
, it wraps in Right
and then gives it to the Operation
constructor.
Now the constraints can be expressed.
result
The test succeeds as shown below.
+ 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 version is 1.5.0, scalacheck version is 1.13.5
- source
impressions
Property derivation and TDD should be separated
As I wrote in the Introduction, defining a consistent specification and thinking of the simplest implementation that meets that specification still seem like a rather alien task.
DDT: Design-driven testing, which has been proposed in the ICONIX area, also pointed out that the problem with TDD is that the user story itself used for input and the model derived from it have not been verified3 。 As I tried this time, I feel that by developing and verifying models with dedicated methods and tools separately from test coding with models, it will lead to improving the quality of both specifications/models and TDD. However, it is naturally necessary to have the skills to master formal specification description languages and tools.
The TDD method, which repeats Red-Green-Refactor in very small steps, had the mental effect of concentrating on the here and now , but I think that cutting out the consideration/verification of properties as a preliminary task is also effective in concentrating on TDD and increasing efficiency.
Switching from special solutions to general solutions is important
An article by the late Masaru Ishii, who was a pioneer in Japan during the JUnit period, presents the concept of special solutions and general solutions in coding, and while product code deals with general solutions, test code deals exclusively with special solutions. It was argued that it should be handled. However, when it comes to property bases, even tests deal with general solutions (or properties that generally hold), so I think that people who are accustomed to conventional UnitTest/TDD/BDD will need to switch their mindset.
A similar thing was mentioned in SlideShare's An introduction to property based testing as the difference between "special case" and "property", but perhaps because it was an entry-level slide, the only properties used were those of a simple additive group. I think that finding properties that are not obvious will be a difficult task.
Discipline can also be used
- If you know in advance that a model satisfies a known algebraic law, you can also verify it using Discipline by implementing an instance of a type class included in a category theory library such as cats. In a previous article, I implemented the Discipline test by thinking of the duration and access rights inclusion relationships as semi-order (
Partialorder
of cats) in algebra. The article also tests in Discipline that Amidakuji satisfies the axioms of a group as well.
-
Alloy is one of the formal specification description languages, provided as a set of Alloy tools for GUI. ↩
-
The hypothesis that within a very small range of sample data ranges, most counterexamples and defects can be captured in practice. ↩
-
As a disadvantage of detaching only UnitTest while leaving AcceptanceTest from XP. ↩