# Alloy Analyzer

> Daniel Jackson이 개발한 모델링 언어. 참고: Language reference

<Daniel Jackson>이 개발한 모델링 언어. 참고: [Language reference](https://alloytools.org/spec.html)

https://alloytools.org

## Features

- [Small scope hypothesis](https://wiki.g15e.com/pages/Small%20scope%20hypothesis.txt)에 기반하여 모든 경우의 수를 자동으로 검사
- 모든 것을 n-ary relation으로 취급. 예: `[{x}]`, 벡터는 `[{x, y}]`, 매트릭스는 `[{w, x}, {y, z}]`
- 내부적으로 [SAT solver](https://wiki.g15e.com/pages/SAT%20solver.txt)를 이용

## Publications

- [Software Abstractions: Logic, Language, and Analysis](https://wiki.g15e.com/pages/Software%20Abstractions%20-%20Logic,%20Language,%20and%20Analysis.txt)
- [Practical Alloy](https://wiki.g15e.com/pages/Practical%20Alloy.txt)

## Articles

- <2025-06-13> - [Alloy: Communications of the ACM](https://cacm.acm.org/research/alloy/) by <Daniel Jackson>