Testing from Structured Algebraic Specifications

  • Patrícia D. L. Machado
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1816)


This paper deals with testing from structured algebraic specifications expressed in first-order logic. The issue investigated is the so- called oracle problem, that is, whether a finite and executable procedure can be defined for interpreting the results of tests. For flat specifications, the oracle problem often reduces to the problem of comparing values of a non-observable sort and how to deal with quantifiers. How ever, specification-building operations introduce an additional barrier to this problem which can restrict the way specifications and test suites are defined. In this paper, we present a framework for testing from structured specifications and a thorough discussion of the problems which can arise together with proposed solutions.


Checkable Model Structure Testing Approximate Equality Ground Term Behavioural Equality 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    G. Bernot. Testing Against Formal Specifications: a Theoretical View. In S. Abramsky and T.S.E. Maibaum, eds., TAPSOFT’91, LNCS 494. Springer, 1991.Google Scholar
  2. 2.
    M. Bidoit, M. V. Cengarle, and R. Hennicker. Proof Systems for Structured Specifications and Their Refinements, chapter 11. IFIP Reports. Springer, 1999.Google Scholar
  3. 3.
    M. Bidoit and R. Hennicker. Behavioural Theories and the Proof of Behavioural Properties. Theoretical Computer Science, 165(1):3–55, 1996.zbMATHCrossRefMathSciNetGoogle Scholar
  4. 4.
    R. Burstall and J. Mckinna. Deliverables: an Approach to Program Development in the Calculus of Constructions. ECS-LFCS-91-133, Edinburgh University, 1992.Google Scholar
  5. 5.
    J. Dick and A. Faivre. Automating the Generation and Sequencing of Test Cases from Model-based Specifications. In J. Wookcook and P. Larsen, eds., FME’93, LNCS 670. Springer, 1993.Google Scholar
  6. 6.
    J. Farrés-Casals. Proving correctness w.r.t. specifications with hidden parts. In H. Kirchner and W. Wechler, eds., Alg. and Logic Prog., LNCS 463. Springer, 1990.Google Scholar
  7. 7.
    P. Le Gall and A. Arnould. Formal Specification and Test: Correctness and Oracle. In M. Haveraaen, O. Owe, and O. Dahl, eds., Recent Trends in Data Type Specifocation, LNCS 1130. Springer, 1996.Google Scholar
  8. 8.
    M. Gaudel. Testing can be formal, too. In P. D. Mosses, M. Nielsen, and M. I. Schwartzbach, eds., TAPSOFT’95, LNCS 915. Springer, 1995.Google Scholar
  9. 9.
    R. Hennicker. Structured Specifications with Behavioural Operators: Semantics, Proof Methods and Applications. Habilitation thesis, Institut fur Informatik, Ludwig-Maximillians-Universitat Munchen, Munchen, Germany, june 1997.Google Scholar
  10. 10.
    Stefan Kahrs and Donald Sannella. Reflections on the design of a specification language. In E. Astesiano, ed., FASE’98, volume 1382 of LNCS. Springer, 1998.Google Scholar
  11. 11.
    P. D. L. Machado. On Oracles for Interpreting Test Results against Algebraic Specifications. In A. Haeberer, ed., AMAST’98, LNCS 1548. Springer, 1999.Google Scholar
  12. 12.
    D. Mandrioli, S. Morasca, and A. Morzenti. Generating test cases for real-time systems from logic specifications. ACM Trans. Comp. Syst., 13(4):365–398, 1995.CrossRefGoogle Scholar
  13. 13.
    M. Wirsing. Algebraic specification. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, chapter 13, pages 675–788. Elsevier, 1990.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2000

Authors and Affiliations

  • Patrícia D. L. Machado
    • 1
  1. 1.LFCS, Division of InformaticsUniversity of Edinburgh, JMCBEdinburghUK

Personalised recommendations