A Powerful Transformation Rule, its Applications and Variants

  • Klaus Achatz
  • Helmuth Partsch
Part of the IFIP Advances in Information and Communication Technology book series (IFIPAICT)


This paper introduces, discusses and proves a transformation rule to convert specifications of set-valued functions defined by set comprehension into functional implementations. The power of the rule is illustrated by several examples, among them a Prolog interpreter. Also, variants of the rule for specifications involving existential quantification and arbitrary choice are presented and illustrated by representative examples.


Transformational programming backtracking set comprehension functional implemention 


  1. Achatz, K. and Partsch, H.A. (1996) From Descriptive Specifications to Operational ones: A powerful transformation rule, its applications and variants. Faculty for Informatics, University of Ulm, Nr. 96–13, Ulmer Informatik-Berichte, 1996.Google Scholar
  2. Bauer, F.L. and Berghammer, R. and Broy, M. and Dosch, W. and , F. and Gnatz, R. and Hangel, E., Hesse, W. and Krieg-Brückner, B. and Laut, A. and Matzner, T. and Möller, B. and Nickl, F. and Partsch, H. and Pepper, P. and Samelson, K. and Wirsing, M. and Wössner, H. (1985) The Munich project CIP. Volume I: The wide spectrum language CIP-L. Lecture Notes in Computer Science 183, Springer, Berlin.CrossRefGoogle Scholar
  3. Bauer, F.L. and Möller and B., Partsch and H., Pepper, P. (1989) Programming by formal reasoning–computer-aided intuition-guided programming. IEEE Transactions on Software Engineering 15: 2, 165–180.zbMATHCrossRefGoogle Scholar
  4. Boiten, E.A. and Partsch, H.A. and Tuijnman, D. and Völker, N. (1992) How to produce correct software — an introduction to formal specification and program development by transformations. The Computer Journal 35: 6, 547–554.CrossRefGoogle Scholar
  5. Broy, M. and Wirsing, M. (1980) Program development: from enumeration to backtracking. Information Processing letters 10:4, 5, 193–197.zbMATHCrossRefGoogle Scholar
  6. Gerhart, S.L. and Yelowitz, L. (1976) Control structure abstractions of the backtracking programming technique. Proc. 2nd Int. Conf. on Software Engineering, October 13–15, 1976, San Francisco, Ca., 44–49. Also: IEEE Transactions on Software Engineering 2: 4, 285–292.MathSciNetGoogle Scholar
  7. Partsch, H.A. (1990) Specification and transformation of programs — a formal approach to software development. Springer, BerlinzbMATHCrossRefGoogle Scholar
  8. Smith, D.R. (1987) On the design of generate-and-test algorithms: subspace generators. Technical Report KES.U.86.6. Kestrel Institute, Palo Alto, Ca., 1986. Also: Meertens, L.G.L.T. (ed.): Program specification and transformation. Amsterdam: North-Holland, 207–220.Google Scholar
  9. Smith, D.R. (1988) The structure and design of global search algorithms.Technical Report KES.U.87.12, Kestrel Institute, Palo Alto, Ca.Smith, D.R. (1990) KIDS: a semiautomatic program development system. IEEE Transactions on Software Engineering 16: 9, 1024–1043.Google Scholar

Copyright information

© IFIP 1997

Authors and Affiliations

  • Klaus Achatz
    • 1
  • Helmuth Partsch
    • 1
  1. 1.Department of Computer ScienceUniversity of UlmUlmGermany

Personalised recommendations