The use of Functional Programming in the Specification and Testing Process
 
  1. Introduction
  2. The problem with formal specifications is that formal tools can only check that the specifications are internally consistent. No method is conceivable to automatically check that the specification expresses the intentions of the (collective) mind of the specification body, i.e., that it is correct. However, humans can easily detect if the result of an operation corresponds to their expectations. The idea of this paper is to show how this human capability can be exploited in the writing and testing of specifications for interoperable GIS.

    A problem related to that of deciding the correctness of specifications is that of checking the compliance of an implementation with a specification. It is practically (though not fundamentally) impossible to prove the compliance of a program with a specification, but one can test (with a limited set of examples) if an implementation produces no results prohibited by the specification.

    The same solution applies to both cases: if specifications are written in an executable language, they can be run and the results of specific test cases can be directly inspected. The results can be used to demonstrate and better understand what the specification means, and to check compliance of implementations. The paper applies this idea to the specification of semantics for interoperable components. It shows how the use of a functional language for specification writing (as explained in the companion paper, Frank and Kuhn) achieves the goal of unifying the specification and testing processes.
     

  3. Current Situation: a three-step specification process
  4. Today’s specifications formally describe the signatures of operations, assuming an implicit type system. The semantics of operations are typically expressed using first-order logic or natural language. Such expressions often assume the semantics of analytical geometry which are not supported by straight-forward implementations. They are difficult to combine and to understand in their collective meaning. It is not unusual that there is no implementation (i.e. no model) satisfying all of them. Operations from analytical geometry (e.g., line intersection or point equality) are notorious examples.

    Faced with these difficulties, current specification practice follows a three-step process:

    This separation of specification from testing is dangerous for the success of the whole process and potentially very expensive, because only phase three can reveal if an implementation is feasible or not. It has to be assumed that an implementation (a model, in terms of proof theory) exists. Even if such a model exists, it remains to be tested whether it does what the specifiers had in mind. And there is no guarantee at all that the semantics of the model have been specified such that ambiguities cannot endanger interoperability.
     
  5. Application of Proof Theory to Specification Writing
  6. Proof theory is the appropriate theoretical framework to discuss specifications and to improve the process:

    The relationship between theory and model is blurred in most specification and programming environments. Pure functional languages (Bird and Wadler 1988) with classes, like Haskell or Gofer (Peterson et al. 1996; Jones 1991), provide a clean and useful separation of the two levels.
     
  7. Executable Specifications
  8. If specifications can be executed, they can serve as prototypes for an implementation. This has tremendous advantages for the specification process, by moving the testing phase up to the specification writing phase and allowing for early error recognition and rectification.

    Writing specifications in an executable language, however, reduces them automatically to constructive expressions (of the kind of rewrite rules). This is a serious restriction, but it can be circumvented by expressing what cannot be stated in the theory as (constructive) test functions and supplementing the theory with a simplistic execution model. This model is not optimized for effective execution, but can demonstrate that an implementation is possible and support human understanding of what is going on in the specified operations.
     

  9. Demonstrating the Semantics of a Specification
  10. Executable specifications allow to compute results for any input data. They allow the specifier to observe if her intuition about what the specification should say corresponds to what the specification actually says. The specification can easily be distributed, so that any interested parties can submit test cases and convince themselves that the specification matches the collective understanding of the specification group.
     

  11. Compliance Testing
  12. Outcomes for test cases can be computed with an executable specification. These results can then be compared with the output for the same test cases from the implementation to be tested. An automated compliance test system can thereby be designed.

    If one has a hypothesis about a ‘wrong’ implementation, it is possible to produce specific test cases where the outcome from a ‘wrong’ implementation would be detectably different.
     

  13. Conclusions

  14. The processes of specification and compliance testing must be closely linked to avoid that the specification of semantics is effectively in the compliance testing program. Functional programming allows for such a close link. Pure functional languages with a class system separate the levels of theory and model. Thereby, they achieve both conceptual simplicity and practical utility for specification and testing.

    References

    Jones, M. P. (1991). An Introduction to Gofer, Yale University.

    OGC (1997). A compliance testing strategy. The Open GIS Consortium, Document 97-007. http://www.opengis.org.

    Peterson, J., K. Hammond, et al. (1996). Report on the functional programming language Haskell, Version 1.3. http://haskell.cs.yale.edu/haskell-report/haskell-report.html