AN EXECUTABLE SPECIFICATION FORMALISM REPRESENTING ABSTRACT DATA TYPES

Abstract

It has been proved to be very useful and necessary to give formal specifications of software systems to be developed. The specifications should help to avoid the necessity of creating prototypes by offering direct executability. A useful specification language aiming the description of abstract data types - while maintaining abstractness - should also support the representation of states of objects, as well as support the transformation of declarative specifications into efficiently executable code. The present paper is intended to give an informal description of a specification language aimed to offer the features discussed above. Although the development of the language has mainly been motivated by the object-oriented language (OMOHUNDRO, 1993), it is intended to function as a specification formalism at a much broader field.