Alloy Introduction

• Readings
  • Recommended readings
• Topics covered
• Resources
• Transitive closure

Readings

• Class notes on set theory recap

• Class notes on Alloy intro

• Class notes on Alloy constraints

• Old recorded lectures
• Old class notes on an introduction to Alloy [part 1, part 2]
  • In particular try to do the exercises in these lecture notes

Recommended readings

• Alloy FAQ
• Lecture notes on first-order logic
  • by Cesare Tinelli
  • by Mario S. Alvim
• Alloy Analyzer tutorial, notes by Greg Dennis and Rob Seater [part 1, part 2]

• A hands-on introduction to Alloy, by Michael Sperberg-McQueen

• Automatic generation of security exploits with Alloy, by Caroline Trippel et al. [paper 1, paper 2]

• More generally, how Amazon Web Services has been leveraging formal methods:
  • Provable Security: Security Assurance, Backed by Mathematical Proof
  • CAV 2022 keynote - A Billion SMT Queries A Day

Topics covered

• Modeling general software systems.
  • Introduction to the Alloy modeling language.
  • Alloy’s foundadions.
  • Signatures, fields, and multiplicity constrainst.
• Modeling simple domains in Alloy.
  • Generating and analyzing model instances.
• Relations and operations on them.
  • Formulas, Boolean operators and quantifiers.
  • Expressing constraints on relations using Alloy formulas.
• Functions and predicates.

Resources

• A simple family model for the Alloy Analyzer: family-1.als
• A simple family model with facts, different run configurations and assertions for the Alloy Analyzer: family-2.als

Transitive closure

A relation is transitive when it satisfies the transitivity property, which can be stated as:

∀xyz . ((x, y) ∈ R ∧ (y, z) ∈ R) → (x, z) ∈ R

for any relation R : A × A, with x,y,z ∈ A. The transitive closure of a relation R is the smallest transitive relation containing it. It can be defined as

R⁺ = R ∪ (R ; R) ∪ ((R ; R) ; R) ∪ ...

in which ; is relation composition.

Consider a relation S = {(a, b), (b, c)}. This relation is not transitive. Its transitive closure can be obtained by creating a new relation T which contains S, is transitive, and is the smallest relation with these two properties. This is the case if T = {(a, b), (b, c), (a, c)}, i.e., T = S ∪ (S ; S).

Note that (S ; S) ; S is the empty set. So no new pairs can be obtained via composition.