Formal Specifications Guide Development and Testing of Software Components

R.E. Davis

doi:10.6180/jase.1999.2.1.01

Formal Specifications Guide Development and Testing of Software Components

Computer Science and Information Engineering

R. E. Davis This email address is being protected from spambots. You need JavaScript enabled to view it.¹

¹Computer Engineering Department Santa Clara University Santa Clara, CA 95053, U.S.A.

Received: May 4, 1999
Accepted: June 21, 1999
Publication Date: June 21, 1999

Download Citation: ||https://doi.org/10.6180/jase.1999.2.1.01

ABSTRACT

Formal specifications provide many benefits to software developers. It has long been recognized that formal methods are required in safety critical applications, where it may even be necessary to perform formal proofs of correctness to increase confidence in the reliability of the system. However, not all uses of formal methods require the same level of detail, or even formality. We can design formal specifications of software components, and then use the specifications in an informal way to guide the development of an implementation as well as to provide a blueprint for testing of the finished component. In this paper we use the Larch Shared Language (LSL) to specify abstract data types, and show how the specification can be used both to guide implementation in Ada95 and to develop a testing plan. This approach increases both the quality of documentation and confidence in the correctness of reusable components providing abstract data structures.

Keywords: formal methods, formal specification, Larch, LSL, testing, software components, abstract data types, Ada.

REFERENCES

[1] Barnes, J. G. P., Programming in Ada, Addison-Wesley Publishing Company, Menlo Park, CA. (1994).
[2] Biggerstaff, T. and Richter, C., “Reusability Framework, Assessment, and Directions,” IEEE Software, Vol. 4, No. 2, pp.41-49 (1987).
[3] Booch, G., Software Components with Ada. Benjamin/Cummings, Menlo Park, CA. (1987).
[4] Davis, R. E. and Danielson, R. L., “LSL + Ada Æ Reusable Data Structures,” In Proceedings of the Tenth Annual Washington Ada Symposium, pp. 115-124 (1993).
[5] Garlan, D., “Formal Methods for Software Engineers: Tradeoffs in Curriculum Design,” In C. Sledge, editor, Software Engineering Education, volume 640 of Lecture Notes in Computer Science, pp. 131-142. Springer-Verlag (1992).
[6] Garland, S. J., Guttag, J. V. and Horning, J. J., “Debugging Larch Shared Language Specifications,” IEEE Transactions on Software Engineering, Vol. 16, No. 9, pp.1044-1057 (1990).
[7] Guttag, J. V., Horning, J. J. and Modet, A., “Report on the Larch Shared Language,” version 2.3. Technical Report DEC/SRC SRC-58, Digital Equipment Corporation Systems Research Center Report, April, (1990).
[8] Guttag, J. V. and Horning, J. J. and Wing, J. M., “The Larch Family of Specification Languages,” IEEE Software, Vol. 2, No. 5, pp. 24-36 (1985).
[9] Guttag, J. V. and Modet, A. and Horning, J. J. (eds.) with Garland, S. J. and Jones, K. D. and Wing, J. M., “Larch: Languages and Tools for Formal Specification,” Texts and Monographs in Computer Science. Springer-Verlag (1993).
[10] Jefferson, O. A. and Roland, H. U., “Software Reuse in an Educational Perspective,” In C. Sledge, editor, Software Engineering Education, volume 640 of Lecture Notes in Computer Science, pp. 88-98. Springer-Verlag (1992).
[11] Krueger, C. W., “Software Reuse,” ACM Computing Surveys, Vol. 24, No. 2, pp. 131-183 (1992).
[12] Sindre, G. and Karlsson, E. A. and Stålhane, T., “Software Reuse in an Educational Perspective,” In C. Sledge, editor, Software Engineering Education, volume 640 of Lecture Notes in Computer Science, pp. 99-114. Springer-Verlag (1992).
[13] Woodfield, S. N., Embley, D. W. and Scott D. T., “Can Programmers Reuse Software?,” IEEE Software, Vol. 4, No. 4, pp.52-59 (1987).