Разработка, доказательство корректности

Учебное пособие Редактор А. В. Крейцер Издательство спбгэту «лэти» 1 97376, С. Петербург, ул. Проф. Попова, 5
2. Деревья поиска Идеально сбалансированные бинарные деревья
2 Случайные бинарные деревья поиска
Абракадабра!, содержащий 12 символов, включая специальный символ !
Задача кодирования сообщений. Префиксные коды и деревья Пусть задан алфавит
1 Код Фано-Шеннона
1 Метод Хаффмана
1 Реализация алгоритмов кодирования
1 Доказательство оптимальности кода Хаффмана Лемма 1
1 Энтропийная оценка средней длины кода
1 Динамическое кодирование по Хаффману
Абракадабра!, содержащий 12 символов, включая специальный символ !
Абракадабра!, содержащий 12 символов, включая специальный символ !
А. Ю. Алексеев с. А. Ивановский д. В. Куликов
При обучении программированию особую трудность вызывает работа с динамическими структурами данных
2. стеки и очереди спецификация стека и очереди
3 Определения дерева, леса, бинарного дерева. Скобочное представление
Примечания и библиографические указания
Списки
Задача о порядке перемножения матриц
С. А. Ивановский разработкакорректныхпрограм м санкт-Петербург 2003
Программирования
Разработка, доказательство корректности и анализ алгоритма
2. основы аналитической верификации программ основные правила аналитической верификации программ
3. индуктивные функции на последовательностях
4. корректность программ при работе с массивами
5. поиск в массиве линейный поиск
Разработка, доказательство корректности
Шень А. Программирование: теоремы и задачи: Учеб пособие

скачать doc

О Г Л А В Л Е Н И Е

Введение . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .	3
РАЗРАБОТКА, ДОКАЗАТЕЛЬСТВО КОРРЕКТНОСТИ
И АНАЛИЗ АЛГОРИТМА . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .	4
1.1. Основные определения . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .	4
1.2. Разработка алгоритма . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .	5
1.3. Метод математической индукции . . . . . . . . . . . . . . . . . . . . . . . . . . .	7
1.4. Запись алгоритма и доказательство корректности . . . . . . . . . . . . . .	10
1.5. Анализ алгоритма Евклида . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .	12
1.6. Числа Фибоначчи и анализ алгоритма Евклида . . . . . . . . . . . . . . . .	13
1.7. Бинарный алгоритм нахождения НОД . . . . . . . . . . . . . . . . . . . . . . .	15
1.8. Неструктурированная версия бинарного алгоритма
нахождения НОД . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .	20
1.9. Сравнительные испытания алгоритмов нахождения НОД . . . . . . . .	23
2. ОСНОВЫ АНАЛИТИЧЕСКОЙ ВЕРИФИКАЦИИ ПРОГРАММ . . . . . .	28
2.1. Основные правила аналитической верификации программ . . . . . .	28
2.2. Теорема о цикле, его инварианте и ограничивающей функции . . .	35
2.3. Соотношение между хоаровскими инвариантами цикла и
индуктивными утверждениями Флойда . . . . . . . . . . . . . . . . . . . . . . . . .	36
2.4. Алгоритм возведения в степень . . . . . . . . . . . . . . . . . . . . . . . . . . . . .	40
3. ИНДУКТИВНЫЕ ФУНКЦИИ НА ПОСЛЕДОВАТЕЛЬНОСТЯХ . . . . .	49
3.1. Последовательности и файлы . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .	49
3.2. Индуктивные функции . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .	51
3.3. Стационарные значения индуктивных функций . . . . . . . . . . . . . . .	53
3.4. Индуктивные расширения функций . . . . . . . . . . . . . . . . . . . . . . . . .	54
3.5. Примеры задач с индуктивными функциями . . . . . . . . . . . . . . . . . .	55
4. КОРРЕКТНОСТЬ ПРОГРАММ ПРИ РАБОТЕ С МАССИВАМИ . . . . . .	59
4.1. Кванторы и запись утверждений о массивах . . . . . . . . . . . . . . . . . .	59
4.2. Правила вывода для цикла с параметром . . . . . . . . . . . . . . . . . . . . .	63
4.3. Примеры программ работы с массивами . . . . . . . . . . . . . . . . . . . . .	64
4.4. Задача разделения массива на две части . . . . . . . . . . . . . . . . . . . . . .	68
4.5. Задача слияния упорядоченных массивов . . . . . . . . . . . . . . . . . . . . .	70
4.6. Задачи перестановки и обращения сегментов массива . . . . . . . . . .	72
4.7. Задача о максимальной равнине . . . . . . . . . . . . . . . . . . . . . . . . . . . .	82
5. ПОИСК В МАССИВЕ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .	84
5.1. Линейный поиск . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .	84
5.2. Разработка алгоритма бинарного поиска . . . . . . . . . . . . . . . . . . . . .	86
5.3. Анализ алгоритма бинарного поиска . . . . . . . . . . . . . . . . . . . . . . . .	88
5.4. Оптимизация программы бинарного поиска . . . . . . . . . . . . . . . . . .	92
Список литературы . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .	96
Список условных обозначений . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .	97

Ивановский Сергей Алексеевич
РАЗРАБОТКА КОРРЕКТНЫХ ПРОГРАММ
Учебное пособие
Редактор Э. К. Долгатов
ЛР № 020617 от 24.06.98

------------------------------------------------------------------

Подписано в печать . Формат

. Бумага офсетная.

Печать офсетная. Усл.печ.л. 5.81. Уч.-изд.л. 6.25.

Тираж 170 экз. Заказ

------------------------------------------------------------------

Издательство СПбГЭТУ «ЛЭТИ»

197376, С.-Петербург, ул. Проф. Попова, 5

Учащимся

Учителям