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 Alloy¹ (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 address Addr or a name Name.
• Name is either an alias Alias or a group Group.
• An address book Book has a set names of Name.
• A Book has a map addr that associates each element of the names with one or more Target.

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

About Constraints

• Circular references to addr are prohibited. In other words, if you recursively apply addr to an element of names, you should not get to itself.
• Alias can be associated with no more than one Target.

About Operations

• add adds Name and Target associations to the Book.
• del removes the association between Name and Target from the Book.
• The lookup gets a set of reachable Addr from the specified Name.

About Properties

The assert statement in Alloy code can be interpreted as a property as is.

• delUndoesAdd: del undo changes made by add. However, only if the Name added in the add is not registered in the Book.
• addIdempotent: Repeated application of add with the same Name and Target combination does not change the result after the second time.
• lookupYields: lookup about Name already held by Book yields at least one Target.

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.