Requirements Engineering Formal Analysis of the Shlaer-Mello(9)

In this paper, we define a number of tools that we think belong to the core of any toolkit for requirements engineers. The tools are conceptual and hence, they need precise definitions that lay down as exactly as possible what their meaning and possible us

more. This is formalised by maintaining a unary predicate Used that is true for all identifiers that have ever been added to the existence set. The extension of this predicate is nondecreasing. Figure 3 shows an example of a formalisation of part of the information model in Fig. 1 in LCM. The specification of object class H O M E is syntactic sugar for the declaration of an identifier type H O M E and of functions address : H O M E ~ S T R I N G etc. The set of attributes {address, unit at address} is declared to be a key. This is syntactic sugar for an axiom which says that if two existing homes have the same value for this set of attributes, then they are equal:address(hi) = address(h2) and unit at address(hi) = unit at address(h2) ~" h l = h2begin object class HOME attributes address : STRING; unit at address : STRING; square_fee~ : NATURAL; property_tax fee :MONEY; keys address, unit at_address; end object class HOME; begin object class HOME_0WNEK attributes owner_name : STRING; addres : STRING; keys owner_name; end object class HOME_0WNER; begin link class OWNERSHIP components home : HOME; owner : HOME_OWNER; attributes date_purchased : DATE; end link class OWNERSHIP;Fig. 3. Specification of a relationship with attributes in LCM,where -~ stands for logical implication. Note that we formalize the identifier concept of O O A as keys in LCM. A relationship instance is a labelled tuple of component objects called a link in LCM; a relationship is called a link class in LCM. The specification of a link class must declare the components of the links. The components section of the specification of O W N E R S H I P is syntactic sugar for the specification of an identifier type whose values have the followingstructure:< home: h, owner: o > where h and o are identifiers of type H O M E and HOMEOWNER, respectively. The labels h o m e and owner in the link are the names of projection functions that retrieve the components of these identifiers. These projection functions are called component functions in LCM. Thus, we have a functionhome: O W N E R S H I P -~ H O M Edefined byh o m e (< home: h, owner: o >) = h The components section generates implicit component existence axioms such as the following:112R.J. Wieringa and G. Saakeforall os : O W N E R S H I P :: Exists(os) ~ (home(os))Exists-Cardinality constraints are formalised by placing constraints on the component functions of a link class. For example, if each existing H O M E must participate in an existing O W N E R S H I P link, then the home component function is declared to be a surjection and if each existing H O M E must participate in at most one link, then the component function home is declared to be an injection. The axioms for this are straightforward and are omitted here. Attributes applicable to relationships are formalized as functions that take link identifiers as arguments. For example, the date attribute of an O W N E R S H I P instance is a function O W N