Можно ли использовать UML с OCL для формальных спецификаций?

Question

Я спрашиваю, потому что UML используется для неформальных спецификаций и имеет некоторую неопределенность в своей семантике. Тем не менее, я думаю, что OCL может использоваться для указания условий до и после, а также инвариантов и других ограничений достаточно эффективно.

Я недавно столкнулся с обозначениями Z и алгебраическими спецификациями. Мой вопрос, достаточно ли сочетания UML и OCL для формальных спецификаций?

Answer 1

Да, для большинства систем, которые вы можете построить.

Я имею в виду, что UML и OCL являются лишь полуформальными языками (их синтаксис четко определен, но их семантика формализована лишь частично, многие аспекты просто описаны на естественном языке в спецификациях стандартных документов). Следовательно, если вы создаете критическую систему и вам необходимо доказать ее корректность, тогда UML / OCL может не сработать, но для многих других типов систем такой тип формальности, который может обеспечить UML / OCL, достаточно хорош