Formal specifications and test: Correctness and oracle

  • Pascale Le Gall
  • Agnès Arnould
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1130)


This article presents a new formal approach to testing. In the field of dynamic testing, as soon as a program fails for a test set, it is flagged incorrect. The remaining question is: how far can a successful program be considered as correct? We give a definition of program correctness with respect to a specification which is adequate to dynamic testing. Similarly to the field of abstract implementation, the idea is that in order to declare a program as correct, it suffices that its behavior fulfills the specification requirements. An intermediate semantic level between the program and the specification, called the oracle framework, is introduced in order to interpret observable results obtained from dynamic experiments on the program. This allows to give algebraic semantics (i.e. a set of models) to the program, compatible with the program behavior. Program correctness is then defined by some adequacy criterion between the specification semantics and the program semantics. We point out that while for some specifications, there exist exhaustive test sets (the success of which means program correctness), for some other specifications, there only exist “complete” (but not exhaustive) test sets. Of course, all the programs rejected by a complete test set are incorrect but unfortunately, there still exist successful incorrect programs. We also explain how the test set selection can be formalized within our approach.


test against a specification axiomatic semantics behavioral theories program correctness oracle institutions test set selection hypothesis 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    M. Aiguier and G Bernot. Algebraic semantics of object type specifications. In R.J.Wieringa R.B.Feenstra eds, editor, Information Systems Correctness and Reusability, Selected papers from the IS-CORE workshop. World Scientific Publishing, 1995.Google Scholar
  2. 2.
    G. Bernot. Testing against formal specifications: a theoretical view. In TAPSOFT'91, Internationnal Joint Conference on the Theory and Practice of Software Developement, number 494 in Springer Verlag, LNCS, pages 99–119, 1991.Google Scholar
  3. 3.
    G. Bernot, M.C. Gaudel, and B. Marre. Software testing based on formal specifications: a theory and a tool. Software Engineering Journal, Vol.6(6):387–405, 1991. (also technical report LRI 581, Orsay (Avril 1991)).Google Scholar
  4. 4.
    G. Bernot and P. Le Gall. Exception handling and term labelling. In TAPSOFT'93, Internationnal Joint Conference, Theory And Practice of Software Developement, number 668 in Springer Verlag, LNCS, pages 421–436, 1993.Google Scholar
  5. 5.
    M. Bidoit, R. Hennicker, and M. Wirsing. Behavioural and abstractor specifications. Science of Computer Programming, 25:149–186, 1995.Google Scholar
  6. 6.
    E. Brinksma, J. Tretmans, and L. Verhaard. A framework for test selection. In Procol Specification, Testing, and Verification XI, North Holland, 1991.Google Scholar
  7. 7.
    M. Cerioli and G. Reggio. Institutions for very abstract specifications. In LNCS, editor, Recent Trends in Data Type Specification, volume 785, pages 113–127, 1994.Google Scholar
  8. 8.
    P. Dauchy, M.-C. Gaudel, and B. Marre. Using algebraic specifications in software testing: a case study on the software of an automatic subway. Journal of Systems and Software, 21(3):229–244, 1993.Google Scholar
  9. 9.
    H. Ehrig and B. Mahr. Fundamentals of Algebraic Specification 1. Equations and initial semantics, volume 6. Springer-Verlag,EATCS Monographs on Theoretical Computer Science, 1985.Google Scholar
  10. 10.
    M.C. Gaudel. Testing can be formal, too. TAPSOFT'95, Theory and Practice of Software Developement, 6th International Joint Conference, CAAP/FASE, Aarhus, Denmark, LNCS 915, 1995.Google Scholar
  11. 11.
    J.A. Goguen and R.M. Burstall. Introducing institutions. In Springer-Verlag LNCS 164, editor, Proc. of the Workshop on Logics of Programming, pages 221–256, 1984.Google Scholar
  12. 12.
    R. Hennicker. Context induction: a proof principle for behavioural abstractions and algebraic implementations. Formal Aspects of Computing, 3(4):326–345, 1991.Google Scholar
  13. 13.
    P. Le Gall. Les algèbres étiquetées: une sémantique pour les spécifications algébriques fondée sur une utilisation systématique des termes. Application au test de logiciel avec traitement d'exceptions. Phd, Université de Paris XI, 1993.Google Scholar
  14. 14.
    B. Marre. Toward automatic test data set selection using Algebraic Specifications and Logic Programming. mEigth International Conference on Logic Programming, ICLP'91, Paris, 25–28, MIT Press, 1991.Google Scholar
  15. 15.
    B. Marre, P. Thevenod, H. Waeselynk, P. Le Gall, and Y. Crouset. An experimental evaluation of formal testing and statistical testing. In SAFECOMP'92, Actes Safety of Computer Control System 1992, Pergamon Press”, 1992.Google Scholar
  16. 16.
    M. Phalippou. Relations d'implantation et hypothèses de test sur des automates à entrées et sorties. Phd, Université de Bordeaux, 1994.Google Scholar
  17. 17.
    D.J. Richardson, S. Aha, and T. Owen O'Malley. Specification-based test oracles for reactive systems. In Proceedings of the 14th International Conference on Software Engineering, pages 105–118, 1992.Google Scholar
  18. 18.
    D. Sannella and A. Tarlecki. Toward formal development of programs from algebraic specification: implementation revisited. Acta Informatica, 25:233–281, 1988.Google Scholar
  19. 19.
    P. Stocks and D.A. Carrington. Test template framework: A specification-based testing framework. In Proceedings of the 15th International Conference on Software Engineering, pages 405–414, 1993.Google Scholar
  20. 20.
    E.J. Weyuker. On testing non testable programs. In The Computer Journal 25, pages 465–470, 1982.Google Scholar
  21. 21.
    M. Wirsing. Algebraic Specification. Handbook of Theoretical Computer Science, vol B, the MIT Press, 1990.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1996

Authors and Affiliations

  • Pascale Le Gall
    • 1
  • Agnès Arnould
    • 2
  1. 1.Cours Monseigneur RoméroL.a.M.I., Université d'ÉvryEvry CedexFrance
  2. 2.L.R.I, URA 410, Bât 490, Université de Paris XIOrsay CedexFrance

Personalised recommendations