Alloy
Formal verification · a modeling language and analyzer
created · updated
A way to describe objects and the links between them and ask a program to find a small example where a rule is broken. For example, the rule “an employee has exactly one boss”: the program finds an example where one employee has two bosses at once. It suits checking the structure of data and access rights. Like TLA+, it uses a mathematical notation. The language was created in the Software Design Group at MIT.
Source: alloytools.org, the Alloy site
Where it appears · 4
- Vitest vs Jest · Specs and context
- How to find a race condition in code · Specs and context
- How model checking differs from testing · Specs and context
- TLA+ vs Alloy vs Quint · Specs and context