New book: Practical Alloy -- A hands-on guide to formal software design

[grayswandyr]

It is my pleasure to announce Practical Alloy – A hands-on guide to formal software design, a new (draft) online book on Alloy 6+, by Alcino Cunha, Nuno Macedo, Julien Brunel and David Chemouil.

This book is an introduction to formal software design with Alloy.

A key activity in design is to develop models of the software system to be implemented. Models are abstractions that allow us to quickly explore design alternatives and help us reason about the expected requirements.

Alloy is a formal modeling language that can be used to describe complex mutable software structures using simple mathematical concepts. The Alloy Analyzer supports both automatic model validation and verification of expected requirements, making Alloy one of the most cost-effective formal design frameworks nowadays.

This book starts by presenting the basics of both structural and behavioral modeling with Alloy, and then explores its application in the formal design of different kinds of software systems, ranging from simple user apps to distributed protocols.

The presentation of the different concepts is always illustrated with practical examples, making this book a hands-on guide to learn formal software design with Alloy.

All the examples in this book are available in a public GitHub repository This repository has a directory for each chapter (or advanced topic) in the book containing the example models at that chapter.

The book also has a comment system that allows you to leave comments or suggestions for each chapter and each advanced topic.

More details at Practical Alloy!

[roasbeef]

Nice work! Looking forward to diving into a new up to date resource on Alloy.

I clicked through a bit and noticed that some of the links to the full models appear to be broken:

Clicking “Full model for the section” leads to a Github link that doesn’t resolve (404): https://github.com/practicalalloy/models/tree/main/behavioral-modeling/verifying-expected-properties.

[grayswandyr]

Hi thanks for the report, this is fixed.

[Alejandro]

Hello. I’m not sure where to send feedback for the book. Is this thread ok?

On this page there’s a typo.

The, relation shared is declared as a variable field inside the File signature

[grayswandyr]

If you’re connected to Github, you should in principle see a comment box at the bottom of every page (on my browser, it appears after a short but noticeable period of time). This will automatically add an issue to the issue tracker.

EDIT: I will handle this, no need to file an issue for this one. Thanks.