Skip to main content
SpringerLink
Log in

The application of formal specifications to software documentation and debugging

  • Software Maintenance and Debugging of Logic Programs III
  • Conference paper
  • First Online:
Automated and Algorithmic Debugging (AADEBUG 1993)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 749))

Included in the following conference series:

  • 133 Accesses

Abstract

This paper illustrates the application of formal specifications to software documentation and debugging by presenting a real-life scenario involving the use of a garbage collection package. It illustrates the advantages of using formal specifications over informal documentation. The paper also illustrates the usefulness of run-time checking tools that compares program behavior with their formal specifications.

The scenario presented in this paper goes through a series of steps that include formal specification, run-time checking, and modification of the specification and program based on the results of run-time checking — the typical steps involved in a debugging process, except that this scenario makes use of formal specifications.

Although various research ideas presented in this paper have been published earlier, this paper assimilates all these ideas into a real-life scenario, and illustrates in an easy-to-understand way that these ideas are really useful to software documentation and debugging.

The example has been developed in Ada, and formally specified using the Anna specification language. The tool used in the example is the Anna Run-Time Consistency Checking System developed at Stanford University.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. R. W. Floyd. Assigning meanings to programs. In Proceedings of a Symposium in Applied Mathematics of the American Mathematical Society, volume 19, pages 19–32. American Mathematical Society, 1967.

    Google Scholar 

  2. J. B. Goodenough and S. L. Gerhart. Towards a theory of test data selection. In Proceedings of the International Conference on Reliable Software, pages 493–510, April 1975.

    Google Scholar 

  3. C. Green, D. Luckham, R. Balzer, T. Cheatham, and C. Rich. Report on a knowledge based software assistant. Technical report, Kestrel Institute, 1983.

    Google Scholar 

  4. J. V. Guttag, J. J. Horning, and J. M. Wing. The Larch family of specification languages. IEEE Software, 2(5):24–36, September 1985.

    Google Scholar 

  5. D. P. Helmbold and D. C. Luckham. Runtime detection and description of deadness errors in Ada tasking. Technical Report 83-249, Computer Systems Laboratory, Stanford University, November 1983. (Program Analysis and Verification Group Report 22).

    Google Scholar 

  6. W. E. Howden. Algebraic program testing. Acta Informatica, 10:53–66, 1978.

    Google Scholar 

  7. B. Krieg-Brückner. Transformation of interface specifications, 1985. PROSPECTRA Study Note M.1.1.S1-SN-2.0.

    Google Scholar 

  8. R. L. London. A view of program verification. In Proceedings of the International Conference on Reliable Software, pages 534–545, April 1975.

    Google Scholar 

  9. D. C. Luckham, S. Sankar, and S. Takahashi. Two dimensional pinpointing: An application of formal specification to debugging packages. IEEE Software, 8(1):74–84, January 1991. (Also Stanford University Technical Report No. CSL-TR-89-379.).

    Google Scholar 

  10. D. C. Luckham and F. W. von Henke. An overview of Anna, a specification language for Ada. IEEE Software, 2(2):9–23, March 1985.

    Google Scholar 

  11. David C. Luckham. Programming with Specifications: An Introduction to ANNA, A Language for Specifying Ada Programs. Texts and Monographs in Computer Science. Springer-Verlag, October, 1990.

    Google Scholar 

  12. David C. Luckham, Friedrich W. von Henke, Bernd Krieg-Brückner, and Olaf Owe. ANNA, A Language for Annotating Ada Programs, volume 260 of Lecture Notes in Computer Science. Springer-Verlag, 1987.

    Google Scholar 

  13. N. Madhav and W. R. Mann. A methodology for formal specification and implementation of Ada packages using Anna. In Proceedings of the Computer Software and Applications Conference, 1990, pages 491–496. IEEE Computer Society Press, 1990. (Also Stanford University Computer Systems Laboratory Technical Report No. 90-438).

    Google Scholar 

  14. N. Madhav and S. Sankar. Application of formal specification to software maintenance. In Proceedings of the Conference on Software Maintenance, pages 230–241. IEEE Computer Society Press, November 1990.

    Google Scholar 

  15. Walter Mann. The Anna package specification analyzer user's guide. Technical Note CSL-TN-93-390, Computer Systems Lab, Stanford University, January 1993.

    Google Scholar 

  16. B. Meyer. Object-Oriented Software Construction. Prentice-Hall, 1988.

    Google Scholar 

  17. S. Sankar. Automatic Runtime Consistency Checking and Debugging of Formally Specified Programs. PhD thesis, Stanford University, August 1989. Also Stanford University Department of Computer Science Technical Report No. STAN-CS-89-1282, and Computer Systems Laboratory Technical Report No. CSL-TR-89-391.

    Google Scholar 

  18. S. Sankar. A note on the detection of an Ada compiler bug while debugging an Anna program. ACM SIGPLAN Notices, 24(6):23–31, 1989.

    Google Scholar 

  19. S. Sankar and D. S. Rosenblum. The complete transformation methodology for sequential runtime checking of an Anna subset. Technical Report 86-301, Computer Systems Laboratory, Stanford University, June 1986. (Program Analysis and Verification Group Report 30).

    Google Scholar 

  20. Sriram Sankar. Run-time consistency checking of algebraic specifications. In Proceedings of the Symposium on Testing, Analysis, and Verification (TAV4), pages 123–129, Victoria, Canada, October 1991. ACM Press.

    Google Scholar 

  21. Sriram Sankar, Anoop Goyal, and Prakash Sikchi. Software testing using algebraic specification based test oracles. Forthcoming Stanford University Technical Report, April 1993.

    Google Scholar 

  22. J. M. Spivey. Understanding Z, A Specification Language and its Formal Semantics. Cambridge Unversity Press, 1988. Tracts in Theorectical Computer Science, Volume 3.

    Google Scholar 

  23. L. G. Stucki and G. L. Foshee. New assertion concepts for self-metric software validation. In Proceedings of the International Conference on Reliable Software, pages 59–65, April 1975.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Stanford University, 94305, Stanford, California

    Anoop Goyal

  2. Sun Microsystems Laboratories, Inc., 2550 Garcia Avenue, 94043, Mountain View, California

    Sriram Sankar

Authors
  1. Anoop Goyal
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Sriram Sankar
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Peter A. Fritzson

Rights and permissions

Reprints and permissions

Copyright information

© 1993 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Goyal, A., Sankar, S. (1993). The application of formal specifications to software documentation and debugging. In: Fritzson, P.A. (eds) Automated and Algorithmic Debugging. AADEBUG 1993. Lecture Notes in Computer Science, vol 749. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0019418

Download citation

  • DOI: https://doi.org/10.1007/BFb0019418

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-57417-0

  • Online ISBN: 978-3-540-48141-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation