Formalizing informal requirements some aspects

  • N. W. P. van Diepen
  • H. A. Partsch
Part I Invited Contributions
Part of the Lecture Notes in Computer Science book series (LNCS, volume 490)


Formal specifications are nowadays considered as an important intermediate stage in the software development process. There are various approaches for constructing an efficient program satisfying a given formal specification. The formalization process, however, has not yet been investigated as thoroughly. Thus, it is still one of the main sources for inconsistencies between the wishes of the customer and the program finally delivered. Some problems to be solved during formalization are identified and illustrated with a real-world example.


Requirement Engineering Functional Requirement Specification Language Efficient Program Requirement Definition 
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. [Abrial et al. 79]
    Abrial, J.-R., Schuman S.A., Meyer, B.: Specification language. In: McKeag, R.M., MacNaughten, A.M. (eds.): On the construction of programs, Oxford University Press, 1979.Google Scholar
  2. [Agresti 86]
    Agresti, W.M. (ed.): New paradigms for software development. Washington, D.C.: IEEE Computer Society Press, 1986.Google Scholar
  3. [Backhouse 86]
    Backhouse, R.C.: Program construction and verification. London: Prentice-Hall, 1986.Google Scholar
  4. [Balzer 81]
    Balzer, R.: Final report on GIST. Technical Report USC/ISI, Marina del Rey, 1981.Google Scholar
  5. [Balzer et al. 83]
    Balzer, R., Cheatham, T.E. Jr., Green, C.: Software technology in the 1990's: using a new paradigm. In: Computer, November 1983, pp. 39–45.Google Scholar
  6. [Balzer Goldman 79]
    Balzer, R., Goldman, N.: Principles of good software specification and their implications for specification languages. In: Proc. Specifications of Reliable Software, Cambridge, Mass., 1979.Google Scholar
  7. [Bauer 81]
    Bauer, F.L.: Programming as fulfillment of a contract. In: Henderson, P. (ed.): System design. Infotech State of the Art Report 9:6, pp. 165–174. Maidenhead: Pergamon Infotech Ltd., 1981.Google Scholar
  8. [Bauer et al. 89]
    Bauer, F.L., Möller, B., Partsch, H., Pepper, P.: Programming by formal reasoning — computer-aided intuition-guided programming. In: IEEE Transactions on Software Engineering, 15:2, 1989.Google Scholar
  9. [Bergstra et al. 89]
    Bergstra, J.A., Heering, J., Klint P. (eds.): Algebraic specification. ACM Press Frontier Series. New York: Addison Wesley, 1989.Google Scholar
  10. [Bird Wadler 88]
    Bird, R.S., Wadler, P.L.: Introduction to functional programming. Hemel Hempstead: Prentice Hall, 1988.Google Scholar
  11. [Broy 87]
    Broy, M.: Predicative specifications for functional programs describing communicating networks. In: Information Processing Letters 25, pp. 93–101, 1987.CrossRefGoogle Scholar
  12. [Burstall Goguen 80]
    Burstall, R.M., Goguen, J.A.: Semantics of CLEAR, a specification language. In: Bjørner, D. (ed.): Abstract software specifications, pp. 292–332, Lecture Notes in Computer Science 86, Berlin: Springer, 1980.Google Scholar
  13. [Dijkstra 76]
    Dijkstra, E.W.: A discipline of programming. Englewood Cliffs, N.J.: Prentice-Hall, 1976.Google Scholar
  14. [Dubois et al. 88]
    Dubois, E., Hagelstein, J., Rifaut, A.: Formal requirements engineering with EREA. Philips Journal of Research 43:3/4, pp. 393–414, 1988.Google Scholar
  15. [Ehler 85]
    Ehler, H.: Making formal specifications readable. Institut für Informatik, TU München, Report TUM-I8527, 1985.Google Scholar
  16. [Ehrig et al. 83]
    Ehrig, H., Fey, W., Hansen, H.: ACT ONE — an algebraic specification language with two levels of semantics. TU Berlin, Technical Report 83–03, 1983.Google Scholar
  17. [Fairley 85]
    Fairley, R.: Software engineering concepts. New York: McGraw-Hill, 1985.Google Scholar
  18. [Feather 86]
    Feather, M.S.: A survey and classification of some program transformation approaches and techniques. In: Meertens, L.G.L.T. (ed.): Program specification and transformation. Proc. IFIP TC 2 Working Conference, Bad Tölz, April 15–17, 1986. Amsterdam: North-Holland, 1987.Google Scholar
  19. [Feijs et al. 87]
    Feijs, L.M.G., Jonkers, H.B.M, Obbink, J.H., Koymans, C.P.J., Renardel de Lavalette, G.R., Rodenburg, P.H.: A survey of the design language COLD. In: ESPRIT '86: Results and Achievements, pp. 631–644. Amsterdam: North-Holland, 1987.Google Scholar
  20. [Fey 86]
    Fey, W.: Introduction to Algebraic Specification in ACT TWO. T.U. Berlin, Technical Report 86-13, 1986.Google Scholar
  21. [Futatsugi et al. 85]
    Futatsugi, K., Goguen J.A., Jouannaud, J.P., Meseguer, J.: Principles of OBJ2. In: Proc. 12th Ann. ACM Symp. on Principles of Programming Languages, pp. 52–66. ACM, 1985.Google Scholar
  22. [Gaudel 85]
    Gaudel, M.C.: Toward structured algebraic specification. In: ESPRIT '85: Status Report of Continuing Work. Part I, pp. 493–510. Amsterdam: North-Holland, 1986.Google Scholar
  23. [Gijssen Haggenburg 88]
    Gijssen, G., Haggenburg, W.G.: Zwitsers Systeem. Amsterdam: KNSB, 1988 (partially in Dutch).Google Scholar
  24. [Goguen Tardo 77]
    Goguen, J.A., Tardo, J.: OBJ-0 preliminary users manual. University of California at Los Angeles, Computer Science Department, 1977.Google Scholar
  25. [Goguen Meseguer 81]
    Goguen, J., Meseguer, J.: OBJ-1, a study in executable algebraic formal specifications. SRI International Technical Report, 1981.Google Scholar
  26. [Gries 81]
    Gries, D.: The science of programming. Berlin: Springer, 1981.Google Scholar
  27. [Guttag Horning 83]
    Guttag, J.V., Horning, J.J.: Preliminary Report on the LARCH shared language. Technical Report CSL 83-6, Xerox, Palo Alto, 1983.Google Scholar
  28. [Hehner et al. 86]
    Hehner, E.C.R., Gupta, L.E., Malton, A.J.: Predicative Methodology. In: Acta Informatica 23, pp. 487–505, 1986.CrossRefGoogle Scholar
  29. [Henderson 80]
    Henderson, P.: Functional programming: application and implementation. Englewood Cliffs, N.J.: Prentice-Hall, 1980.Google Scholar
  30. [Henderson 81]
    Henderson, P.: System design: analysis. Infotech State of the Art Report 9:6, System design, pp. 5–163. Maidenhead: Pergamon Infotech Ltd., 1981.Google Scholar
  31. [Herik 88]
    Van den Herik, J.: Computerschaak. In: Schakend Nederland 95:9, pp. 38–39, 1988 (in Dutch).Google Scholar
  32. [Hußmann 87]
    Hußmann, H.: RAP-2 User Manual. Universität Passau, Fachbereich Mathematik und Informatik, Technical Report, 1987.Google Scholar
  33. [IEEE 77]
    Special Collection on Requirement Analysis. IEEE Transactions on Software Engineering SE-3:1, pp. 2–84, 1977.Google Scholar
  34. [IEEE 83]
    IEEE Standard Glossary of software engineering terminology. IEEE Standard 729, 1983.Google Scholar
  35. [Jones 80]
    Jones, C.B.: Software development: a rigorous approach. Englewood Cliffs, N.J.: Prentice-Hall, 1980.Google Scholar
  36. [Jonkers et al. 86]
    Jonkers, H.B.M., Koymans C.P.J., Renardel de Lavalette, G.R.: A semantic framework for the COLD-family of languages. Logic Group Preprint Series No. 9, Department of Philosophy, University of Utrecht, 1986.Google Scholar
  37. [Kažić 80]
    Kažić, B.M.: The Chess Competitor's Handbook. London: Badsford, 1980.Google Scholar
  38. [Kühnel et al. 87]
    Kühnel, B., Partsch, H., Reinshagen, K.P.: Requirements Engineering — Versuch einer Begriffsklärung. In: Informatik-Spektrum 10:6, pp. 334–335, 1987 (in German).Google Scholar
  39. [Lehman 80]
    Lehman, M.M.: Programs, life cycles, and laws of software evolution. In: Proc. IEEE 68:9, 1980.Google Scholar
  40. [London Feather 82]
    London, P., Feather, M.S.: Implementing specification freedom. In: Science of Computer Programming 2, pp. 91–131, 1982.Google Scholar
  41. [Möller 87]
    Möller, B.: Higher-order algebraic specifications. Habilitation thesis, Fakultät für Mathematik und Informatik, T.U. München, 1987.Google Scholar
  42. [Möller et al. 88]
    Möller, B., Tarlecki, A., Wirsing, M.: Algebraic specification with built-in domain constructions. In: Dauchet, M., Nivat, M. (eds.): CAAP '88. Lecture Notes in Computer Science 299, pp. 132–148, Berlin: Springer, 1988.Google Scholar
  43. [Partsch 86]
    Partsch, H.: Algebraic requirements definition: a case study. Technology and Science of Informatics 5:1, pp. 21–36, 1986.Google Scholar
  44. [Partsch 87]
    Partsch, H.: Requirements Engineering und Formalisierung — Problematik, Ansatz und erste Erfahrungen. In: Schmitz, P., Timm, M., Windfuhr, M. (eds.): Requirements Engineering '87, pp. 9–31. GMD-Studien 121, 1987 (in German).Google Scholar
  45. [Partsch 89]
    Partsch, H.: Algebraic specification — A step towards future software engineering. In: Proc. METEOR-Workshop, Passau, May 1987, Lecture Notes in Computer Science 394, Berlin: Springer, 1989.Google Scholar
  46. [Partsch Laut 82]
    Partsch, H., Laut, A.: From requirements to their formalization — a case study on the stepwise development of algebraic specifications. In.: H. Wössner (ed.): Programmiersprachen und Programmentwicklung, 7. Fachtagung, München 1982, pp. 117–132. Informatik-Fachberichte 53, Berlin: Springer, 1982.Google Scholar
  47. [Partsch Steinbrüggen 83]
    Partsch, H., Steinbrüggen, R.: Program transformation systems. In: ACM Computing Surveys 15, pp. 199–236, 1983.CrossRefGoogle Scholar
  48. [Polya et al. 83]
    Polya, G., Tarjan, R.E., Woods, D.R., Notes on Introductory Combinatorics. Basel, 1983.Google Scholar
  49. [Roman 85]
    Roman, G.-C.: A taxonomy of current issues in requirements engineering. In: IEEE Computer 18:4, pp. 14–23, 1985.Google Scholar
  50. [Rzepka Ohno 85]
    Rzepka, W.E., Ohno, Y.: Requirements engineering environments: software tools for modeling user needs. In: IEEE Computer, 18:4, pp. 9–12, 1985.Google Scholar
  51. [Smith Lowry 89]
    Smith, D.R., Lowry, M.J.: Algorithm theories and design tactics. In: Van de Snepscheut, J.L.A. (ed.): Proc. Mathematics of Program Construction, pp. 379–398, Lecture Notes in Computer Science 375, Berlin: Springer, 1989.Google Scholar
  52. [Swartout 82]
    Swartout, W.: GIST English generator. In: Proc. AAAI 82, August 1982.Google Scholar
  53. [Webster 74]
    Webster's New World Dictionary. Second College Edition. Cleveland: William Collings & World Publishing, 1974.Google Scholar
  54. [Wirsing 83]
    Wirsing, M.: A Specification Language. Habilitation thesis, Fachbereich Mathematik und Informatik, T. U. München, 1983.Google Scholar
  55. [Yeh 82]
    Yeh, R.T.: Requirements analysis — a management perspective. In: Proc. COMPSAC '82, pp. 410–416, November 1982.Google Scholar
  56. [Yeh Zave 80]
    Yeh, R.T., Zave, P.: Specifying software requirements. In: Proc. IEEE 68:9, pp. 1077–1085, 1980.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1991

Authors and Affiliations

  • N. W. P. van Diepen
    • 1
  • H. A. Partsch
    • 1
  1. 1.Department of Computer ScienceUniversity of NijmegenNijmegenThe Netherlands

Personalised recommendations