3 ways to model the set of non-negative even numbers

Introduction

Here’s why I think you should read this paper:

1. It shows you Alloy and Alloy is really useful. Used effectively, Alloy can help you create better, more reliable software.
2. This paper is short and easy to read and will give you a good feel for what you can do with Alloy.

Here’s the downside of this paper: The thing being modeled - the set of non-negative even numbers - is not interesting, nor is it typical of the things that you would normally model with Alloy. Alloy is typically used to model software and/or systems.

Despite the downside, I feel this paper is quite useful and worth reading.

I'll assume that you're still reading, so let's begin with an overview of what you will see in this paper.

This paper shows 3 different ways to model the set of non-negative even numbers. It shows how you can get a higher level of assurance that your model is correct by specifying and checking some defining properties. Lastly, it shows how you can check whether two different models are equivalent.

Problem Statement: Concisely represent (model) this instance: 0, 2, 4, …

List Model

Let’s start simple. Instead of modeling an infinite list, let’s model this finite list: 0, 2, 4, 6.

Here is the Alloy model:

one sig List {
    numbers: set Int
}{
    numbers = 0 + 2 + 4 + 6
}

sig is a reserved word. It stands for signature. A signature declaration defines a set. In this case the signature declaration defines a set named List. The set has just one member. You can think of List as an object (in the object-oriented sense). The object has one field called numbers. It will hold the desired list of values (0, 2, 4, 6). The value of numbers is a set of Int (integers).

However, we do not want the value of numbers to contain any old set of integers. We want it to contain just the integers 0, 2, 4, 6. So, supplement the signature declaration with a signature fact that contrains the set. (The signature fact is the stuff in the second pair of curly braces) The plus symbol ( + ) does not mean addition, it means set union. In Alloy each value is a set, e.g., 0 is {0}, 1 is {1} and 0 + 1 is {0, 1}. So, the value of numbers is the desired set.

Predicate Model

The list notation can only be used to model finite sets. The predicate notation can be used to model infinite sets.

The approach taken by the predicate notation is to represent a set by specifying properties that each member of the set must have. In our case, each integer in the set must have these two properties:

1. The integer must be even.
2. The integer must be non-negative.

These are called "defining properties."

Here is the Alloy model:

one sig List {
    numbers: set Int
}{
    numbers = {i: Int | i >= 0 and (rem[i,2] = 0)}
}

The signature fact uses a set comprehension to specify the value of numbers: The set of all integer i such that i is greater than or equal to 0 and the remainder of dividing i by 2 is 0.

Generator Model

Suppose there exists a model of a number line in which each integer i is connected to i+2

Then, the desired set of integers can be modeled as: The chain of integers starting at 0.

It is better to model the number line as a sequence where each integer i has i.next and i.prev rather than i+1 and i-1. Here’s why: Since computers are finite, instances are also finite. Instances modeled by adding 2 to each integer will eventually fail with arithmetic overflow or with addition circling around to negative values. So, instead of the instance connecting i to i+2, the instance connects i to the integer that is two steps away in the sequence: i.next.next

Here is the Alloy model:

one sig NumberLine {
    connections: Int -> Int
} {
    all i: Int | connections[i] = i.next.next
}

The signature declaration defines NumberLine, which has a field called connections. The value of connections is a set of (int, int) pairs. The arrow operator ( -> ) means "all possible combinations of the set on the left of the arrow with the set on the right of the arrow." You might remember from your high school math class that this is called the cartesian product.

However, we do not want the value of connections to be all possible (int, int) pairs. We only want (i, i.next.next) pairs. The signature fact constrains the pairs: For all integer i the value of the i’th connection is i.next.next

Now that the number line is defined, we are ready to model the desired list. The value of numbers is the chain starting at 0.

one sig List {
    numbers: set Int 
} {
    numbers = 0.*(NumberLine.connections)
}

The reflexive transitive closure operator ( * ) means "in a set of pairs, wherever there is a pair (A, B) and a pair (B, C), then add these pairs: (A, A) and (A, C)." In other words, create pairs for all the values that A can reach, including itself. For our case, the set of pairs contains (0, 2) and (2, 4), so the * operator will add these pairs: (0, 0) and (0, 4).

0.*(NumberLine.connections) means "all the integers that can be reached from 0," which is: 0, 2, 4, 6, …

To raise the level of confidence that this model generates an instance with the desired list of integers, we can check that each integer in numbers has the two defining properties that we saw earlier:

1. Even property: each integer must be even.
2. Non-negative property: each integer must be non-negative.

The Alloy assert is used to check a model. The following assert checks that each integer in numbers has the two defining properties:

assert only_positive_even_numbers {
    all i: List.numbers | i >= 0 and rem[i, 2] = 0
}

Read as: For all numbers i in List.numbers, i must be greater than or equal to 0 and the remainder of dividing i by 2 must be zero.

When the Alloy Analyzer is requested to check the assert, it responds with, "No counterexample found." In other words, the Alloy Analyzer is unable to find a member of numbers that is not non-negative and/or not even.

Equivalence of the Predicate and Generator Models

The predicate model concisely represents (models) the list: 0, 2, 4, 6, … The generator model likewise concisely represents (models) the list: 0, 2, 4, 6, … We would like to show that the two models are equivalent; that is, they both represent (model) the same instance.

Below are the two models and an assert which tests their equivalence. Notice that the signature fact for the List signature is gone. Instead, there are two pred (predicates). The pred named Predicate, when invoked, constrains numbers using a set comprehension. The pred named Generator, when invoked, constrains numbers to the chain of integers in NumberLine starting at 0. Also notice that in each pred the numbers field is explicitly qualified with “List.” to indicate that numbers is a field within List. Previously, when using a signature fact, the “List.” was implicit. At the bottom is an assert. It says this: If an instance satisfies the constraints specified in Predicate, then the instance will also satisfy the constraints specified in Generator, and vice versa. In other words, the instance represented by Predicate is the same instance represented by Generator. When the Alloy Analyzer is requested to check the assert, it responds with, "No counterexample found." In other words, the Predicate model and the Generator model are equivalent. Very cool.

Here is the Alloy model:

one sig NumberLine {
    connections: Int -> Int
} {
    all i: Int | i.connections = i.next.next
}

one sig List {
    numbers: set Int 
} 

pred Predicate {
    List.numbers = {i: Int | i >= 0 and (rem[i,2] = 0)}
}

pred Generator {
    List.numbers = 0.*(NumberLine.connections)
}

assert Equivalent {
    Predicate iff Generator
}