Да, Сплав - это фальсификатор.Основная новинка Alloy, когда она была представлена 20 лет назад, заключалась в том, чтобы утверждать, что фальсификация часто более важна, чем проверка, поскольку большинство конструкций не являются правильными, поэтому роль анализатора должна заключаться в том, чтобы находить ошибки, а не показывать, что их нет,Обсуждение этой проблемы см. В разделе 1.4 «Проверка и опровержение» в Анализ программного обеспечения: дорожная карта (Джексон и Ринард, 2000);Раздел 5.1.1, Нахождение экземпляров и компромиссы неразрешимости в программных абстракциях (Jackson 2006).
В случае Alloy, однако, есть еще один аспект, который является аргументом, что на самом деле полный анализдовольно эффективно с точки зрения проверки.Это утверждение является тем, что мы назвали «гипотезой малого объема» - что большинство ошибок можно найти в небольших областях (то есть анализах, которые ограничены небольшим фиксированным числом элементов в каждом базовом типе).
КстатиAlloy был одним из первых инструментов, предложивших использовать SAT для ограниченной проверки.См., Например, Булева компиляция реляционных спецификаций (Дэниел Джексон, 1998), технический отчет, который был известен авторам первой ограниченной бумаги для проверки моделей, в которой обсуждается предшественник Alloy, Nitpick, в следующемусловия:
гипотеза, лежащая в основе придираться является спорным.Дело в том, что на практике достаточно небольших областей применения.Другими словами, большинство ошибок может быть продемонстрировано контрпримерами в небольшом объеме.Это чисто эмпирическая гипотеза, поскольку соответствующее распределение ошибок не может быть описано математически: оно определяется спецификациями, которые пишут люди.
Мы надеемся, что успешное использование инструмента Nitpick оправдает гипотезу.Уже есть некоторые доказательства его правдоподобия.По нашему опыту работы с Nitpick на сегодняшний день мы не получили дополнительную информацию, расширив область действия до 6.
Подобное понятие области применения подразумевается в контексте проверки модели оборудования.Хотя отдельные конечные автоматы обычно конечны, дизайн часто параметризуется количеством машин, выполняющихся параллельно.Эта метрика аналогична области;с увеличением числа машин пространство состояний экспоненциально увеличивается, и редко можно проанализировать систему, в которой задействовано более нескольких машин.К счастью, однако, кажется, что для поиска ошибок требуются только небольшие конфигурации.Знаменитый анализ протокола кэширования Futurebus + [C + 95], который, возможно, стал поворотным моментом в промышленной проверке модели, был выполнен для 8 процессоров и 3 шин.Однако сообщенные недостатки могут быть продемонстрированы на контрпримерах, включающих не более 3 процессоров и 2 шин.