THE FORMAL SPECIFICATION OF ABSTRACT-DATA-TYPES AND THEIR IMPLEMENTATION IN FORTRAN-90

In this paper we present an approach to the development of computation al science software based on the identification and specification of A bstract Data Types and their implementation in Fortran 90. Our aim is to improve upon current standards of documentation and levels of gener icity of such software, and, by the use of a formal specification nota tion, afford the possibility of undertaking correctness proofs. We ill ustrate the approach by applying it to a problem which is concerned wi th the construction of sets of electron configurations and their angul ar momentum couplings; software to solve this problem is required to e nhance the Graphical R-matrix Atomic Collision Environment (GRACE) gra phical user interface. In particular, we show how a formal notation ca n be used to specify unambiguously the functionality of software compo nents and we describe the role of the formal specification from the pe rspective of the ADT implementor and the ADT user. Finally we show how Fortran 90, through its derived types and module facility, directly s upports the encapsulation of ADTs thereby enabling the construction of better engineered software than has hitherto been possible using Fort ran.