3

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 specifications?

Gabriel Ščerbák
  • 18,240
  • 8
  • 37
  • 52
  • @Robert Harvey Unit tests are nice, but they are not formal specifications, they can be used only to proove concrete examples, not every possible combination of inputs and outputs. – Gabriel Ščerbák May 11 '10 at 23:27

1 Answers1

6

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

Jordi Cabot
  • 8,058
  • 2
  • 33
  • 39
  • 1
    Thank you, although your answer starts with "Yes", the result seems to be "No":) Could you provide some example of semantic variation being useful? I mean, why not to fully formalize UML? – Gabriel Ščerbák May 12 '10 at 09:35
  • 1
    Many people have tried to formalize the UML but all of them have failed (UML is too large and too complex). At most they have managed to formalize specific subsets by reexpressing UML in some formal language. – Jordi Cabot May 13 '10 at 22:33