The same information in German
The use of compiler-generating methods and tools for the implementation of higher semantical models is studied. Especially the advantages of algebraic specification, e.g. correctness aspects, and attribute grammars, e.g. intuitivity and efficiency, should be combined.
A new specification technique, called attributed algebraic specification, is investigated closing the gap between the specification formalisms of algebraic specifications and attribute grammars to unify the advantages of algebraic specifications (precise model class semantics, theorem proving techniques, deductive aspects, abstraction, implementation relations) and those of attribute grammars (intuitivity, efficiency, description of context dependent information, distinction of syntax and semantics specification).
The contribution of this research is to extend algebraic specifications in such a way that the ideas of both specification techniques are combined, i.e. especially to describe context dependent informations and to prove their correctness.
Undirected attribute equations, instead of directed attribute equations as in ' usual attribute grammar systems, are applied in the new specification technique allowing an abstract specification of the attribute dependencies. These equations are solvable in the considered logical framework. But they require the investigation of new dependency notions and new attribute evaluation strategies.
Specification building operations for the new formalism are defined and it is shown how they can be normalized. Especially these operations take the notion of behaviour for attributed trees as an abstraction mechanism into consideration.
A standard and behavioural implementation relation are developed with proof theoretical characterizations and properties, like transitivity or monotonicity relative to the specification building operations.
Calculi for solving existential and universal quantified formulae are presented. For the universal quantified formulae an induction principle and a notion of complete set is defined usable especially for showing the correctness of implementation relations.
Case studies show the applicability of the new approach in the area of specifying the dynamics of user interfaces, compilers and document architecture systems.
The presented formalism can be used in a formal software engineering process. A software engineering process in this framework would start with a loose attributed algebraic specification until after several implementation steps a usual attribute grammar is reached from which an executable programme can be generated.
All considered aspects can be applied in this process as the following considerations show: Undirected attribute equations allow a loose and abstract specification. To execute such specifications (catchword: rapid prototyping), calculi are necessary for solving existential quantified formulae. To speed up execution time attribute evaluation algorithms have to be derived for the undirected attribute equations. Specification building operations allow modularization in the software development process resulting in readable specifications. First of all, testing on a high level of abstraction is necessary (usage of calculi for proving existential and universal quantified formulae) to obtain correct software after several implementation steps. Secondly, the correctness of the implementation steps must be shown (proof theoretical handling of the implementation relations). In the considered case studies these aspects are shown exemplarily.
Bernhard Bauer 2.3.1994