Abstract
The concepts of specification and formalization, as relevant to the development of programs, are introduced and discussed. It is found that certain arguments given for using particular formal modes of expression in developing and proving programs correct are invalid. As illustration a formalized description of Algol 60 is discussed and found deficient. Emphasis on formalization is shown to have harmful effects on program development, such as neglect of informal precision and simple formalizations. A style of specifications using formalizations only to enhance intuitive understandability is recommended.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
A. V. Aho, J. E. Hopcroft and J. D. Ullman,The design and analysis of computer algorithms. Addison-Wesley, Reading, Mass., 1974.
J. W. Backus,The syntax and semantics of the proposed international algebraic language of the Zürich ACM-GAMM conference, Proc. International Conf. on Information Processing, UNESCO, 1959, pp. 125–132.
J. W. Backus, F. L. Bauer, J. Green, C. Katz, J. McCarthy, P. Naur (ed.), A. J. Perlis, H. Rutishauser, K. Samelson, B. Vauquois, J. H. Wegstein, A. van Wijngaarden and M. Woodger,Revised report on the algorithmic language ALGOL 60, Comm. ACM 6, 1 (1963, January), 1–17; Computer Journal 5, 349–367; Num. Math. 2, 106–136.
R. M. de Morgan, I. D. Hill and B. A. Wichman,Modified report on the algorithmic language ALGOL 60, Computer Journal 19 (1976), 364–379.
C. F. Gauss,Theorematis arithmetici — demonstratio nova, Commentationes Societatis Regiæ Scientiarum Gottingensis, Vol. 16, Göttingen, 1808;Werke, 1876, Bd. 2, pp. 1–8;English translation in D. E. Smith, A Source Book in Mathematics, Vol. 1, Dover, New York, 1959, pp. 112–118.
J. Goguen,Thoughts on specification, design and verification, ACM SIGSOFT Software Engineering Notes, Vol. 5 no. 3 (1980, July), 29–33.
W. Henhapl and C. B. Jones,A formal definition of ALGOL 60 as described in the 1975 Modified Report, in D. Bjørner and C. B. Jones (eds.),The Vienna development method: the meta-language, Springer, Lecture Notes in Computer Science 61, Berlin - Heidelberg - New York, 1978, pp. 305–336.
C. B. Jones,The meta-language: a reference manual, in D. Bjørner and C. B. Jones (eds.),The Vienna development method: the meta-language, Springer, Lecture Notes in Computer Science 61, Berlin - Heidelberg - New York, 1978, pp. 218–277.
C. B. Jones,Software development: a rigorous approach, Prentice-Hall, Englewood Cliffs, New Jersey, 1980.
B. Liskov,Modular program construction using abstractions, in D. Bjørner (ed.),Abstract software specifications, Springer, Lecture Notes in Computer Science 86, Berlin - Heidelberg - New York, 1980, pp. 354–389.
B. Liskov and S. Zilles,An introduction to formal specifications of data abstractions, in R. T. Yeh (ed.),Current Trends in Programming Methodology, Vol. 1, Prentice-Hall, Englewood Cliffs, New Jersey, 1977, pp. 1–32.
P. Naur,Concise survey of computer methods, Studentlitteratuur, Lund, Sweden, 1974.
P. Naur,Control-record-driven processing, in R. T. Yeh (ed.), Current Trends in Programming Methodology, Vol. 1, Prentice-Hall, Englewood Cliffs, New Jersey, 1977, pp. 220–232.
B. Russell,Mysticism and logic, Penguin, Harmondsworth, England, 1953.
B. Russell,Introduction, in L. Wittgenstein, Tractatus logico-philosophicus, Routledge and Kegan Paul, London, 1922.
H. Zemanek,Abstract Architecture, in D. Bjørner (ed.), Abstract software specifications, Springer, Lecture Notes in Computer Science 86, Berlin- Heidelberg - New York, 1980, pp. 1–42.
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Naur, P. Formalization in program development. BIT 22, 437–453 (1982). https://doi.org/10.1007/BF01934408
Received:
Issue Date:
DOI: https://doi.org/10.1007/BF01934408