Transformational design summarizes a methodology where the description of a system is stepwise derived from the specification of its functional behaviour using semantics preserving rules. We exemplify the transformational design on the functional level with two major case studies, viz. the derivation of algorithms for manipulating polynomials and the derivation of digital circuits for counters. This exhibits important design strategies for sequential and parallel software and hardware systems.
This study is part of the research programme at Augsburg in which we attempt to come up with a more manageable formalism for deductive design in general. Many of the currently used derivation suffer from the use of lengthy expressions involving formulae from predicate calculus. However, in particular in the case of graph algorithms the calculus of formal languages and relations allows considerable compactification. We illustrate this with derivations of algorithms for computing the length of a shortest path between two graph vertices and for cycle detection.