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.
Preview
Unable to display preview. Download preview PDF.
References
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.
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.
C. Green, D. Luckham, R. Balzer, T. Cheatham, and C. Rich. Report on a knowledge based software assistant. Technical report, Kestrel Institute, 1983.
J. V. Guttag, J. J. Horning, and J. M. Wing. The Larch family of specification languages. IEEE Software, 2(5):24–36, September 1985.
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).
W. E. Howden. Algebraic program testing. Acta Informatica, 10:53–66, 1978.
B. Krieg-Brückner. Transformation of interface specifications, 1985. PROSPECTRA Study Note M.1.1.S1-SN-2.0.
R. L. London. A view of program verification. In Proceedings of the International Conference on Reliable Software, pages 534–545, April 1975.
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.).
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.
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.
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.
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).
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.
Walter Mann. The Anna package specification analyzer user's guide. Technical Note CSL-TN-93-390, Computer Systems Lab, Stanford University, January 1993.
B. Meyer. Object-Oriented Software Construction. Prentice-Hall, 1988.
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.
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.
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).
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.
Sriram Sankar, Anoop Goyal, and Prakash Sikchi. Software testing using algebraic specification based test oracles. Forthcoming Stanford University Technical Report, April 1993.
J. M. Spivey. Understanding Z, A Specification Language and its Formal Semantics. Cambridge Unversity Press, 1988. Tracts in Theorectical Computer Science, Volume 3.
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.
Author information
Authors and Affiliations
Editor information
Rights 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