ББК 22.18 Г 85 УДК 681.3 Грис Д. Г 85 Наука программирования: 1984.— 416 с., ил. Пер. с англ.—М.: Мир, Монография известного американского ученого написана как введение в науку программирования и отражает богатый опыт автора в научной и преподавательской работе. По своему замыслу она примыкает к известной книге Э. Дейкстры «Дисцип- лина программирования» (М.: Мир, 1976). Автор знаком советским читателям по книге «Конструирование компиляторов для цифровых вычислительных машин» (М.: Мир, 1975). Для программистов и разработчиков математического обеспечения ЭВМ. 2405000000-183 160-84, ч. 1 ББК 22.18 517.8 041 (01)-84 Редакция литературы по математическим наукам Дэвид Грис НАУКА ПРОГРАММИРОВАНИЯ Научный редактор Бабынина Л. П. Мл. научн. редактор Полякова Н. С. Художественный редактор Шаповалов В. И. Художник Бычков С. А. Технический редактор Потапенкова Е. С. Корректор Смирнов М. А. ИБ № 3618 Сдано в набор 27.02.84. Подписано и печати 31.08.84. Формат 60Х90'/и. Бумага типографская № 2. Гарнитура литературная. Печать высокая Объем 13,00 бум. л. Усл. печ. л, 26,00. Усл. кр.-отт. 26,00. Уч.-изд. л. 23,50. Изд. № 1/2618. Тираж 20000 экз. Заказ № 1718. Цена 1 р. 90 к. ИЗДАТЕЛЬСТВО «МИР» 129820, Москва, И-110. ГСП, 1-й Рижский пер., 2 Отпечатано с матриц Ордена Октябрьской революции и ордена Трудо- вого Красного Знамени Первой Образцовой типографии имени А А. Жда- нова Союзполиграфпрома при Государственном комитете СССР по делам издательств, полиграфии и книжной торговли, 113054, Москва, Валовая, 28 в Ленинградской типографии № 4 ордена Трудового Красного Знамени Ленинградского объединения «Техническая книга» им. Евгении Соколо- вой Союзполнграфпрома при Государственном комитете СССР по делам издательств, полиграфии и книжной торговли. 191126, Ленинград, Со- циалистическая ул., 14. © by Springer-Vcrlag Berlin Heidelberg 1981 All rights reserved. Authorized translation from English language edition published by Springer-Verlag Berlin—Heidelberg—New York © Перевод на русский язык, «Мир», 1984 ПРЕДИСЛОВИЕ РЕДАКТОРА ПЕРЕВОДА Несмотря на помещенные ниже два предисловия, хотелось бы еще кое-что сказать об этой незаурядной книге. Дэвид Грис — один из лучших пропагандистов информатики. Во-первых, он прекрасно владеет ее техническим содержанием. Это владение основано как на его собственном существенном вкладе в теорию и методы трансляции, так и на широком и активном ин- тересе к развитию области, который поддерживается личными кон- тактами автора с ведущими специалистами. Во-вторых, он один из немногих специалистов, которые смотрят на информатику в ис- торической перспективе, улавливая тенденции развития и опираясь на исторические аналогии, обеспеченные хорошим знанием истории науки (и прежде всего истории математики — старшей сестры вы- числительной науки). Это ощущение общей линии развития при- дает учебникам Гриса столь необходимые для хорошего преподава- ния качества стабильности и авторитета. Благодаря этому ощущению Грис избегает излишних конъюнктурных увлечений, характерных для некоторых авторов, пишущих в угоду коммерции и технике. В-третьих, Грис обладает присущим каждому прирожденному пе- дагогу даром выделять в предмете главные черты, объяснять их просто в их видимой и понятной взаимосвязи, передавая тем самым учащемуся чувство уверенности и способности к прямому действию при решении задачи. Наконец, ему свойственна нетривиальная спо- собность к синтезу американской и европейской образовательной традиции, что, как мне кажется, особенно необходимо для хорошей литературы по информатике, если учесть огромные социальные по- следствия предстоящего тотального вторжения ЭВМ в нашу жизнь. Хотелось бы заметить, что, по моему мнению, эта способность Гриса была воспитана не только его длительными визитами в Европу, но и особой интеллектуальной обстановкой, созданной профессорами старшего поколения Корнеллского университета, в котором он работает, и до некоторой степени характерной для всех университе- тов Новой Англии. Результат такого синтеза и есть предлагаемая вниманию чита- телей книга Д. Гриса. В ее внешнем выражении она является адап- тацией известной книги Эдсгера Дейкстры «Дисциплина програм- мирования» (М.: Мир, 1978). Структура книги весьма проста. В первой ее части излагаются элементарные сведения из исчисления высказываний и предикатов. Во второй части на основе пред- и по- стусловий очень подробно описывается логическая семантика про- 1. Alien I E_ WFF'N PROOF: The Game of Modern Logic. Autotelic Instructional Material Publishers, New Haven, 1972. 2- ^T1'17'1'-' samelson K. (eels'). Language Hierarchies and Interfaces. Lecture Notes in Computer Science, v. 46, Springer, 1976. 3. Bauer F.L., Broy M. (eds). Software Engineering: an advanced course. Lecture Notes in Computer Science, v. 30, Springer, 1976 4. Bauer F. L. Broy M. (eds). Program Construction. Lecture Notes in Computer Science, v. 69, Springer, 1979. • 5. Burstall R. Proving programs as hand simulation with a little induction Infor- mation Processing 74, North-Holland Publ. Co, Amsterdam, 1974 p 308-412 6. Buxton J,. N., Naur P., Randell B. Software Engineering. Petrocelli 1975' Сообщение о двух конференциях НАТО, состоявшихся в Гармшпе, октябрь 19Ь8 г., и в Риме, октябрь 1969 г.) 7. Constable R. L., O'Donnell M. A Programming Logic. Cambridge, 1978 «. Cook ;> A. Axiomatic and interpretative semantics for an Algol fragment University of Toronto, CS TR 79, 1975. "ds"'-"i. 9. Conway R Cries D. An Introduction to Programming. Winlrop Publ., Camb- Г1 Og6, 1 У 1 и. 10. De Millo R. A., Lipton R. J ., Perlis A. J. Social processes and proofs of theorems and programs. Communications of the ACM, v. 22 (May 1979) p 271-280 ю^" ^У' some ''"^'^'""s on advanced programming. Proc. IFIP Congr^ 190z, p. 000-—ОиО. 12' "'"'S't'TMarch^Ol^'? t0 ;>ыетеп1 considered harmful. Communications ACM, 13. Dijkstra E. W A short introduction to the art of programming. EWD316, Eind- 14. DiJ-kstra E. W. Notes on Structured Programming. In Dahl 0. J., HoareC. A R DiJkstra E.W.^ Structured Programming. New York, 1972. (Ест. русский пере^ вод: Э. В. Деикстра в кн. Дал У., Дейкстра Э., Хоор К. Структурное про- граммирование, M.: Мир, 1975. с. 7—97.) ^л'>рноепро 15. Dijkstra E. W. Guarded commands, nondetfcrminacy and tlie fomal derivation of programs. Communications ACM, v. 18 (August 1975), p. 453-457 ю^ ^ Discipline of Programming. Prentice Hall, Englewood Cliffs, M Шil^T1""* "еревол: Д^^^а э- Дисциплина программирования. 17. Dijkstra E. W. Program inversion. EWD671, Eindhoven, 1978 "• Е?1^^1^7'!4"1- А set of Programming exercises. WF25, Eindhoven, July 1979 19. Floyd R. Assigning meaning to programs. In Mathematical Aspects of Computer Science, Providence, 1967, p. 19—32. ^"i" 20. Gentzen G. Untersuchungen liber das logische Schlissen. Math Zeitschrifft v. 39 (1935), p. 176-210, 405-431. (Есть русский перевод: в кн. Хте^ти- ческа.ч теория логического вывода». M.: Наука, 1967 с 4—76 ) 21. Gnes D. An illustration of current ideas on the derivation of correctness proofs с^Ьег^бГГ^^ Transactions on Software Engeneering, v. 2(Dc- 22- o?lWSGЬ(eSp)riЙra^iгrkeT9d781"gy' a collection of articles by members 23. Gnes D., Levin G. Assignments and procedure call proof rules. Theory of Prog- ramming Languages and their Semantics, v. 2 (October 1980), p. 564-579, 24. dries D., Mills H. Swapping sections. TR 81-542, Cornell University, Ithaca January 1981. 25. Guttag J. V., Horning J. J. The algebraic specification of data types. Acta Informatica, v. 10, (1978), p. 27—52. 26. Hoare C.A.R. Quicksort. Computer Journal, v. 5 (1962), p. 10—15. 27. Hoare C.A.R. An axiomatic basis of computer programming. Communications ACM, v. 12 (October 1969), p. 576—5?0, 583. 28. Hoare C.A.R. Procedures and parameters: an axiomatic approach. In Sympo- sium on Semantics of Programming Languages, New York, 1971, p. 102—116. 29. Hoare C.A.R. Proof of correctness of data representation. Acta Informatica, v. 1 (1972), p. 271—281. (Есть русский перевод: в сб. «Данные в языках про- граммирования», М.: Мир, 1982, с. 54—67.) 30. Hoare C.A.R., Wirth N. An axiomatic definition of the programming langu- age Pascal. Acta Informatica, v, 2 (1973), p. 335—355. 31. Hunt J. W., Mcllroy M.D. An algorithm for differential file comparison. CS TR 41, Bell Laboratories, Murray Hill, New Jersey, 1976. 32. Igarashi S., London R. L., Luckham D. C. Authomatic program verification: a logic basis and its implementation. Acta Informatica, v. 4 (1975), p. 145—182. 33. l.iskov В., Zilles S. Programming with abstract data types. Proc. ACM SIG- PLAN Conf. on Very High Level Languages, in SIGPLAN Notices, v. 9 (April 1.974), p. 50—60. 34. London R. L., Guttag J, V., Horning J. J., Mitcheil B. W., Popek G. J. Proof rules for the programming language Euclid. Acta Informatica, v. 10 (1979), p. 1—79. 35. McCarthy J. A basis for a mathematical theory of computation. Proc. Western Joint Сотр. Conf., Los Angeles, May 1961, p. 225-238. 36. Melville R. Asymptotic Complexity of Iterative Computations. Ph. D. Thesis, CS Department, Cornell University, Ithaca, January 1981. 37. Melville R., Gries D. Controlled density sorting. Information Processing Let- ters, v. 10 (July 1980), p. 169—172. 38. Misra J. A. A technique of algorithm construction on sequences. IEEE Tran- sactions on Software Engineering, v. 4 (January 1978), p. 65—69. 39. Naur P. et al. Report on the algorithmic language ALGOL-60. Communications ACM, v. 3 (May 1960^, p. 299-314. 40. Naur P. Proofs of algorithms by general snapshots. BIT, v. 6 (1969), p. 310—316. 41. Quine W.V.O. Methods of Logic. New York, 1961. 42. Steel Т. В. (ed). Formal language description languages for computer program- ming. Proc. IFIP Working Conference on Formal Language Description Lan- guages. Vienna, 1964, Amsterdam, 1971. 43. Szabo M. E. The collected works of Gerhard Gentzen. Amsterdam, 1969. 44. Wirth N. Progtam development by stepwise refinement. Communications ACM, v. 14 (April 1971), p. 221—227. 9.3. Присваивание элементу массива ............... 9.4. Краткое присваивание общего вид;| ............. Глава 10. Команда выбора ...................... Глава 11. Команда повторения ..................... Глава 12. Вызов процедуры ...................... 12.1. Вызовы с входными и выходными параметрами ....... 12.2. Две теоремы о вызове процедуры ............. 12.3. Использование параметров — переменных ........... 12.4. Допуск входных параметров в постусловие .......... ЧАСТЬ III. ПОСТРОЕНИЕ ПРОГРАММ ................ Глава 13. Введение .......................... I Глава 14. Программирование как целенаправленная деятельность. .... Глава 15. Построение циклов, исходя из инвариантов и ограничений . . . 15.1. О первоочередности разработки охраны ............ 15.2. Приближение цикла к завершению ............. Глава 16. Построение инвариантов ..... .............. 16.1. Теория воздушного шарика .......... ........ 16.2. Устранение конъюнктивного члена .............. 16.3. Замена константы переменной ............... 16.4. Расширение области значений переменной ........... 16.5. Комбинирование пред- и постусловий ............ Глава 17. Замечания об ограничивающих функциях .......... Глава 18. Использование циклов вместо рекурсии ........... 18.1. Сведение к более простым задачам .............. 18.2. Разделяй и властвуй .................... 18.3. Обход двоичных деревьев .................. Глава 19. Соображения эффективности ................. 19.1. Ограничение недетерминизма ................. 19.2. Вынесение утверждения из цикла ............... 19.3. Изменение представления данных ............... Глава 20. Два йо.чьших примера построения программ ......... 20.1. Выровненные строки текста ................. 20.2. Максимальная восходящая последовательность ........ Глава 21. Обращение программ .................... Глава 22. Замечания о документации ................. 22.1. Размещение программы при печати .............. 22.2. Определения и описания переменных ............. 22.3. Написание программ на других языках ............ Глава 23. Исюрические замечания ................... 23.1. Краткая история методологии программирования ....... 23.2. Задачи, использованные в книге .............. Приложение 1. Форма Бэкуса — Наура ................. Приложение 2. Множества, последовательности, целые и действительные числа .......................... Приложение 3. Отношения и функции ................. Приложение 4. Асимптотические свойства времени выполнения программ Ответы к упражнениям ........................ Примечания переводчика ....................... Литература ..............................