A UML com OCL pode ser usada para especificações formais?

Question

Estou perguntando porque a UML é usada para especificações informais e tem algumas ambiguidades em sua semântica. No entanto, a OCL pode ser usada para especificar condições pré/pós -pós -invariantes e outras restrições com bastante eficiência, eu acho.

Recentemente, encontrei as especificações Z e algébricas Z. Minha pergunta, a combinação de UML e OCL é suficiente para especificações formais?

Answer 1

Sim, para a maioria dos sistemas que você pode construir.

Quero dizer, a UML e o OCL são apenas idiomas semi-formais (a sintaxe deles é bem definida, mas sua semântica é apenas parcialmente formalizada, muitos aspectos são descritos na linguagem natural nas especificações de documentos padrão). Portanto, se você estiver construindo um sistema crítico e precisar provar a correção do sistema, o UML/OCL pode ficar aquém, mas para muitos outros tipos de sistemas, o tipo de formalidade que a UML/OCL pode fornecer é bom o suficiente