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.

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.