5. Formal Specification

In this chapter, we discuss formal specification of software systems. We will use Alloy, a lightweight modeling language based on relational logic, to express our specifications. We focus on modeling data structures, defining constraints, specifying operations, and reasoning about system behavior using Alloy’s built-in analysis tools.

Note

This chapter is in its initial stages for spring 2025 and subject to ongoing revisions!

More details, including additional examples, are available in the book Formal Software Design with Alloy 6.

5.1. Introduction to Alloy

Alloy is a declarative language for specifying structural properties of systems. It is built on first-order relational logic and provides an automatic analysis engine, the Alloy Analyzer, to explore instances and verify properties.

These are Alloy’s key features:

Uses signatures (sig) to define entities and their relationships.
Defines constraints using facts, predicates, and assertions.
Allows instance exploration and counterexample generation.
Supports temporal reasoning with basic transition modeling.

Alloy 6 extends earlier versions with improved support for expressing operations and transitions.

5.2. Modeling Data Structures in Alloy: A Simple Queue

We begin by modeling a bounded queue to illustrate formal specification concepts using Alloy as a notation. A queue holds elements in a first-in, first-out (FIFO) order. We define a basic queue structure:

module Queue

sig Element {}

sig Queue {
    elements: seq Element
}

Here, Element is a basic type representing items in the queue. The Queue signature has a relation elements using a sequence (seq), which ensures order.

5.3. Basic Constraints

We now define a fact to limit the queue’s size:

fact BoundedSize {
    all q: Queue | #q.elements <= 5
}

This constraint ensures no queue contains more than five elements.

5.4. Exploring Instances

We can generate sample instances using the Alloy Analyzer:

run {} for 3 Queue, 5 Element

This command searches for valid queue instances under the given bounds.

5.5. Modeling operations: Enqueue and Dequeue

We now add operations to manipulate the queue. In Alloy, we define these using predicates:

pred enqueue[q: Queue, e: Element] {
    #q.elements < 5
    q.elements' = q.elements + e
}

pred dequeue[q: Queue, e: Element] {
    some q.elements
    e = first q.elements
    q.elements' = rest q.elements
}

Here, enqueue adds an element (if space allows), and dequeue removes the first element.

5.6. Checking Properties

We verify queue behavior using assertions:

assert FIFO {
    all q: Queue, e1, e2: Element |
        enqueue[q, e1] and enqueue[q, e2] implies
        dequeue[q, e1]
}

check FIFO for 5 Queue, 5 Element

If a counterexample exists, Alloy will generate one.

5.7. Basic Behavioral Specification

We now model state transitions in Alloy. We start with a state-based view of the queue:

sig State {
    queues: Queue
}

pred step[s, s': State] {
    some q: Queue |
        enqueue[q, some Element] or dequeue[q, some Element]
}

5.8. Temporal Properties

We check sequences of operations:

pred always_not_empty {
    all s: State | some s.queues.elements
}

check always_not_empty

This verifies that the queue is never empty across all states.

5.9. Conclusion

This chapter introduced Alloy 6 for modeling data structures, specifying operations, and verifying behaviors using constraints and assertions. The next topic extends these concepts to temporal logic and model checking.