Formal Specifications Guide Development and Testing of Software Components

10.6180/jase.1999.2.1.01

R. E. Davis

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

淡江理工學刊

2卷1期（1999 / 06 / 01）

1 - 10

英文

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.

1. 黃潔君(2016)。喪失重要客戶對會計師客戶組合與審計品質之影響。淡江大學會計學系碩士班學位論文。2016。1-57。 
2. 黃威翔(2018)。臺灣地區犬貓死亡原因與死亡方式研究。臺灣大學獸醫學研究所學位論文。2018。1-195。 
3. 曾郁祺(2016)。投資者情緒與中國股票報酬之研究。國立臺灣大學財務金融學系學位論文。2016。1-34。 
4. 郭政賢(2016)。大臺南地區國民小學自然科教師使用電子教科書之喜好因素探討--以康軒出版社為例。長榮大學經營管理研究所學位論文。2016。1-148。