Из Википедии, бесплатной энциклопедии
Перейти к навигации Перейти к поиску

В информатике и программной инженерии , сплав декларативный язык спецификаций для выражения сложных структурных ограничений и поведение в системе программного обеспечения . Alloy предоставляет простой инструмент структурного моделирования, основанный на логике первого порядка . [1] Alloy предназначен для создания микромоделей, которые затем могут автоматически проверяться на правильность . Характеристики сплава можно проверить с помощью анализатора сплавов.

Хотя Alloy разработан с учетом автоматического анализа, Alloy отличается от многих языков спецификаций, предназначенных для проверки моделей, тем, что позволяет определять бесконечные модели. Анализатор сплавов разработан для выполнения проверок в ограниченном объеме даже на бесконечных моделях.

Язык и анализатор Alloy разработаны командой под руководством Дэниела Джексона из Массачусетского технологического института в США .

История и влияние [ править ]

Первая версия языка Alloy появилась в 1997 году. Это был довольно ограниченный язык объектного моделирования . Последующие итерации языка «добавили кванторы , отношения более высокой степени арности , полиморфизм , подтипы и сигнатуры». [2]

На математическую основу языка сильно повлияла нотация Z , а синтаксис Alloy больше обязан таким языкам, как Object Constraint Language .

Анализатор сплавов [ править ]

Анализатор сплавов.

Анализатор сплавов был специально разработан для поддержки так называемых «облегченных формальных методов». Таким образом, он предназначен для обеспечения полностью автоматизированного анализа, в отличие от интерактивных методов доказательства теорем , обычно используемых с языками спецификаций, подобными Alloy. Первоначально разработка анализатора была вдохновлена ​​автоматическим анализом, обеспечиваемым программами проверки моделей . Однако проверка моделей плохо подходит для моделей, которые обычно разрабатываются в Alloy, и в результате ядро ​​анализатора в конечном итоге было реализовано как средство поиска моделей, построенное на логическом решателе SAT . [1]

Начиная с версии 3.0, анализатор сплавов включал в себя встроенный искатель моделей на основе SAT, основанный на стандартном SAT-решателе. Однако, начиная с версии 4.0, Анализатор использует поисковик моделей Kodkod, для которого Анализатор выступает в качестве внешнего интерфейса. Оба средства поиска моделей по существу переводят модель, выраженную в реляционной логике, в соответствующую формулу логической логики , а затем вызывают готовый SAT-решатель для этой логической формулы. В случае, если решающая программа находит решение, результат преобразуется обратно в соответствующую привязку констант к переменным в реляционной логической модели. [3]

Чтобы гарантировать, что проблема поиска модели разрешима , Alloy Analyzer выполняет поиск модели в ограниченном объеме, состоящем из определенного пользователем конечного числа объектов. Это ограничивает универсальность результатов, выдаваемых анализатором. Однако разработчики Alloy Analyzer оправдывают решение работать в ограниченных рамках апелляцией к гипотезе малого объема : большая часть ошибок может быть обнаружена путем тестирования программы для всех входных тестов в небольшом объеме. [4]

Структура модели [ править ]

Сплавные модели носят реляционный характер и состоят из нескольких различных типов утверждений: [1]

  • Сигнатуры определяют словарь модели путем создания новых наборов.
sig Object{}определяет подпись объекта
sig List{ head : lone Node }определяет сигнатуру список , который содержит поле головку типа узла и множественность одинокой - это устанавливает наличие связи между списком s и Node s таким образом, что каждый список связан с не более чем один головным узлом
  • Факты - это ограничения, которые, как предполагается, всегда выполняются.
  • Предикаты - это параметризованные ограничения, которые могут использоваться для представления операций.
  • Функции - это выражения, возвращающие результаты
  • Утверждения - это предположения о модели.

Поскольку Alloy является декларативным языком, на значение модели не влияет порядок операторов.

Ссылки [ править ]

  1. ^ a b c Джексон, Дэниел (2006). Программные абстракции: логика, язык и анализ . MIT Press . ISBN 978-0-262-10114-1.
  2. ^ "Часто задаваемые вопросы о сплавах" . Архивировано из оригинала 7 июня 2007 года . Проверено 7 марта 2013 года .
  3. ^ Torlak, E .; Деннис, Г. (апрель 2008 г.). «Кодкод для пользователей сплавов» (PDF) . Первый цех по сплавам ACM . Портланд, штат Орегон. Архивировано из оригинального (PDF) 22 июня 2010 года . Проверено 19 апреля 2009 .
  4. ^ Андони, Александр; Данилюк, Думитру; Хуршид, Сарфраз; Маринов, Дарко (2002). «Оценка гипотезы малого объема». CiteSeerX 10.1.1.8.7702 .  Цитировать журнал требует |journal=( помощь )

Внешние ссылки [ править ]

  • Сайт сплава
  • Репозиторий Alloy Github
  • Руководство по сплаву
  • Сайт системы анализа Kodkod в Массачусетском технологическом институте
  • Метамодель сплава в Ecore