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

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

ture for the formal details [35-37] and here give an informal indication of what this means. 9 An A D T is a set, called a sort, with a number of operations. 9 ADTs are partially ordered to represent the subtype relation on ADTs. The subtype relation implies a subset relation on sorts. For example, in the partial ordering of number types N A T U R A L < INTEGER represents the fact that N A T U R A L is a subtype of INTEGER; this implies that the sort of naturals is a subset of the sort of integers. 9 The properties of operations are given by means of equations. For example, a property of addition on the sort N A T U R A L is that succ(n + m) = succ(n) + m, where succ is the successor function. 9 Further properties can be derived using equational logic, which is based on the substitution of equals for equals. 9 Each closed term (a term not containing variables) is the syntactic representation of a value. In the initial algebra semantics, all values are named by a closed term and different closed terms represent the same value if and only if they can be proved equal by usingFormal Analysis of the Shlaer-Mellor Method111the axioms in the specification and the rules of equational logic. We define the extension of an A D T as the set of all instances of the type in the intended semantics (in our case, in the initial algebra semantics); this is the set of all values that can be denoted by a closed term. Next, we need to formalise the concept of class. The idea is simply to formalise each attribute as a function that accepts an object identifier as argument and delivers an attribute value as result. The methodological consequence of this idea is that identifiers are themselves not attributes and that objects can never change identifiers. This agrees with our methodological analysis. In the formal specification, we now require for each object class that a corresponding identifier type has been specified, contains all identifiers that will ever be needed for objects of that class. The identifier type has the same name as the class. Each attribute is now formally declared to be a function on the identifier type of the class. For example, if we assume in Fig. 1 the name of a customer is a string, owner_name is a function H O M E O W N E R -~ S T R I N G . In any state of the system only some identifiers will identify existing objects. To single out those identifiers, we assume a predicate Exists that is applicable to all identifiers and that only evaluates to true for identifiers of existing objects. The extension of the Exists predicate is the set of identifiers for which it evaluates to true. Exists may have different extensions in different states. The existence set of a state is the set of all identifiers for which Exists evaluates to true. If Exists(n) is false for an identifier n then n may have existed in the past or it may come into existence in some possible future. If it has existed in the past, it is not available for use as identifier any