-. The involvement of the client for the software decreases and the involvement of the contractor 
   increases as the specification is developed.    
   -. Error detection is the most potent argument for developing a formal specification.

   9.1 Formal specification on trial
       
       -. A formal software specification is a specification expressed in a language whose vocabulary, 
       syntax and semantics are formally defined. 
       
       9.1.1 The case against formal specification
          -. There have been various reasons put forward as to why formal specification and formal 
          development methods have not been widely used :
                +. Software management is ingerently conservative and is unwilling to adopt new techniques
                 for which payoff is not obvious. Is is difficult to demonstrate that the relatively high cost of 
                developing a formal system specification will reduce overall software development costs.
                +. Many software engineers, particularly those in senior positions, have not been trained in the
                 techniques required to develop formal software specifications.
                +. System customers are unlikely to be familiar with formal specification techniques.
                +. Some classes of software system are difficult to specify using existing techniques.
                +. There is widespread ignorance of the practicality of current specification techniques and their
                 applicability.
                +. Most of the effort in specification research has been concerned with the development of 
                 languages and their theoretical underpinnings.
       9.1.2 The case for formal specification   
           -. The reason set out above for the lack of use of formal methods are nostly based on the problems 
            of introducing formal specifications into current software processes.
           -. In an excellent article, Hall(1990) directly refutes some of the arguments against the use of formal 
            methods where he presents 'seven myths of formal methods'. These myths, and the arguments 
            against them, are :
                +. Perfect software results from the use of formal methods.
                +. Formal methods mean program proving.
                +. Formal methods are so expensive that their use can only 
                  be justified in safety-critical systems.
                +. Formal methods require a high level of mathematical skill.
                +. Formal methods increase development costs.
                +. Customers cannot understand formal specifications.
                +. Formal methods have only been used for tricial system 
                  development.
        
       9.1.3 The verdict    
           -. Changes to the market and to software engineering practice have probably been more significant 
            in the rejection of formal methods by large sections of the software engineering community. 
            These changes are :
                +. The move to interactive systems.
                +. Successful software engineering.
           -. Another area where the use of formal specifications is likely to develop is in the area of standards definition.
   
   9.2 Transformational develoment       
       -. Each transformation is sufficiently close to the previous description that the effort of verifying the transformation 
        is not excessive.
   
   9.3 Specifying functional abstractions    
       -. Functions may be specified using pre- and post-conditions.
       -. A pre-condition is a specification of a condition which always holds for the function's inputs.
       -. A post-condition is a specification of the corresponding condition for the function's outputs.
       -. An alternative approach is used in the Larch specification language.
       -. Pre- and post-conditions are predicates over the inputs and outputs of a function.
       -. The development of a specification of a function using pre- and post-conditions involves a number of stages :
                +. Establish the range of the input paramenters over which the function should behave correctly.
                +. Specify a predicat defining a condition which must hold on the output of the function if it behaves correctly.
                +. Establish what changes (if any) are made to the function's inputs but programming langyages usually allow 
                  function inputs to be modified by passing then by reference.
                +. Combine these into pre- and post-conditions for the function.
       -. The function pre-condition states the condition which must hold if the post-condition is to be valid.
       -. The number of possible types of error and whether the error action depends on the error type affects the approach 
        used for error specification.
       -. There are two approaches to formal specification that have been used to develop relatively complex systems :
                +. An algebraic approach whereby the system is described in terms of operations and their relationships.
                +. A model-based approach whereby a model of the system is constructed using well-understood 
                 mathematical entities such as sets and sequences.