Discovering Algebraic Specifications from Java Classes

  • Johannes Henkel
  • Amer Diwan
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2743)


We present and evaluate an automatic tool for extracting algebraic specifications from Java classes. Our tool maps a Java class to an algebraic signature and then uses the signature to generate a large number of terms. The tool evaluates these terms and based on the results of the evaluation, it proposes equations. Finally, the tool generalizes equations to axioms and eliminates many redundant axioms. Since our tool uses dynamic information, it is not guaranteed to be sound or complete. However, we manually inspected the axioms generated in our experiments and found them all to be correct.


Java Classis Primitive Type Reference Equality State Array Abstract Data Type 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Ammons, G., Bodik, R., Larus, J.R.: Mining specifications. In: Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 4–16 (2002)Google Scholar
  2. 2.
    Angluin, D.: Inference of reversible languages. Journal of the ACM (JACM) 29(3), 741–765 (1982)zbMATHCrossRefMathSciNetGoogle Scholar
  3. 3.
    Antoy, S.: Systematic design of algebraic specifications. In: Proceedings of the Fifth International Workshop on Software Specification and Design, Pittsburgh, Pennsylvania (1989)Google Scholar
  4. 4.
    Antoy, S., Hamlet, D.: Automatically checking an implementation against its formal specification. IEEE Transactions on Software Engineering 26(1) (January 2000)Google Scholar
  5. 5.
    Astesiano, E., Kreowski, H.-J., Krieg-Brückner, B. (eds.): Algebraic Foundations of Systems Specification. Springer, Heidelberg (1999)Google Scholar
  6. 6.
    Bartussek, W., Parnas, D.L.: Using assertions about traces to write abstract specifications for software modules. In: Bracchi, G., Lockemann, P.C. (eds.) ECI 1978. LNCS, vol. 65, Springer, Heidelberg (1978)Google Scholar
  7. 7.
    Biermann, A.W.: On the inference of turing machines from sample computations. Artificial Intelligence 3, 181–198 (1972)zbMATHCrossRefMathSciNetGoogle Scholar
  8. 8.
    Biermann, A.W.: The inference of regular Lisp programs from examples. IEEE Transactions on Systems, Man, and Cybernetics 8, 585–600 (1978)zbMATHCrossRefMathSciNetGoogle Scholar
  9. 9.
    Biermann, A.W., Krishnaswamy, R.: Constructing programs from example computations. IEEE Transactions on Software Engineering 2(3), 141–153 (1976)CrossRefMathSciNetGoogle Scholar
  10. 10.
    Boyapati, C., Khurshid, S., Marinov, D.: Korat: Automated testing based on java predicates. In: International Symposium on Software Testing and Analysis, Rome, Italy (July 2002)Google Scholar
  11. 11.
    Buy, U., Orso, A., Pezze, M.: Automated testing of classes. In: Proceedings of the International Symposium on Software Testing and Analysis, Portland, Oregon (2000)Google Scholar
  12. 12.
    Chen, H.Y., Tse, T.H., Chan, F.T., Chen, T.Y. In black and white: An integrated approach to class-level testing of object oriented programs. ACM Transactions on Software Engineering 7(3) (July 1998)Google Scholar
  13. 13.
    Dodoo, N., Donovan, A., Lin, L., Ernst, M.D.: Selecting predicates for implications in program analysis (March 2002),
  14. 14.
    Doong, R., Frankl, P.G.: The ASTOOT approach to testing object-oriented programs. ACM Transactions on Software Engineering 3(2) (April 1994)Google Scholar
  15. 15.
    Ernst, M.D., Cockrell, J., Griswold, W.G., Notkin, D.: Dynamically discovering likely program invariants to support program evolution. ACM Transactions on Software Engineering 27(2), 1–25 (2001)Google Scholar
  16. 16.
    Ernst, M.D., Czeisler, A., Griswold, W.G., Notkin, D.: Quickly detecting relevant program invariants. In: Proceedings of the 22nd International Conference on Software Engineering, pp. 449–458 (June 2000)Google Scholar
  17. 17.
    Ernst, M.D., Griswold, W.G., Kataoka, Y., Notkin, D.: Dynamically discovering program invariants involving collections. TR UW-CSE-99- 11-02, University of Washington (2000) (revised version of March 17, 2000)Google Scholar
  18. 18.
    Gannon, J., McMullin, P., Hamlet, R.: Databstraction implementation, specification and testing. ACM Transactions on Programming Languages and Systems 3(3), 211–223 (1981)CrossRefGoogle Scholar
  19. 19.
    Graves, T.L., Harrold, M.J., Kim, J.-M., Porter, A., Rothermel, G.: An empirical study of regression test selection techniques. ACM Transactions on Software Engineering and Methodology (TOSEM) 10(2), 184–208 (2001)zbMATHCrossRefGoogle Scholar
  20. 20.
    Gries, D.: The science of programming. Texts and monographs in computer science. Springer, Heidelberg (1981)zbMATHGoogle Scholar
  21. 21.
    Guttag, J.V., Hornig, J.J., Garland, S.J., Jones, K.D., Modet, A., Wing, J.M.: Larch: Languages and Tools for Formal Specification. Springer, Heidelberg (1993) (out of print)zbMATHGoogle Scholar
  22. 22.
    Guttag, J.V., Horning, J.J.: The algebraic specification of abstract data types. Acta Informatica 10, 27–52 (1978)zbMATHCrossRefMathSciNetGoogle Scholar
  23. 23.
    Hangal, S., Lam, M.S.: Tracking down software bugs using automatic anomaly detection. In: Proceedings of the International Conference on Software Engineering, pp. 291–301 (May 2002)Google Scholar
  24. 24.
    Harder, M., Morse, B., Ernst, M.D.: Specification coverage as a measure of test suite quality, Septermber 25 (2001)Google Scholar
  25. 25.
    Hardy, S.: Synthesis of Lisp functions from examples. In: Proceedings of the Fourth International Joint Conference on Artificial Intelligence, pp. 240–245 (1975)Google Scholar
  26. 26.
    Helm, R., Holland, I.M., Gangopadhyay, D.: Contracts: specifying behavioral compositions in object-oriented systems. In: Proceedings of the European conference on object-oriented programming on Object-oriented programming systems, languages, and applications, pp. 169–180. ACM Press, New York (1990)CrossRefGoogle Scholar
  27. 27.
    Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of the ACM 12(10), 576–580 (1969)zbMATHCrossRefGoogle Scholar
  28. 28.
    Van Horebeek, I., Lewi, J.: Algebraic specifications in software engineering: an introduction. Springer, Heidelberg (1989)Google Scholar
  29. 29.
    Hughes, M., Stotts, D.: Daistish: Systematic algebraic testing for OO programs in the presence of side-effects. In: Proceedings of the International Symposium on Software Testing and Verification, San Diego, California (1996)Google Scholar
  30. 30.
    Janicki, R., Sekerinski, E.: Foundations of the trace assertion method of module interface specification. ACM Transactions on Software Engineering 27(7) (July 2001)Google Scholar
  31. 31.
    Jeng, B., Weyuker, E.J.: A simplified domain-testing strategy. ACM Transactions on Software Engineering 3(3), 254–270 (1994)CrossRefGoogle Scholar
  32. 32.
    Kataoka, Y., Ernst, M.D., Griswold, W.G., Notkin, D.: Automated support for program refactoring using invariants. In: International Conference on Software Maintenance, Florence, Italy (2001)Google Scholar
  33. 33.
    Lin, H.: Procedural implementation of algebraic specification. ACM Transactions on Programming Languages and Systems (1993)Google Scholar
  34. 34.
    Martena, V., Orso, A., Pezze, M.: Interclass testing of object oriented software. In: Proc. of the IEEE International Conference on Engineering of Complex Computer Systems (2002)Google Scholar
  35. 35.
    Mitchell, J.C.: Foundations of Programming Languages. MIT Press, Cambridge (1996)Google Scholar
  36. 36.
    Nimmer, J.W., Ernst, M.D.: Automatic generation of program specifications. In: Proceedings of the 2002 International Symposium on Software Testing and Analysis (ISSTA), Rome (July 2002)Google Scholar
  37. 37.
    O’Callahan, R., Jackson, D.: Lackwit: A program understanding tool based on type inference. In: International Conference on Software Engineering, pp. 338–348 (1997)Google Scholar
  38. 38.
    Rugaber, S., Shikano, T., Kurt Stirewalt, R.E.: Adequate reverse engineering. In: Proceedings of the 16th Annual International Conference on Automated Software Engineering, pp. 232–241 (2001)Google Scholar
  39. 39.
    Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Transactions on Programming Languages and Systems 24(3), 217–298 (2002)CrossRefGoogle Scholar
  40. 40.
    Sankar, S.: Run-time consistency checking of algebraic specifications. In: Proceedings of the Symposium on Testing, Analysis, and Verification, Victoria, British Columbia, Canada (September 1991)Google Scholar
  41. 41.
    Sannella, D., Tarlecki, A.: Essential concepts of algebraic specification and program development. Formal Aspects of Computing 9, 229–269 (1997)zbMATHCrossRefGoogle Scholar
  42. 42.
    Shapiro, E.Y.: Algorithmic Program Debugging. In: ACM Distinguished Dissertation 1982. MIT Press, Cambridge (1982)Google Scholar
  43. 43.
    Summers, P.D.: A methodology for lisp program construction from examples. Journal of the ACM (JACM) 24(1), 161–175 (1977)zbMATHCrossRefMathSciNetGoogle Scholar
  44. 44.
    Whaley, J., Martin, M.C., Lam, M.S.: Automatic extraction of object-oriented component interfaces. In: Proceedings of the International Symposium of Software Testing and Analysis (2002)Google Scholar
  45. 45.
    Woodward, M.R.: Errors in algebraic specifications and an experimental mutation testing tool. IEEE Software Engineering Journal 8(4), 237–245 (1993)Google Scholar
  46. 46.
    Zhu, H., Hall, P.A.V., May, J.H.R.: Software unit test coverage and adequacy. ACM Computing Surveys (CSUR) 29(4), 366–427 (1997)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • Johannes Henkel
    • 1
  • Amer Diwan
    • 1
  1. 1.University of Colorado at BoulderBoulderUSA

Personalised recommendations