Formal Specifications Guide Development and Testing of Software Components

R. E. Davis

《淡江理工學刊》 2卷1期 (1999/06) Pp. 1-10

https://doi.org/10.6180/jase.1999.2.1.01

並列摘要

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.

並列關鍵字

formal methods ； formal specification ； Larch ； LSL ； testing ； software components ； abstract data types ； Ada