# Software Abstractions Example With Alloy 6

**URL:** <https://alloytools.discourse.group/t/software-abstractions-example-with-alloy-6/541>\
**Category:** Alloy 6\
**Created:** [November 5, 2025, 10:36pm UTC](https://alloytools.discourse.group/t/software-abstractions-example-with-alloy-6/541 "2025-11-05T22:36:25Z")\
**Posts on this page:** 3\
**Page:** 1

<div class="post-metadata">

**Author:** ![OnorioCatenacci](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/onoriocatenacci/32/65_2.png) [@OnorioCatenacci](https://alloytools.discourse.group/u/OnorioCatenacci)\
**Post date:** [November 5, 2025, 10:36pm UTC](https://alloytools.discourse.group/t/software-abstractions-example-with-alloy-6/541/1 "2025-11-05T22:36:26Z")

</div>

Looking at the Software Abstractions book, on page 9 there’s the following example:

```auto
pred add(b, b’: Book, n: Name, a: Addr)

{

b’.addr = b.addr + n → a

}

```

Since Alloy 6 now reserves the single quote, I tried this (and it appears to have worked):

```auto
pred add(b: Book, n: Name, a: Addr)

{

b’.addr = b.addr + n → a

}

```

I just want to ensure I’m not making a bad assumption. Both expressions are asserting that the set of addresses in the book after a new name → address mapping is added is the old set plus the name → address mapping. So they’re equivalent, right?

---

<div class="post-metadata">

**Author:** ![alcino](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/alcino/32/25_2.png) [@alcino](https://alloytools.discourse.group/u/alcino)\
**Post date:** [November 6, 2025, 12:05pm UTC](https://alloytools.discourse.group/t/software-abstractions-example-with-alloy-6/541/2 "2025-11-06T12:05:00Z")

</div>

Hi,

To adapt the book example to Alloy 6 it takes a bit more work. Alloy 5 did not had an implicit notion of state nor support for mutable relations. This means that we needed to model the state of the system explicitly. In the “Software Abstractions” example, signature `Book` was actually being used to model the different states of a single address book, not different address books. In Alloy 6 we don’t need to model the system state explicitly so and we can declare fields and signatures to be mutable, so we can just have the following declarations.

```alloy
sig Name {
	var addr : lone Addr
}
sig Addr {}

```

We have names and addresses and `add` is a mutable field that associates each name with its address, if any. Now, to model `add` we can do the following.

```alloy
pred add[n: Name, a: Addr] {
	addr' = addr + n -> a
}

```

The prime operator show be applied to mutable expressions (namely mutable fields) and determines the value of that expression in the next state. If you apply it to a non-mutable expression it has no effect. Here we say that in the next state the pair `n->a` will be added to the current value of `addr`. You can ask for an “interesting” example of this predicate with the following command.

```alloy
pred showAdd[n: Name, a: Addr] {
	add[n,a]
	#addr' > #addr
}
run showAdd for 3 but 2 steps

```

Notice the scope `2 steps` which states that we are only interested in seeing the first two states of execution. The predicate is only imposing that predicate `add` should be true in the first state, so there is no point in looking at more than two states because no restrictions are being imposed on what happens afterwards, so the trace will be more or less random. The result of this command could be the following.

 ![image](https://global.discourse-cdn.com/free1/uploads/alloytools/original/1X/398a1bbae450b7b63316482040ce72d45310c247.jpeg)

Similar to what was done in “Software Abstractions” we can now model `del` and check the assertion that delete undoes add as follows.

```alloy
pred del[n: Name, a: Addr] {
	addr' = addr - n -> a
}

assert delUndoesAdd {
	all n: Name, a: Addr |
		add[n,a] and after del[n,a] implies addr'' = addr
}
check delUndoesAdd for 3 but 3 steps

```

Notice the use of the `after` temporal operator, which is true for a formula if that formula holds in the next state. In this case we want to check that if `add` happens in the first state and `del` in the second (the next) state, then the value of `addr` in the third state is equal to the value of `addr` in the first state. Since we need three states to reason about this property we set the scope of `3 steps`. As mentioned in the book, this assertion is not valid and a possible counter-example is the following.

 ![image](https://global.discourse-cdn.com/free1/uploads/alloytools/original/1X/435adf304d5f25d4c2c7680e87e23aa6d968fa14.jpeg)

 ![image](https://global.discourse-cdn.com/free1/uploads/alloytools/original/1X/65fb76216568a88498c7caa81912454588c52e61.jpeg)

Notice that to see what is happening in the transition between the second and third state (as shown in the second picture above) we need to press right arrow button.

I hope this helped. I recommend you take a look at [https://practicalalloy.github.io](https://practicalalloy.github.io) to learn a bit more about Alloy 6, in particular about all the new temporal operators and how to model a state machine with those operators.

Best,

Alcino

---

<div class="post-metadata">

**Author:** ![OnorioCatenacci](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/onoriocatenacci/32/65_2.png) [@OnorioCatenacci](https://alloytools.discourse.group/u/OnorioCatenacci)\
**Post date:** [November 7, 2025, 4:13pm UTC](https://alloytools.discourse.group/t/software-abstractions-example-with-alloy-6/541/3 "2025-11-07T16:13:49Z")

</div>

Thank you so much for the thorough and illuminating explanation! I am still trying to wrap my head around Alloy and how to use it properly. Learning on my own makes progress quite slow. 🙂