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
-- effect a x i o m for a c c e p t _ c h e c k f o r a l l a : A C C O U N T , b, m : M O N E Y balance(a) = b ->m)] balance(a)= b-m;and m <= balance(a); :: m)] balance(a) = b-m;[accept_check(a;--- g u a r d i n g a x i o m for r e f u s e _ c h e c k f o r a l l a : A C C O U N T , m : MONEY :: < r e f u s e check(a; m ) > t r u e -> m > balance(a); --- effect axioms for refuse check f o r a l l a : A C C O U N T , b, m : MONEY :: b a l a n c e ( a ) = b and fee > b -> [refuse check(a; m)] balance(a) = b-fee and current state(a)=0VERDRAWN; f o r a l l a : A C C O U N T , b, m : MONEY :: b a l a n c e ( a ) = b and Fee >= b -> [refuse check(a; m)] balance(a) = b-fee and c u r r e n t _ s t a t e ( a ) = I N ~ G O G D _ S T A N D I N O ;Fig. 13. Transition axioms for the ACCOUNT object class.Formal Analysis of the Shlaer-Mellor Method1239 Within a single object, a transition axiom may change several local attributes and:predicates. The simplest assumption here is to assume that any attribute and predicate that does not occur in the postcondition remains unchanged. For example, we can add ttie axiom that increase_balance does not change the attribute customer_ID. The problem with this approach is that some transitions may imply derived updates of the object state. We have~sl, iown elsewhere how to deal with this when derivation rules have the form of Horn clauses [50]. We are currently looking at ways to generalise this approach. 9 The qualification assumption can be formalised in a simple way by conjoining~all guards of a transition and declaring these necessary as well as sufficient for a transition to be possible. This is a kind of "guard completion". The problem with this is that in a speciatisation of the class, additional guards may be specified for the transition. The solution to this is to apply guard completion only to the most specific classes, where all constraints on a transition are known. Returning to the formalisation of the OOA techniques, we remark that the state model of a class is formalised simply by introducing a state variable and updating this variable in the effect axioms. The actions performed by a state model appear as transitions in the LCM specification and the effect axioms define the effect of these actions on the local state o f t h e object. The effect axioms thus provide the essential information about object transactions as represented in the essential data flow model of these transactions. Finally, the guard axioms formalise the guards that we. added to the statemodels in our methodological analysis of Section 4. The informal specifications of object transactions such as shown in Fig. 11 are really paraphrases of the effect and guard axioms. Note that in the formalisation we do not distinguish input from output parameters of actions; this is extra information provided by the essential data flow diagram that may be useful to the programmer who.implements the transaction. This leaves the communic