2 Specifications: Rigorous and Formal

To build a system that satisfies users needs, we must understand these needs and precisely specify them. These specifications should serve as a contract for building a system. To be enforceable, contracts have to be precise and explicit. They have to specify semantics - as opposed to just signatures - without relying on implicit default knowledge, or on ``natural language'' (for the reasons eloquently expressed in [Dij96] and elsewhere). This has been acknowledged in industry: in particular, current activities within the Object Management Group, including but not restricted to its semantics working group (of the Object Model subcommittee), are concerned with exactly these issues. All too often, the only reliable semantics of the system has been provided by the implementation code, which was not understandable by humans; the very serious problems of such an approach are only too well-known. It is also well-known (e.g. from Dijkstra's work in the mid-1960s) how to make semantics understandable: use abstraction and separate concerns.

Semantics can be defined in a structured ``natural language" (examples include standards [ISO95a,ISO95c] - the subject of this paper), but, due to the inevitable ambiguity of natural language, a notation based on mathematics should be relied upon in cases of doubt. As the use and reuse of such a notation is the topic of our paper, some familiarity with the concepts of RM-ODP and with the Z specification language is assumed. Specifically, we will use object-oriented terminology as defined in [ISO95a,ISO95b,ISO,ISO95c] and try to explain any new terminology we introduce. We will also use names within their naming context (as specified in [ISO95a]) and especially distinguish object-oriented terminology from Z terminology whenever confusion is a danger, e.g. for ``type".

The very use of a formal notation forces specifiers to think and express themselves precisely and explicitly. The ease and efficiency of reasoning depends upon the language used [Dij96]. Although a formal specification can be unambiguously translated into stylized English and the result shown to the customer [ISO95c,KR94,KMS96,Red96], the reverse is not true. If the business semantics is not understood and specified properly, then a system specification cannot be checked for conformance with its business specification. The implementor will have to create both the system and the business specification as he understands it, usually leading to the expression of business semantics as ``business logic" in the application code. The Year 2000 problem is one example of the results.