The Use of Ada as an Implementation Language in Formally Specified Systems

Formal specification languages such as SPECIAL and Ina Jo were designed to be used with a variety of implementation languages. Our attempts to uae them with Ada are reviewed here. In order to develop a rational compliance document which shows how Ada code implements the formal specification it was necessary to bypass most of the structuring features of the specification language and to use just the latter's first order logical features to axiomatize Ada typing, etc . Our experience underlines the need for a new Ada based formal specification language.