The Design and Use of Specification Languages.

The goal of proving the correctness of computer programs has been hindered by the difficulty of stating formally what is to be proven. The tools developed to achieve this latter purpose often receive the name of specification languages, but the formalization and implementation of such languages has seldom been carried out, and very few of these languages have been described in the literature. We present some design issues concerning specification languages, e.g., desirable properties of such languages, and their limitations, as well as some ideas on their use and hence on the use of specifications in general as an integral part of the design process leading to reliable software systems. The possibly automated verification of some properties of formal specifications is considered, and some conclusions are drawn concerning the help such an approach can bring in providing greater confidence in the final software product. Author