Formal Methods, UML and OCL

I am now studying formal methods wherein I have come across something interesting I thought I could share with people.

Formal Methods is the application of logic to the development of "correct" systems. They are mathematical foundations for many technologies and practices that software engineers use. Joseph Goguen says that formal methods are “syntactic in essence but semantic in purpose.” A more narrower definition could be "A formal method in software development is a method that provides a formal language for describing a software artifact (e.g. specifications, designs, source code) such that formal proofs are possible, in principle, about properties of the artifact so expressed."

UML is one of the tools Engineers use to design more formal systems. This language fits Goguen’s description of a formal method. It is syntactic in essence, offering a well-defined way to construct a model. It is also semantic in purpose — that is, it is designed to convey meaning. Much information can be encoded in a UML model. But it is not always easy to construct syntactically correct and semantically rich models of software using just UML diagrams. The rules for which type of arrowhead and which type of connector to use for which purpose can be just as confusing as the syntax for a programming language such as Java. And then, even if you can construct a correct UML diagram, there is much information that it will not convey.
However, OCL, a formal specification language that is part of the UML specification, enables you to annotate models with expressions that clarify meaning. In UML 1.1, the main purpose of OCL was to identify the constraints on model elements. More on this...