| Summary: | In recent years a new framework for specification has been defined around ASL [SW 83, Wir 86, ST 88a, ST 88b]. Stress has been put on defining a specification language consisting of a few powerful specification building operations (SBO's for short) with simple semantics and an elegant implementation notion. Some important features of this work are the generalization to an arbitrary institution [GB 84] of a lot of previous work done on algebraic specification and the study of behavioural abstraction in the context of a model-oriented specification language. The basic research on formal specifications is generally regarded as the basis for a new generation of specification languages. These specification languages will instantiate ASL with their institution of interest, and will define their own specification constructs and implementation notion in terms of ASL's primitive SBO's and implementation notion. However, any useful formal framework for program development needs an inference system for the implementation relation, <i>i.e.</i> proofs that one specification implements another must be produced by a fixed family of rules without model-theoretical considerations. This poses a new and difficult problem to ASL due to its model-oriented nature and the great generality of both the implementation relation and the SBO's. In this thesis we study this problem starting from a simple specification language with only three SBO's, and progressively adding other common SBO's. In the course of this analysis we encounter four main problems for the verification of implementations: hiding of auxiliary functions, behavioural abstraction, reachability constraints and parameterization. These problems can be considered classical of algebraic specifications and the study of their verification aspects at an institution-independent level provides valuable results for many other specification languages. New results for the verification of implementations w.r.t. specifications with hidden parts and abstracted specifications at an institution-independent level are the main contribution of the thesis. Verification of reachability constraints is shown to be below the institutional level. In this case, a common institution for constraints is formally presented showing some ignored verification aspects. Finally, an original presentation of parameterization and structured implementations concludes the thesis. In conclusion, this thesis presents a collection of sublanguages, inference systems and side conditions which add a new dimension to the fascinating job started by ASL in [SW 83].
|
|---|
