ОГЛАВЛЕНИЕ
Предисловие 7
Математические обозначения 9
0. Ученики чародея в сказочной стране 11
1. Введение 16
1.1Постановка задачи — ошибки в программном обеспечении 16
1.2.Решение — классический подход, заимствованный из техники 17
1.3.Кому адресована эта книга 20
1.4.Основные цели данной книги 21
1.5.Содержание данной книги 21
2. Выполнение операторов программы — результаты и допущения 25
2.1.Вычисление выражений 26
2.2.Выполнение оператора присваивания 27
2.3.Выполнение условного оператора if 29
2.4.Выполнение последовательности операторов 30
2.5.Выполнение цикла с условием продолжения – while 30
2.6.Выполнение вызова подпрограммы call 32
3. Основы доказательства корректности 33
3.1.Определения 34
3.2.Предусловия и постусловия в доказательствах корректности 35
3.3.Правила вывода (доказательства) 36
3.4.Применение правил вывода 54
3.5.Следствия для документации к программам 55
4. Анализ — проверка корректности программы 57
4.1.Оператор присваивания 58
4.2.Условный оператор if 65
4.3.Последовательность операторов 72
4.4.Цикл с условием продолжения – while 73
4.5.Применение правил вывода «разделяй и властвуй» 82
4.6.Подпрограмма или сегмент программы 86
4.7.Заключение — анализ и проверка программы 91
5. Разработка корректной программы 93
5.1.Пример разработки — линейный поиск 95
5.2.Пример разработки — разделение массива на части 100
5.3.Пример разработки — поиск подстроки (подцепочки символов) 108
5.4.Пример разработки — определение позиции следующего имени
в массиве строк 118
5.5.Заключение — разработка программы 127
6.Формулирование предусловий и постусловий 129
6.1.Булевы выражения как язык 129
6.2.Преобразование выражений естественного языка в язык алгебры логики 130
6.3.Дополнительные рекомендации относительно предусловий и постусловий,
а также инвариантов цикла 131
6.4.Небольшой глоссарий "английский (русский) язык - булева, алгебра" 132
6.5.Примеры преобразования выражений в язык алгебры логики 133
6.6.Заключение — формулирование условий на языке алгебры логики 137
7.Заключение 139
7.1.Теоретические основы практического использования подхода создания
программного обеспечения без ошибок 139
7.2.Будущее разработки программного обеспечения 141
Приложение А. Алгебра логики (булева алгебра) 143
А.1.Определения булевых функций 143
А.2.Порядок вычисления функций в выражениях 144
А.3.Основные свойства булевых функций 144
А.4.Упражнения по алгебре логики 146
А.5.Ряды операций И и ИЛИ 147
Приложение Б. Ответы к упражнениям 148
Литература 167
Предметный указатель 169
Справочная карточка по применению правил вывода
Наиболее важные правила вывода:
Р1: усиление предусловия и ослабление постусловия 37
А.1: вывод предусловия оператора присваивания 38
А.2: проверка предусловия оператора присваивания 40
IF1: проверка предусловия условного оператора if 41
IF2 вывод предусловия условного оператора, if 42
S1: последовательность операторов 46
W1: цикл с условием продолжения без инициализации 46
W2: цикл с условием продолжения с инициализацией 47
DC1: разделяй и: властвуй 49
DC3: разделяй и властвуй 51
SP2: подпрограмма или сегмент программы 52