A Formally Grounded Software Specification Method

One of the goals of software engineering is to provide what is necessary to write relevant, legible, useful descriptions of the systems to be developed, which will be the basis of successful developments. This goal was addressed both from informal approaches (providing in particular visual notations) and formal ones (providing a formal sound semantic basis). Informal approaches are often driven by a software development method, and, while formal approaches sometimes provide a user method, it is usually aimed at helping to use the proposed formalism when writing a speci\ufb01cation. Our goal here is to provide a companion method that helps the user to understand the system to be developed, and to write the corresponding formal speci\ufb01cations. We also aim at supporting visual presentations of formal speci\ufb01cations, so as to \u201cmake the best of both formal and informal worlds\u201d. We developed this method for the (logical-algebraic) speci\ufb01cation languages Casl (Common Algebraic Speci\ufb01cation Language, developed within the joint initiative CoFI) and for an extension for dynamic systems Casl-Ltl, and we believe it is general enough to be adapted to other paradigms. Another challenge is that a method that is too general does not encompass the different kinds of systems to be studied, while too many different specialized methods result in partial views that may be difficult to integrate in a single global one. We deal with this issue by providing a limited number of instances of our method, \ufb01tted for three different kinds of software items, while keeping a common \u201cmeta\u201d- structure and way of thinking. More precisely, we consider here that a software item may be a simple dynamic system, a structured dynamic system, or a data structure, and we show here how to support property-oriented (axiomatic) speci\ufb01cations. We are thus providing support for the \u201cbuilding-bricks\u201d tasks of specifying software artifacts that in our experience are needed for the development process. Our approach is illustrated with a lift case study