Literate program derivation: A case study

  • Peter Pepper
Part II. Deductive Program Development
Part of the Lecture Notes in Computer Science book series (LNCS, volume 544)


“Literate programming” is a notion that has been introduced by Don Knuth as a means for improving the art of programming by amalgamating explanatory text with the program proper. In this paper, we attempt to combine the principal ideas of literate programming with the concepts of formal program development, based on algebraic specifications and transformations. This experiment is performed using the sublinear string-searching algorithm of Boyer and Moore (1977) as an illustrating example.


Transformation System Borderline Case Recursive Equation Main Lemma Program Text 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. Bauer, F.L., Wössner, H.: Algorithmic Language and Program Development. Berlin, Springer 1982.Google Scholar
  2. Bird, R.S.: An Introduction to the Theory of Lists. In: Broy, M. (ed.): Logic of Programming and Calculi of Discrete Design. Proc. Int. Summer School, Marktoberdorf. NATO ASI Series F, Vol. 36, Berlin, Springer 1985, 5–42.Google Scholar
  3. Boyer, R.S., Moore, J.S.: A Fast String Searching Algorithm. Comm. ACM 20 (1977) 762–772.Google Scholar
  4. Broy, M., Pepper, P.: Program Development as a Formal Activity. IEEE Transactions on Software Engineering SE-7, 1 (1981), 14–22.Google Scholar
  5. Burstall, R.M., Darlington, J.: A Transformation System for Developing Recursive Programs. J.ACM 24 (1977), 44–67.Google Scholar
  6. CIP-group (Bauer, F.L. et al.): The Munich Project CIP. Vol. II: The Program Transformation System CIP-S. Lecture Notes in Comp. Sc. 292, Berlin, Springer 1987.Google Scholar
  7. Gries, D.: The Science of Programming. New York, Springer 1981.Google Scholar
  8. Gries, D.: On “A Small Work of Literature”. Comm. ACM 30, 4 (1987), 286–288.Google Scholar
  9. Hamilton, E.: Expanding Generalized Regular Expressions. Comm. ACM 31, 12 (1988), 1377–1382.Google Scholar
  10. Hanson, D.R.: Printing Common Words. Comm. ACM 30, 7 (1987), 594–598.Google Scholar
  11. Jackson, M.: Processing Transactions. Comm. ACM 30, 12 (1987), 1001–1008.Google Scholar
  12. Knuth, D.E.: Literate Programming. Comp. Journal 27, 2 (1984), 37–111. (See also Comm. ACM 29, 5 (1986), 364–369 and 29, 6 (1986) 471–483.)Google Scholar
  13. Partsch, H.A.: Transformational Program Development in a Particular Problem Domain. Science of Comp. Progr. 7 (1986), 99–241.Google Scholar
  14. Partsch, H.A., Stomp, F.A.: A Formal Derivation of Boyer and Moore's Pattern Matching Algorithm. Techn. Rep. 88–12, Dept. of Informatics, Univ. Nijmegen, 1988. (To appear in: Formal Aspects of Computing).Google Scholar
  15. Pepper, P.: A Simple Calculus For Program Transformation. Science of Computer Programming 9 (1987) 221–262.Google Scholar
  16. Roszak, Th.: Der Verlust des Denkens (Engl.: The Cult of Information) München, Droemer 1986.Google Scholar
  17. Smith, D.R.: KIDS — A Knowledge-Based Software Development System. In: Proc. of the Workshop on Automating Software Design, AAAI 1988.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1991

Authors and Affiliations

  • Peter Pepper
    • 1
  1. 1.Institut für Angewandte InformatikTechnische Universität BerlinBerlin 10

Personalised recommendations