Verifying Models with Alloy Before Property-Based Testing

To be precise, I should write "checking," but in this article, I will basically use the more familiar term "verification."

Property-based testing is attracting a lot of attention lately. At the end of last year, I was reading "Property-Based Testing in Erlang, Elixir, and PropEr".

In Chapter 10 of this book, an example of a book lending system is used as a case study for property-based testing. Before implementing the tests, they first model the state and list all operations on the system (page 260). Here is an excerpt from one of them:

• Expected result for "adding a book not yet registered in the system" is "success"

Similarly, "operation content" and "expected result" are written for other operations as well. While reading these specifications, a few things caught my attention:

• How does the result of one operation affect other operations?
• Is the result of one operation consistent with the results of other operations?

These must be understood by reading the specification yourself. While we can rely on AI these days, setting that aside, we humans can't just skip understanding the specs. As the specifications grow, the cost of this work increases. For various personal reasons, it has become quite difficult for me to remember or keep track of specifications, so this is a serious issue for me, not self-deprecation or a joke.

One reason for the high cost is that specifications are written in natural language (Japanese). Natural language is ambiguous, so no matter how logically a text is written, it becomes difficult to completely grasp the author's intention. On top of that, verifying it against other specifications must be done manually. As mentioned before, while we can rely on AI now, if what the AI outputs is also natural language, the problem remains the same.

Verifying the Model?

What would make things easier? Considering my situation:

• A strict, text-based notation suitable for describing specifications
• A feature that verifies things on behalf of humans

Having these would be great. In particular, a verification feature could reduce the cost of thinking in natural language.

A verification feature is a function that lets a computer verify questions such as whether there are contradictions in the specifications or how to interpret specifications in specific situations. However, AI is not a reliable means because it can make mistakes.

That's why I want to try formally verifiable formal specification languages. It sounds grand and difficult, but it's actually a surprisingly familiar concept.

"Formal" refers to methods or procedures that follow specific, strict rules. A familiar example is regular expressions, which are a formal language. They represent patterns that match text according to specific rules. As you may have noticed, programming languages are also formal languages.

