В компьютерной науке и программной инженерии Alloy — это декларативный язык спецификаций для выражения сложных структурных ограничений и поведения в программной системе . Alloy предоставляет простой инструмент структурного моделирования, основанный на логике первого порядка . [1] Alloy нацелен на создание микромоделей , которые затем могут быть автоматически проверены на корректность . Спецификации Alloy можно проверить с помощью Alloy Analyzer.
Хотя Alloy разработан с учетом автоматического анализа, Alloy отличается от многих языков спецификаций, разработанных для проверки моделей , тем, что он позволяет определять бесконечные модели. Анализатор Alloy разработан для выполнения проверок конечной области даже на бесконечных моделях.
Язык и анализатор Alloy разработаны командой под руководством Дэниела Джексона из Массачусетского технологического института в США .
Первая версия языка Alloy появилась в 1997 году. Это был довольно ограниченный язык объектного моделирования . Последующие итерации языка «добавили квантификаторы , отношения более высокой арности , полиморфизм , подтипирование и сигнатуры». [2]
Математическая основа языка во многом сформировалась под влиянием нотации Z , а синтаксис Alloy в большей степени обязан таким языкам, как Object Constraint Language .
Анализатор Alloy был специально разработан для поддержки так называемых «легких формальных методов». Таким образом, он предназначен для обеспечения полностью автоматизированного анализа, в отличие от интерактивных методов доказательства теорем , обычно используемых с языками спецификаций, похожими на Alloy. Разработка анализатора изначально была вдохновлена автоматизированным анализом, предоставляемым проверщиками моделей . Однако проверка моделей плохо подходит для типов моделей, которые обычно разрабатываются в Alloy, и в результате ядро анализатора в конечном итоге было реализовано как поисковик моделей, построенный поверх решателя булевых SAT . [1]
В версии 3.0 Alloy Analyzer включал в себя встроенный SAT-based model-finder, основанный на готовом SAT-solver. Однако, начиная с версии 4.0 Analyzer использует Kodkod model-finder, для которого Analyzer выступает в качестве front-end. Оба model-finder по сути переводят модель, выраженную в реляционной логике , в соответствующую формулу булевой логики , а затем вызывают готовый SAT-solver для булевой формулы. В случае, если решатель находит решение, результат переводится обратно в соответствующую привязку констант к переменным в реляционной логической модели. [3]
Чтобы гарантировать разрешимость проблемы поиска модели , Alloy Analyzer выполняет поиск модели в ограниченных областях, состоящих из определенного пользователем конечного числа объектов. Это ограничивает общность результатов, выдаваемых Analyzer. Однако разработчики Alloy Analyzer оправдывают решение работать в ограниченных областях, ссылаясь на гипотезу о малой области : большую долю ошибок можно найти, тестируя программу для всех тестовых входов в некоторой малой области. [4]
Модели сплавов имеют реляционную природу и состоят из нескольких различных видов утверждений: [1]
sig Object{}определяет объект подписиsig List{ head : lone Node }определяет сигнатуру List , содержащую заголовок поля типа Node и множественность lone — это устанавливает существование связи между List s и Node s, такой что каждый List связан не более чем с одним головным узломПоскольку Alloy является декларативным языком, смысл модели не зависит от порядка операторов.