Я спрашиваю, потому что UML используется для неофициальных спецификаций и имеет некоторую двусмысленность в своей семантике. Однако я думаю, что OCL можно использовать для указания условий до/после, инвариантов и других ограничений достаточно эффективно.
Недавно я столкнулся с обозначением Z и алгебраическими спецификациями. Мой вопрос: достаточно ли комбинации UML и OCL для формальных спецификаций?
Да, для большинства систем, которые вы можете построить.
Я имею в виду, что UML и OCL — это только полуформальные языки (их синтаксис четко определен, но их семантика формализована лишь частично, многие аспекты просто описаны на естественном языке в стандартных спецификациях документов). Таким образом, если вы строите критическую систему и вам нужно доказать правильность системы, то UML/OCL может оказаться недостаточным, но для многих других типов систем формальности, которые может обеспечить UML/OCL, достаточно хороши.