A "specification description language" is, as the name suggests, a language for describing specifications. A familiar example is UML (it also has strict notation, so it's also a formal language). Since UML doesn't have an automatic verification feature, it doesn't suit my needs.

As a language that meets these criteria, I would like to try Alloy this time. Alloy is a specification language for model checking, and an analysis tool is distributed with it.

Model checking is based on mathematical theory (mathematical logic), but Alloy can be used reasonably well without being conscious of mathematics (I don't know much about it at all). I hope that by reading this article, you will feel even a little more familiar with Alloy and model checking.

The Model to Verify

In this article, we will implement code to check the model of a book lending system using Alloy. This model is the one treated in Chapter 10 of "Property-Based Testing in Practice."
However, it's not a problem if you don't have "Property-Based Testing in Practice" at hand. This model is small, so it is self-contained within the article.

Installing Alloy

Alloy can be downloaded from the official website. On macOS, you can also install it via Homebrew with the following command (the desktop app will be installed in /Applications).

brew install alloy

The Alloy application comes with a simple editor, but the VSCode extension is also recommended. This extension displays an execution button above runnable code, and the execution results are shown within the VSCode window.

Defining Objects

First, we define the objects at the core of the model. Launch Alloy (not necessary if using the VSCode plugin) and create a file with the following content.

Bookstore.als:

sig Title {}

sig Author {}

sig Isbn {}

sig Book {
    title: Title,
    author: Author,
    isbn: Isbn,
}

sig NAME {...} is called a signature, a syntax for defining new types. It is similar to defining classes or structs in programming languages. Models defined with signatures are called atoms.

Signatures can define multiple fields. This is also roughly the same as fields or properties in programming languages. Title, Author, and Isbn have no fields (it is fine if they are empty if there are no fields to define). Book has three fields: title, author, and isbn. The right side of the : represents the type of the field.

String Types Do Not Exist

The signatures for Title, Author, and Isbn have no fields. In an actual implementation, these fields would likely be of string type, so you might be tempted to write the type of each field in Book as String. However, there are no string types in Alloy.

A string type is a concrete data type that depends on the programming language. Depending on the language, there might not even be a dedicated string type. For example, Erlang, used in "Property-Based Testing in Practice," does not have a string type. There is a string type for convenience, but it is just an alias for a "list of character codes (integers)." Alloy represents models using abstract data types rather than concrete ones.

To express things abstractly, let's think about more concrete data. Even if you implement titles, author names, and ISBNs collectively as string types, not every character will be usable. If a title or author name contains Hokkaido Itaiji (Hokkaido variant characters), Unicode without unassigned mappings wouldn't be able to handle them. There are countless other characters that cannot be represented in Unicode. Similarly, for ISBNs, any string other than 10 or 13-digit numbers would be invalid.

To give these slightly more accurate types, a title could be thought of as a "list (ordered set) of 'characters usable in a title'." The same applies to author names and ISBNs. If defined in Alloy, it might look like this:

sig TitleCharacter {}

sig Title {
    contents: set TitleCharacter,
}

Now the string type is no longer necessary. Alternatively, you could define a signature representing a string and inherit from it (define subtypes). By doing the following, you can prepare a common type String for Title, Author, and Isbn.

sig String {}
sig Title extends String {}
sig Author extends String {}
sig Isbn extends String {}

It has become an abstract signature.

However, we won't handle such detailed types in this model because they aren't necessary. In a system dealing with official documents or ancient texts, there might be benefits to defining more detailed types.

Defining the System

Next, we define the signature of the system that manages book inventory. Lines starting with // are comments.

sig System {
    // Registered books
    catalog: set Book,

    // Inventory
    copies: catalog -> Int
}

The System signature has two fields: catalog, representing registered books, and copies, representing inventory. Both field types may look unfamiliar.

First is set Book. set is a keyword representing multiplicity, and set indicates an unordered collection. It's like a Bag in programming languages. (To handle ordered sets, you use the util/ordering module, which is omitted in this article.)

Next is catalog -> Int. catalog refers to the catalog field, and -> represents a mapping of types. It is similar to a Map or Dictionary in programming languages.

However, note that this catalog merely represents the type and is not a definition indicating the relationship with the contents of catalog. For example, it does not mean that a Book included in catalog is necessarily included in copies.

Representing this signature in pseudocode would look like this:

sig System {
    catalog: Bag<Book>,
    copies: Map<Book, Int>
}

Defining the "Add Book" Operation

We have now defined the object types. However, just defining types doesn't allow us to do anything yet. From here, we will define the elements for verifying the model.

Model verification requires constraints. Constraints are conditions or rules that the model must satisfy. This is also true for the definition of operations representing dynamic behavior. To distinguish the term "operation," from here on, we will refer to operations on the book lending system as "system operations" and operations in Alloy simply as "operations."

First, let's define the "add book" operation. To quote the system operation and its expected results:

• Expected result for "adding a book not yet registered in the system" is "success"
• Expected result for "adding a book already registered in the system" is "failure"

To represent an operation with these rules, we will define a predicate this time. A predicate verifies whether specific conditions or rules are met. It takes arguments and handles the verification results as boolean values, making it similar to a function, but it is not a means for processing data. In programming terms, it's like an assert() that throws an exception.

Since Alloy has no concrete data type to represent success or failure, we will determine success or failure based on the presence or absence of state changes this time. If successful, there is a state change where a book is added to the system; if it fails, the state of the system does not change at all.

Now, let's define the predicate addBook representing the "add book" operation as follows:

pred addBook [sys: System, sys": System, b: Book] {
    b not in sys.catalog => sys".catalog = sys.catalog + b
}

You might be taken aback by the unfamiliar syntax. Let's look at it one by one.

pred is the keyword that begins a predicate definition. The predicate name addBook is specified after pred.

The following [...] are the arguments of the predicate. Each argument is declared in the form argument_name: type. You can also use " in argument names. The " has no special meaning; sys" is a normal argument name.

There are two System arguments, but in addBook, the first argument is used to represent the "before state change (pre-state)" and the second for the "after state change (post-state)." The reason there is an "after state change," which would normally be a future result, is that operations in Alloy are declarative rather than procedural.

In general programming languages, you specify the procedures for processing data to obtain an expected result. In Alloy, you directly specify the expected result. Let's examine the content of the predicate:

b not in sys.catalog => sys".catalog = sys.catalog + b

This expression can be split into a left side and a right side. The left side is b not in sys.catalog, and the right side is sys".catalog = sys.catalog + b.

A not in B on the left side is an operator expressing that A is not contained in the set of objects B. b not in sys.catalog means "the catalog in the pre-state does not contain b."

The => operator connecting the two sides represents the logical relationship between them. I'll discuss this later.

Before explaining that, let's move to the right side sys".catalog = sys.catalog + b. sys.catalog + b adds b to the set of Book. This represents the registration of a book.

= is an equality operator. In programming terms, it is like == and is not an assignment. Since sys" on the left represents the "after state change," sys".catalog = sys.catalog + b expresses that "the catalog in the post-state is equal to the catalog in the pre-state with b added."

The => Operator

The => operator mentioned earlier is called implication, and it means "if the left side is true, then the right side is also true." While it is similar to an if statement in programming languages, they are not equivalent because the result when the left side is false is different.

When the left side of => is false, the overall result is true regardless of whether the right side is true or false. The table below shows this:

A	B	A => B
True	True	True
True	False	False
False	True	True
False	False	True

If the result of a predicate is true, the verification result is considered to be without problems. In the case of the left side b not in sys.catalog, it would be false if the book is already in the system, but the overall result of addBook would be true. Also, if the left side is false, the right side is not evaluated, so sys".catalog = sys.catalog + b is not executed. Summarizing each result into a table gives the following:

b not in sys.catalog	sys".catalog = sys.catalog + b	addBook	System State
Book is not registered	Add the book	True	Changes
Book is not registered	Cannot add book	False	Does not change
Book is already registered	(Not evaluated)	True	Does not change
Book is already registered	(Not evaluated)	True	Does not change

The state of the system only changes if "the book is not registered and was successfully added." In the system's specifications, "the book is already registered" is considered a failure, so it might feel strange that the result of addBook is true when the book is already registered. However, a "failure" in system operations is not a bug; it is part of the specification.

Verification only fails if "the book is not registered but could not be added." The addition process, sys".catalog = sys.catalog + b, looks like a simple operation that shouldn't cause issues, but it's not guaranteed to always hold true (as will be explained later).

Therefore, if the verification results are clear, if "the book is not registered" is true, then "the book can be added" must always be true. This also means that a scenario where "the book is not registered but cannot be added" would be inconsistent with other constraints or is undefined in the specification.

Few programming languages have an implication operator (maybe just VBA?), so it might be hard to digest at first, but for the beginning, it shouldn't cause much trouble if you use it with the same feeling as an if statement.

Incidentally, the => operator can also be represented by the implies keyword. => is the shorthand version, and implies is the long-form version. Since both => and implies can be combined with else, implies is sometimes used to match the appearance when using else.

Verifying the Model

Now, let's verify the "add book" operation using addBook. I'll quote the content and expected results of this operation again:

• Expected result for "adding a book not yet registered in the system" is "success"
• Expected result for "adding a book already registered in the system" is "failure"

As mentioned in the previous section, the failure in this case is not a bug but part of the specification. This time, we will compare the "state change" caused by addBook. The verification contents are as follows:

• Expected for "adding a book not yet registered in the system": "state change exists" and "book is added after state change"
• Expected for "adding a book already registered in the system": "no state change"

Verification is performed using assertion and check commands. You define the verification content with an assertion and perform the verification based on that assertion with the check command.

This time, we will prepare two separate assertions representing the success and failure of adding a book.

• addNewBookSuccess: Adds an unregistered book. State change exists.
• addExistingBookFail: Adds a registered book. No state change.

The definitions are shown below. Since both are almost identical, I will present them together:

assert addNewBookSuccess {
    all sys, sys": System, b: Book |
        b not in sys.catalog
        implies addBook[sys, sys", b]
        implies b in sys".catalog
}

assert addExistingBookFail {
    all sys, sys": System, b: Book |
        b in sys.catalog
    	    implies addBook[sys, sys", b]
        implies b in sys".catalog
}

An assertion is defined by starting with assert, followed by the constraints within {...}. In the above assertions, everything from all to the end of the block is a single expression. This is also an unfamiliar syntax, so let's break it down.

This expression defines constraints for combinations of (bound) variables sys, sys", and b, separated by the | operator. The leading all is one of the quantifiers representing multiplicity, expressing constraints for all instances. During execution, instances with all sorts of possible contents are generated, and it's verified whether all combinations satisfy the constraints.

I'll also list other quantifiers. Quantifiers are used in other elements like signatures as well:

• lone: 0 or 1
• one: 1
• some: 1 or more
• no: 0

sys" is used to represent the "after state change" of the system, as mentioned in addBook.

b [not] in sys.catalog implies ... implies is also a single expression. b [not] in sys.catalog is the same expression defined in addBook. implies is the redundant notation for =>. It seems implies is often used in assertions, perhaps for better readability.

If b [not] in sys.catalog is true, then addBook[sys, sys", b] is also true, and the whole expression becomes true. As mentioned in the section on =>, there is no situation where only one of the three expressions is true. Either "all are true" or "all are false."

addBook[sys, sys", b] specifies the predicate addBook as a constraint. If the book is unregistered, the book is added to sys".catalog via addBook. Finally, b [not] in sys".catalog specifies whether the book has been added to sys".catalog.

The final b in sys".catalog is the same in both assertions. In addExistingBookFail, it guarantees that if the addition fails because the book was already registered, there is no change in the contents of catalog. It might seem obvious, but it is important to build up these "obvious" points. Meticulous definitions help prevent unexpected errors and contradictions.

After defining the assertions, describe the contents of the check commands to be executed:

check addNewBookSuccess for 5

check addExistingBookFail for 5

The check command performs verification based on an assertion. The numeric value following for is called the scope, and it specifies the breadth (range) of cases to consider. We'll discuss scope later, so for now, let's just run it.

In the desktop version, select "Check addNewBookSuccess for 5" from the Execute menu. In VSCode, you can run it by pressing the Execute button above the line for the check command.

Desktop version

VSCode

When executed, the verification results are displayed on the right side of the window.

Desktop version

VSCode

If "No counterexample found. Assertion may be valid." is displayed, there are no problems with the verification results. A state where all constraints are true is called valid.

A counterexample refers to a case where the constraints do not hold. Conversely, a case where constraints hold is called an example. Since no counterexample was found this time, the verification result is valid.

Instances and Scope

How are assertions verified? Alloy generates objects for the signatures and uses them as concrete examples for verification. These objects are called instances.

Instances are generated based on constraints for all possible relationships (states and configurations) that should be investigated. The main relationships are shown below:

• Multiplicity
  Exhausts the multiplicities of types.

  For example, if the type of the Book.title field were lone Title, a Book would have 0 or 1 Title. In this case, Book instances with 0 Title and those with 1 Title would be generated.

  Collection types with infinite elements, like set, generate instances with a certain number of elements. For set Int, for example, instances with integers from 0 to 10 might be generated. The range of generated integers depends on the constraints and scope.

• Signatures and Fields
  Signature objects are generated with combinations of multiplicities that fields can take.

  For example, if the multiplicities of both the Book.title field and the Book.author field are lone, there are 4 combinations of title and author: (0, 0), (0, 1), (1, 0), and (1, 1). These four types of Book instances will be generated.

  If the multiplicity of all fields is 1, or if fields are empty, the signature object will consist of only one instance.

• Relationships between Signatures
  Exhausts possible relationships between signatures.

  For example, there may be cases where different Book instances share the same Title. In addBook, there is no constraint that the value of Book.title must not be shared with other instances.

  Also, there is no constraint that a Book added to System.catalog must necessarily be included in the keys of System.copied. Conversely, there is no constraint that a Book included in the keys of copied must be in catalog. Therefore, combinations of instances will be generated, such as "containing the same Book in both catalog and copied," "catalog containing a Book not in copied," and "copied containing a Book not in catalog."

However, the more signatures and fields there are, the more dramatically the combinations of relationships increase. The scope determines the range of those combinations. Smaller scopes mean fewer instances, while larger scopes dramatically increase the number of instances. More instances make it easier to find counterexamples, but if the scope is too broad, execution will never finish.

Here are the pros and cons of scope ranges:

Range	Pros	Cons
Small	Instances are simple and easy to understand	Counterexamples are harder to find
Large	Counterexamples are easier to find	Instances are complex and hard to understand

With a larger scope, combinations of relationships become more diverse, so if a counterexample is found, the content of the instance might be an unexpected case, making debugging difficult. Therefore, it is recommended to start with a small scope and gradually increase it. Ultimately, a scope of 10 seems to be sufficient to cover most cases.

Facts

Constraints that always hold, unlike predicates which apply to specific situations, are called facts. A fact is applied both before and after a predicate is executed, so if there is a fact that contradicts the state before addBook is executed, no instance will be generated. If there is a fact that contradicts the state after execution, it will be considered that a counterexample was found.

Before defining a fact, let's look at the instances that are actually generated. Add the following command:

run addBook

The run command searches for instances that satisfy the specified constraints. Like check, you can execute it from the Execute menu. When executed, a window like the following will open (in VSCode, click the "Instance found. Predicate is consistent." link after execution):

Execution result of run addBook

This diagram shows the relationships between instances. Rectangles represent individual instances, and arrows represent the relationships between them. Integers enclosed in rectangles are also "integer instances." In this diagram, integer instances from "-8" to "7" are generated.

There are 2 instances of System and a total of 16 instances of Book (not explicitly shown in the diagram, but included in copies). The Book on the right end is the argument for addBook. This instance is referenced by both System instances and is included in both catalog and copies. There are 15 Books included in copies that are not included in catalog. One Author instance, Author0, is independent and does not belong to any Book, which we'll consider fine since you might register just an author's name.

Was the result more cluttered and different from what you expected? The definition of addBook only adds a Book to the System, with no other constraints. We didn't define that there is only one instance of System, nor that the same Book shouldn't be shared between different systems. We didn't define that inventory should be 0 or greater, nor that an Author instance must belong to a Book.

Alloy generates diverse instances considering all kinds of relationships. If there are few constraints, the relationships between instances expand, and if the scope is large, it exhausts those relationships boundlessly. While it's fine if the relationships you want to cover are within the intended range, this model includes many unintended relationships.

Therefore, we define facts to remove unnecessary relationships and add constraints that we want to always hold. First, we'll limit the number of System instances to one:

fact singletonSystem {
    #System = 1
}

The relationship between System and Book instances has decreased, making it a bit cleaner. Next, we add a fact to ensure the inventory count is always 0 or greater. Since copies is a field managed by System, it's easiest to add the fact to the System signature (facts can also be written within a signature):

sig System {
    catalog: set Book,
    copies: catalog -> Int
} {
   all b: Book | copies[b] >= 0
}

Setting the inventory count to 0 or more

Instances where the inventory count was negative have disappeared. The number of copies has also changed, but since the example found by run is just one of many, it's not an issue.

In this way, by defining facts, you can apply constraints outside of predicates and assertions. For now, we've set the inventory count to 0 or more, but depending on the system, negative numbers might be allowed, or there might be an upper limit to the inventory. This is a specification that was overlooked until we checked the instances. It's a minor detail, but whether you think it's good to discover oversights before implementation or feel the cost-performance of such a discovery is poor is the trade-off of model checking.

Defining "Adding Book Inventory"

Next, we define and verify the predicate for "adding book inventory." To quote the content and expected results of this operation:

• Expected result for "adding one copy of a book already registered in the system" is "success (inventory increases by 1 immediately)"
• Expected result for "adding one copy of a book not yet registered in the system" is "error"

Again, we'll represent success and error through state changes. "Success" will be "inventory increases by 1," and "error" will be "inventory does not increase":

pred addCopy [sys, sys": System, b: Book] {
    b in sys.catalog =>
        sys".copies = sys.copies + (b -> (sys.copies[b] + 1))
}

The unfamiliar notation here is likely (b -> (sys.copies[b] + 1)) (parentheses can be omitted; they are included here to clearly distinguish the expressions). -> represents a relationship, just like in the type definition of System.copies. It's like a key and a value. The -> within the expression also represents a key-value pair.

sys.copies[b] accesses the value of sys.copies with the key b. Since the type of the value in copies is Int, sys.copies[b] represents getting the inventory count. Therefore, b -> (sys.copies[b] + 1) is a pair where the inventory count of b is increased by 1. It declares that the result of adding this new pair to sys.copies is equal to the sys".copies after the state change.

The left side b in sys.catalog will be false if the book is not registered, but as mentioned in the previous section, since => is an implication operator, the entire expression remains true even if the left side is false. The expression only becomes false if the left side is true and the right side is false. This happens if "the book is registered but the inventory could not be added."

We define the assertions as follows:

// Add one copy of a book that is already registered
assert addCopyExistingSuccess {
    all sys, sys": System, b: Book | 
        b in sys.catalog 
        implies addCopy[sys, sys", b] 
        implies sys".copies[b] = sys.copies[b] + 1
}

check addCopyExistingSuccess for 5

// Attempt to add one copy of a book that is not yet registered
assert addCopyNewFail {
    all sys, sys": System, b: Book | 
        b not in sys.catalog 
        implies addCopy[sys, sys", b]
        implies sys".copies[b] = sys.copies[b]
}

check addCopyNewFail for 5

The last line compares the inventory count after executing addCopy with the state before execution. It is fine if "the book is registered and inventory increased by 1" or "the book is not registered and inventory did not change."

Finding Counterexamples

All the assertions so far were definitions that hold true. This time, let's intentionally try to find a counterexample. By actively thinking about counterexamples, you can identify unexpected behaviors or design errors. The same applies to unit testing.

...However, I couldn't quite figure out an easy-to-understand way to write a counterexample. I'll just write down the behavior when a counterexample is found.

When a counterexample is found through the execution of run or check, a message "Counterexample found. Assertion may be invalid." is displayed with a link on the right side of the window. Clicking it opens a window showing the instance that serves as the counterexample. Here is an example:

An instance of a found counterexample

Functions

Search operations do not change the state whether they succeed or fail. Therefore, combining functions and assertions is more suitable than trying to handle it with predicates.

We define a function to search by ISBN as follows:

fun findBookByIsbn [sys: System, i: Isbn]: set Book {
    {b: sys.catalog | b.isbn = i}
}

findBookByIsbn takes a system and an ISBN and returns a set of books (set Book). | does not mean "or"; it is the same | we've seen so far. {...} represents a set. It is similar to list comprehensions.

b: sys.catalog treats all elements of Book included in sys.catalog as variable b. With b.isbn = i on the right side, it returns them if the ISBN matches.

We check the success and failure of the search with assertions. The code is as follows:

assert findBookByIsbnSuccess {
    all sys: System, i: Isbn, b: Book | 
        b in sys.catalog and b.isbn = i 
        implies b in findBookByIsbn[sys, i]
}

assert findBookByIsbnFail {
    all sys: System, i: Isbn, b: Book | 
        b not in sys.catalog and b.isbn = i 
        implies b not in findBookByIsbn[sys, i]
}

The contents of the expressions used in the assertions are almost the same as before. The parts where we used predicates are now functions. Since findBookByIsbn returns a set Book, we can write b not in relative to the return value.

Other search operations can be defined similarly. Please refer to the code at the end of the article for details.

Final Code

I think the remaining operations can be understood based on what has been explained so far. Since this is the code of a beginner, there might be better ways to write it.

sig Title {}

sig Author {}

sig Isbn {}

sig Book {
    title: Title,
    author: Author,
    isbn: Isbn,
}

sig System {
    catalog: set Book,
    copies: catalog -> Int
} {
   all b: Book | copies[b] >= 0
}

fact singletonSystem {
    #System = 1
}

// Add a book that is not yet registered in the system. In case of success, there is a state change (addition of the book).
pred addBook [sys: System, sys": System, b: Book] {
    b not in sys.catalog => sys".catalog = sys.catalog + b
}

// Add one copy of a book registered in the system. In case of success, there is a state change (increase in inventory).
pred addCopy [sys, sys": System, b: Book] {
    b in sys.catalog => sys".copies = sys.copies + (b -> (sys.copies[b] + 1))
}

// Lend a book that is registered and has available inventory. In case of success, there is a state change (decrease in inventory).
pred borrowCopy [sys: System, sys": System, b: Book] {
    (b in sys.catalog and sys.copies[b] > 0) => sys".copies = sys.copies + (b -> (sys.copies[b] - 1))
}

// Return a book registered in the system. In case of success, there is a state change (increase in inventory).
pred returnCopy [sys, sys": System, b: Book] {
    b in sys.catalog => sys".copies = sys.copies + (b -> (sys.copies[b] + 1))
}

// Function that searches for a book by ISBN and returns the result
fun findBookByIsbn [sys: System, i: Isbn]: set Book {
    {b: sys.catalog | b.isbn = i}
}

// Function that searches for a book by title and returns the result
fun findBookByTitle [sys: System, t: Title]: set Book {
    {b: sys.catalog | b.title = t}
}

// Function that searches for a book by author and returns the result
fun findBookByAuthor [sys: System, a: Author]: set Book {
    {b: sys.catalog | b.author = a}
}

assert addNewBookSuccess {
    all sys, sys": System, b: Book |
        b not in sys.catalog
        implies addBook[sys, sys", b]
        implies b in sys".catalog
}

check addNewBookSuccess for 5

assert addExistingBookFail {
    all sys, sys": System, b: Book |
        b in sys.catalog
        implies addBook[sys, sys", b]
        implies b in sys".catalog
}

check addExistingBookFail for 5

assert addCopyExistingSuccess {
    all sys, sys": System, b: Book | 
        b in sys.catalog 
        implies addCopy[sys, sys", b] 
        implies sys".copies[b] = sys.copies[b] + 1
}

check addCopyExistingSuccess for 5

assert addCopyNewFail {
    all sys, sys": System, b: Book | 
        b not in sys.catalog 
        implies addCopy[sys, sys", b]
        implies sys".copies[b] = sys.copies[b]
}

check addCopyNewFail for 5

assert borrowCopySuccess {
    all sys, sys": System, b: Book | 
        b in sys.catalog and sys.copies[b] > 0 
        implies borrowCopy[sys, sys", b] 
        implies sys".copies[b] = sys.copies[b] - 1
}

check borrowCopySuccess for 5

assert borrowCopyNoStockFail {
    all sys, sys": System, b: Book | 
        b in sys.catalog and sys.copies[b] = 0 
        implies not borrowCopy[sys, sys", b]
}

check borrowCopyNoStockFail for 5

assert borrowCopyNotRegisteredFail {
    all sys, sys": System, b: Book | 
        b not in sys.catalog 
        implies not borrowCopy[sys, sys", b]
}

check borrowCopyNotRegisteredFail for 5

assert findBookByIsbnSuccess {
    all sys: System, i: Isbn, b: Book | 
        b in sys.catalog and b.isbn = i 
        implies b in findBookByIsbn[sys, i]
}

assert findBookByIsbnFail {
    all sys: System, i: Isbn, b: Book | 
        b not in sys.catalog and b.isbn = i 
        implies b not in findBookByIsbn[sys, i]
}

check findBookByIsbnSuccess for 5

check findBookByIsbnFail for 5

assert findBookByTitleSuccess {
    all sys: System, t: Title, b: Book | 
        b in sys.catalog and b.title = t 
        implies b in findBookByTitle[sys, t]
}

assert findBookByTitleFail {
    all sys: System, t: Title, b: Book | 
        b not in sys.catalog and b.title = t 
        implies b not in findBookByTitle[sys, t]
}

check findBookByTitleSuccess for 5

check findBookByTitleFail for 5

assert findBookByAuthorSuccess {
    all sys: System, a: Author, b: Book | 
        b in sys.catalog and b.author = a 
        implies b in findBookByAuthor[sys, a]
}

assert findBookByAuthorFail {
    all sys: System, a: Author, b: Book | 
        b not in sys.catalog and b.author = a 
        implies b not in findBookByAuthor[sys, a]
}

check findBookByAuthorSuccess for 5

check findBookByAuthorFail for 5

Summary

The method of describing specifications in a language with a mathematical foundation and verifying design and behavior is called formal methods. I didn't mention this term earlier because using it from the start might have turned people off. While I knew the term, I always thought it was something unrelated to me.

Formal methods are utilized in fields such as embedded systems or safety-critical systems where errors in specifications or implementation can lead to fatal problems. Many specification languages other than Alloy have been developed, and the tools used vary depending on the project.

As mentioned at the beginning, I've been thinking about whether I can easily use model checking to think about or verify specifications personally. I think it's useful for general apps and web services, but the learning cost is high, and since Alloy doesn't output implementation code, it might not be very realistic to integrate it into team development.

Among specification languages, I think Alloy has a relatively low learning cost. Nowadays, you can ask AI anything, so wouldn't it be interesting to give it a try? (Though, I feel the quality of code output by ChatGPT or GitHub Copilot is not that great.)

If you enjoyed this, I would be happy to receive a badge. It will go toward my coffee fund.

References

Books

• Software Abstractions: Logic, Language, and Analysis: The Address Book example from the Exercises is explained as sample code. It's easier to read than I expected, even without specialized knowledge.

Web

• Alloy Tutorial: Uses a file system as an example.
• Formal Software Design with Alloy 6
• Alloy Docs: The title looks official, but it's unofficial.