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