Сплав (язык спецификации)
В информатике и разработке программного обеспечения Alloy представляет собой декларативный язык спецификаций для выражения сложных структурных ограничений и поведения в программной системе . Alloy предоставляет простой инструмент структурного моделирования, основанный на логике первого порядка . [1] Alloy ориентирован на создание микромоделей которых затем можно автоматически проверить , корректность . Характеристики сплавов можно проверить с помощью анализатора сплавов.
Хотя Alloy разработан с учетом автоматического анализа, Alloy отличается от многих языков спецификаций, предназначенных для проверки моделей, тем, что он позволяет определять бесконечные модели. Анализатор сплавов предназначен для выполнения ограниченных проверок даже на бесконечных моделях.
Язык и анализатор Alloy разработаны командой под руководством Дэниела Джексона из Массачусетского технологического института в США .
История и влияния
[ редактировать ]Первая версия языка Alloy появилась в 1997 году. Это был довольно ограниченный язык объектного моделирования . Последующие версии языка «добавили кванторы , отношения более высокой арности , полиморфизм , подтипирование и сигнатуры». [2]
Математическая основа языка находилась под сильным влиянием нотации Z , а синтаксис Alloy во многом обязан таким языкам, как Object Constraint Language .
Анализатор сплавов
[ редактировать ]
Анализатор сплавов был специально разработан для поддержки так называемых «облегченных формальных методов». Таким образом, он предназначен для обеспечения полностью автоматизированного анализа, в отличие от интерактивных методов доказательства теорем, обычно используемых в языках спецификаций, подобных Alloy. Первоначально анализатор был вдохновлен автоматизированным анализом, обеспечиваемым средствами проверки моделей . Однако проверка моделей плохо подходит для тех моделей, которые обычно разрабатываются в Alloy, и в результате ядро анализатора в конечном итоге было реализовано как средство поиска моделей, построенное на основе логического решателя SAT . [1]
Начиная с версии 3.0, Alloy Analyser включает в себя встроенный инструмент поиска моделей на основе SAT, основанный на стандартном решателе SAT. Однако, начиная с версии 4.0, Анализатор использует средство поиска моделей Kodkod, для которого Анализатор выступает в качестве внешнего интерфейса. Оба средства поиска моделей по существу переводят модель, выраженную в реляционной логике , в соответствующую формулу логической логики , а затем вызывают готовый решатель SAT для обработки булевой формулы. В случае, если решатель находит решение, результат преобразуется обратно в соответствующую привязку констант к переменным в реляционной логической модели. [3]
Чтобы гарантировать разрешимость проблемы поиска модели , Alloy Analyser выполняет поиск модели в ограниченных областях, состоящих из определяемого пользователем конечного числа объектов. Это приводит к ограничению общности результатов, получаемых анализатором. Однако разработчики Alloy Analyser оправдывают решение работать в ограниченных рамках, апеллируя к гипотезе малого объема : большую часть ошибок можно обнаружить путем тестирования программы для всех тестовых входных данных в небольшом объеме. [4]
Структура модели
[ редактировать ]Модели сплавов носят реляционный характер и состоят из нескольких типов операторов: [1]
- Сигнатуры определяют словарь модели путем создания новых наборов.
sig Object{}подписи определяет объектsig List{ head : lone Node }определяет сигнатуру List поля , которая содержит заголовок типа Node и кратности lone — это устанавливает существование связи между List и Node , так что каждый List связан не более чем с одним головным Node.
- Факты — это ограничения, которые, как предполагается, всегда выполняются.
- Предикаты представляют собой параметризованные ограничения и могут использоваться для представления операций.
- Функции — это выражения, которые возвращают результаты.
- Утверждения — это предположения о модели.
Поскольку Alloy является декларативным языком, порядок операторов не влияет на значение модели.
Ссылки
[ редактировать ]- ^ Перейти обратно: а б с Джексон, Дэниел (2006). Абстракции программного обеспечения: логика, язык и анализ . МТИ Пресс . ISBN 978-0-262-10114-1 .
- ^ «Часто задаваемые вопросы по сплавам» . Архивировано из оригинала 7 июня 2007 года . Проверено 7 марта 2013 г.
- ^ Торлак, Э. ; Деннис, Г. (апрель 2008 г.). «Кодкод для пользователей сплавов» (PDF) . Первый цех сплавов ACM . Портленд, Орегон. Архивировано из оригинала (PDF) 22 июня 2010 года . Проверено 19 апреля 2009 г.
- ^ Андони, Александр; Данилюк, Дмитрий; Хуршид, Сарфраз; Маринов, Дарко (2002). «Оценка гипотезы малого масштаба» CiteSeerX 10.1.1.8.7702 .
Внешние ссылки
[ редактировать ]- Сайт сплава
- Репозиторий сплава на Github
- Руководство по сплавам
- Веб-сайт системы анализа Kodkod в Массачусетском технологическом институте
- Метамодель сплава в Ecore