Can UML with OCL be used for formal specifications?

I am asking because UML is used for informal specifications and has some ambiguities in its semantics. However OCL can be used to specify pre/post conditions and invariants and other constraints quite efficiently I think.

I encountered the Z notation and algebraic specifications recently. My question, is combination of UML and OCL sufficient for formal s开发者_开发技巧pecifications?

Yes, for most of the systems you can build.

I mean, UML and OCL are only semi-formal languages (their syntax is well-defined but their semantics is only partially formalized, many aspects are just described in natural language in the standard document specifications). Therefore, if you are building a critical system and you need to prove the correctness of the system then UML/OCL may fall short but for many other kinds of systems, the kind of formality that UML/OCL can provide is good enough