Я использовал Alloy в нескольких проектах и нашел его полезным; в некоторых, но не во всех этих проектах я смог убедить других использовать также Alloy или, по крайней мере, работать с теми моделями Alloy, которые я написал. Эти проекты могут или не могут быть тем, что вы имеете в виду, когда просите о проектах «реального мира», но они, безусловно, имели место в той части реального мира, в которой я работаю.
В 2006 и 2007 годах я создал частичную модель Alloy для тогдашнего чернового варианта спецификации W3C XProc; насколько я могу судить, большинство членов рабочей группы никогда не читали статью, которую я написал (на http://www.w3.org/XML/XProc/2006/12/alloy-models/models.html); они сказали: «О, мы изменили эту часть спецификации на прошлой неделе, так что то, что говорит модель, больше не является релевантный ". Но в статье удалось убедить редактора спецификации, что абстрактный уровень" компонента ", описанный в первом проекте спецификации, был крайне недооценен и должен быть либо полностью определен, либо отброшен. Он отбросил его с помощью (I думаю) хорошие результаты для удобочитаемости и удобства использования спецификации.
В 2010 году я сделал модель Alloy для модели данных XPath 1.0 , которая выявила некоторые недостатки в спецификации. Реакция большинства заинтересованных сторон (включая рабочую группу W3C, ответственную за поддержку спецификации XPath 1.0), к сожалению, не вызывает оптимизма.
Исследовательский проект, с которым я связан, использовал Alloy для моделирования MLCD Overlap Corpus, коллекции образцов документов и связанной с ними информации, которую мы создаем (гиперссылки подавлены по настоянию SO); Модель Alloy нашла несколько ошибок в нашем первоначальном проекте для каталога корпуса, поэтому она того стоила.
И мы также использовали Alloy, чтобы формализовать некоторую работу по моделированию, которую мы проделали над характером транскрипции и расширением различия типа / токена в структуре документа (для нашей статьи, посмотрите материалы 2010 года по Balisage: The Markup Конференция). Это лежит немного за пределами обычной области применения Alloy, поскольку не имеет ничего общего с дизайном программного обеспечения, но способность Alloy проверять согласованность моделей и генерировать экземпляры неоценима, поскольку показывает нам некоторые логические последствия той или иной возможной аксиомы. для нашей модели.
Чтобы ответить на ваши конкретные вопросы: да, Alloy помог мне определить более чистые модели доменов, и да, он обнаружил ошибки и глюки. Они часто бывают небольшими по причинам, которые Даниэль Джексон объясняет в своей книге Абстракции программного обеспечения : во-первых, если вы используете модели во время проектирования, вы рано обнаруживаете ошибки, когда все все еще мало. И, во-вторых (по словам Джексона): «Оглядываясь назад, большинство проблем разработки программного обеспечения тривиальны».
Он продолжает: «Но если вы не решите их в лоб, у тривиальных проблем есть неприятная привычка становиться нетривиальными». Мой опыт наглядно подтверждает это. Намного лучше, чтобы предотвратить такие проблемы рано. Так что да, я снова буду использовать Alloy.