Abstract Combining a set of existing constraint solvers into an integrated system of cooperating solvers is a useful and economic principle to solve hybrid constraint problems. In this paper we show that this approach can also be used to integrate different language paradigms into a unified framework. Furthermore, we study the syntactic, semantic and operational impacts of this idea for the amalgamation of declarative and constraint programming.

Unlike for conventional compilers for imperative programming languages such as C or ADA, no established methods for safeguarding artifacts generated by model-based code generators exist despite progress in the field of formal verification. Several test approaches dominate the engineering practice. This paper describes a general and tool-independent test architecture for code generators used in model-based development. We evaluate the effectiveness of our test approach by means of testing optimizations performed by the TargetLink code generator, a widely accepted and complex development tool used in automotive model-based development.

Formal program construction by transformations is a method of software development in which a program is derived from a formal problem specification by manageable, controlled transformation steps which guarantee that the final product meets the initial specification. This methodology has been investigated in the Munich project CIP (computer-aided intuition-guided programming). The research includes the design of a wide-spectrum language specifically tailored to the needs of transformational programming, the construction of a transformation system to support the methodology, and the study of transformation rules and other methodological issues. Particular emphasis has been laid on developing a sound theoretical basis for the overall approach.>

The algebraic specification of the semantics of programming languages is outlined. Particular emphasis is given to the problem of specifying least-fixed points by first-order conditional equations. To cover this issue, the theory of specifying partial heterogeneous algebras by abstract data types is slightly extended by a more general notion of homomorphism. In this framework the semantics of programming languages can be uniquely specified in a purely algebraic way, using particular models of a hierarchy of abstract types. This approach is demonstrated for a simple procedural programming language. Several increasingly complex versions of iterations are treated and analyzed with respect to their theoretical consequences. Finally, as a complementary algebraic technique, transformational semantics is explained and applied to our examples.

The basic idea of the Schorr-Waite graph-marking algorithm can be precisely formulated, explained, and verified in a completely applicative (functional) programming style.Graphs are specified algebraically as objects of an abstract data type.When formulating recursive programs over such types, one can combine algebraic and algorithmic reasoning: An applicative depth-first-search algorithm is derived from a mathematical specification by applying properties of reflexive, transitive closures of relations.This program is then transformed in several steps into a fmal procedural version with the help of both algebraic properties of graphs and algorithmic properties reflected in the recursion structure of the program.

A methodology of program development by transformations is outlined. In particular, ways of representing the transformation rules are discussed, and the relationship between notions of their correctness and the semantic definition of programming languages is studied. How transformation techniques are complemented by the use of abstract data types and assertions is described. In the resulting calculus of transformations, the single rules not only represent design or optimization techniques, but they also incorporate verification principles. To illustrate this approach, the Warshall algorithm is developed by successive applications of transformations.