Наука программирования

Грис Д.

От автора:
“Программирование начиналось как искусство; даже сейчас большинство учится ему, наблюдая, как работают другие (например, преподаватель или более опытный коллега), постигая приемы и мало задумываясь над принципами, которые лежат в их основе. Однако в результате научных исследований последнего десятилетия найдены некоторые полезные теоретические положения и общие принципы, так что наступает время, когда можно начинать учить принципам и их осознанному применению. В этом учебнике я сделал попытку поделиться своим пониманием возникающей на наших глазах науки программирования и восхищением ею”.

---

Table of contents :
ОГЛАВЛЕНИЕ……Page 414
ВСТУПЛЕНИЕ……Page 6
ПРЕДИСЛОВИЕ……Page 7
ЧАСТЬ 0. ЗАЧЕМ НУЖНО ИСПОЛЬЗОВАТЬ ЛОГИКУ И ДОКАЗЫВАТЬ ПРАВИЛЬНОСТЬ ПРОГРАММ? 12……Page 11
ЧАСТЬ I. ВЫСКАЗЫВАНИЯ И ПРЕДИКАТЫ 17……Page 16
1.1. Высказывания с полным набором скобок 18……Page 17
1.2. Вычисление постоянных высказываний 19……Page 18
1.3. Вычисление высказываний в данном состоянии 21……Page 20
1.4. Правила старшинства для операций 22……Page 21
1.5. Тавтологии 24……Page 23
1.6. Высказывания как множества состояний 25……Page 24
1.7. Переводе естественного языка на язык высказываний 26……Page 25
2.1. Законы эквивалентности 28……Page 27
2.2. Правила подстановки и транзитивности 31……Page 30
2.3. Формальная система аксиом и правил вывода 34……Page 33
3.1. Введение в дедуктивные доказательства 37……Page 36
3.2. Правила вывода 39……Page 38
3.3. Выводы и подвыводы 44……Page 43
3.4. Увеличение гибкости системы естественного вывода 53……Page 52
3.5. Построение доказательств в системе естественного вывода 60……Page 59
4.1. Расширение области значений состояния 74……Page 73
4.2. Кванторы 79……Page 78
4.3. Свободные и связанные идентификаторы 83……Page 82
4.4. Подстановка 86……Page 85
4.5. Кванторы по другим областям 89……Page 88
4.6. Несколько теорем о подстановке и состояниях 92……Page 91
5.1. Одномерный массив как функция 94……Page 93
5.2. Сегменты массивов и картинки массивов 99……Page 98
5.3. Обращение с массивами массивов 102……Page 101
6.1. Спецификации программ 105……Page 104
6.2. Представление начальных и конечных значений переменных 108……Page 107
6.3. Наброски доказательств 109……Page 108
ЧАСТЬ II. СЕМАНТИКА ПРОСТОГО ЯЗЫКА ПРОГРАММИРОВАНИЯ 112……Page 111
Глава 7. Преобразователь предикатов WP 113……Page 112
Глава 8. Команды SKIP, ABORT и композиция команд 119……Page 118
9.1. Присваивание простым переменным 122……Page 121
9.2. Кратные присваивания простым переменным 126……Page 125
9.3. Присваивание элементу массива 129……Page 128
9.4. Краткое присваивание общего вида 131……Page 130
Глава 10. Команда выбора 136……Page 135
Глава 11. Команда повторения 143……Page 142
Глава 12. Вызов процедуры 153……Page 152
12.1. Вызовы с входными и выходными параметрами 154……Page 153
12.2. Две теоремы о вызове процедуры 157……Page 156
12.3. Использование параметров — переменных 162……Page 161
12.4. Допуск входных параметров в постусловие 164……Page 163
Глава 13. Введение 167……Page 166
Глава 14. Программирование как целенаправленная деятельность 176……Page 175
15.1. О первоочередности разработки охраны 183……Page 182
15.2. Приближение цикла к завершению 189……Page 188
16.1. Теория воздушного шарика 196……Page 195
16.2. Устранение конъюнктивного члена 198……Page 197
16.3. Замена константы переменной 202……Page 201
16.4. Расширение области значений переменной 209……Page 208
16.5. Комбинирование пред- и постусловий 214……Page 213
Глава 17. Замечания об ограничивающих функциях 219……Page 218
Глава 18. Использование циклов вместо рекурсии 224……Page 223
18.1. Сведение к более простым задачам 225……Page 224
18.2. Разделяй и властвуй 229……Page 228
18.3. Обход двоичных деревьев 232……Page 231
19.1. Ограничение недетерминизма 241……Page 240
19.2. Вынесение утверждения из цикла 244……Page 243
19.3. Изменение представления данных 249……Page 248
20.1. Выровненные строки текста 256……Page 255
20.2. Максимальная восходящая последовательность 261……Page 260
Глава 21. Обращение программ 268……Page 267
22.1. Размещение программы при печати 278……Page 277
22.2. Определения и описания переменных 286……Page 285
22.3. Написание программ на других языках 289……Page 288
23.1. Краткая история методологии программирования 297……Page 296
23.2. Задачи, использованные в книге 304……Page 303
Приложение 1. Форма Бэкуса — Наура 307……Page 306
Приложение 2. Множества, последовательности, целые и действительные числа 313……Page 312
Приложение 3. Отношения и функции 318……Page 317
Приложение 4. Асимптотические свойства времени выполнения программ 323……Page 322
Глава 01. Высказывания……Page 325
Глава 02. Рассуждения при помощи эквивалентных преобразований……Page 327
3.2……Page 333
3.3……Page 335
3.4……Page 344
3.5……Page 350
4.1……Page 351
4.2……Page 353
4.4……Page 354
5.1……Page 355
5.2……Page 356
6.2……Page 357
Глава 07. Преобразователь предикатов……Page 359
Глава 08. Команды SKIP, ABORT и композиция команд……Page 361
9.1……Page 362
9.2……Page 363
9.4……Page 366
Глава 10. Команда выбора……Page 368
Глава 11. Команда повторения……Page 369
Глава 12. Вызов процедуры……Page 375
Глава 14. Программирование как целенаправленная деятельность……Page 377
15.1……Page 379
15.2……Page 381
16.2……Page 382
16.3……Page 383
16.5……Page 386
18.1……Page 391
18.2……Page 392
18.3……Page 393
19.2……Page 395
19.3……Page 397
Глава 20. Два больших примера построения программ……Page 400
ПРИМЕЧАНИЯ ПЕРЕВОДЧИКА 410……Page 409
ЛИТЕРАТУРА 413……Page 412