ISBN : 978-81-963532-2-3 (E-Book) Limitations of formal requirements specification It is clear that formal methods provide mathematically sound frameworks within large, complex systems can be specified, developed and verified in a systematic rather than in an ad hoc manner. However, formal methods suffer from several shortcomings, some of which are the following: • Formal methods are difficult to learn and use. • The basic incompleteness results of first-order logic suggest that it is impossible to check absolute correctness of systems using theorem proving techniques. • Formal techniques are not able to handle complex problems. This shortcoming results from the fact that, even moderately complicated problems blow up the complexity of formal specification and their analysis. Also, a large unstructured set of mathematical formulas is difficult to comprehend. Axiomatic Specification In axiomatic specification of a system, first-order logic is used to write the pre and postconditions to specify the operations of the system in the form of axioms. The preconditions basically capture the conditions that must be satisfied before an operation can successfully be invoked. In essence, the pre-conditions capture the requirements on the input parameters of a function. The post-conditions are the conditions that must be satisfied when a function completes execution for the function to be considered to have executed successfully. Thus, the post- conditions are essentially constraints on the results produced for the function execution to be considered successful. The following are the sequence of steps that can be followed to systematically develop the axiomatic specifications of a function: • Establish the range of input values over which the function should behave correctly. Also find out other constraints on the input parameters and write it in the form of a predicate. • Specify a predicate defining the conditions which must hold on the output of the function if it behaved properly. 33 Software Engineering Keerthana P, Manasa KN, Ganga D Bengal
39 Publizr Home