Доказательное программирование - разработка алгоритмов и программ без ошибок
и доказательства правильности (доказательствами отсутствия ошибок).
СОДЕРЖАНИЕ КУРСА
-
Введение
Программа - совокупность данных и команд, предназначенных для функционирования ЭВМ.
Программный продукт - надежные программы для работы пользователей на ЭВМ.
Требования к программным продуктам:
- Надежность - отсутствие сбоев и отказов в работе ЭВМ
при выполнении программ.
- Функциональность - наличие у программ определенного набора функций.
- Правильность - правильность результатов при выполнении программ на ЭВМ.
Программист - профессионал должен уметь разрабатывать программы без ошибок.
Э.Дийкстра: только доказательства правильности гарантируют отсутствие ошибок в программах.
-
Технология разработок IBM
Порядок разработки программ/"Каскад"/:
- Выявление требований к программной продукции
- Структурное Проектирование программ
- Кодирование программной продукции
- Тестирование и Испытания программ на ЭВМ
- Документирование и Внедрение программ.
В настоящее время корпорация IBM
в своих разработках использует
Технологию "CleanRoom",
созданную по заказу МинОбороны США:
Обеспечивает удаление более 90% ошибок.
Статистика: 2-3 ошибки на 1000 операторов.
-
Технология разработок MicroSoft
Порядок разработки продукта /"Спираль"/:
- версия 0.1 (альфа-версия)
- версия 1.0 (бета-версия)
- версия 2.0 (первый релиз)
- версия 3.0 (третий релиз)
Обеспечение качества:
- тщательное тестирование на ЭВМ
- "обратная связь" с клиентами
-
Отладка программ на ЭВМ
Отладка программ - процесс поиска и исправления
ошибок в программах на ЭВМ
Особенности отладки программ:
- Количество ошибок в программах - заранее неизвестно.
- Продолжительность отладки программ - заранее неизвестна.
- Количество ошибок в "программном продукте" неизвестно.
- Гарантии качества и надежности программ отсутствуют.
Дийкстра: Тестирование программ не гарантирует отсутствие ошибок.
Статистика IT-проектов в США
- 25% проектов завершаются успешно
- 25% превышают время разработок (в 2-3 раза)
- 25% превышают бюджет разработок (в 2-3 раза)
- 25% завершаются полным провалом
Основная причина: срывов ошибки и дефекты в программной продукции
Официальная статистика:
в российских разработках программного обеспечения
2-3 ошибки на 100 операторов.
Дийкстра: Гарантии в отсутствии ошибок могут дать
только доказательства правильности программ.
-
Стандарты ЕСПД
ЕСПД - Единые Стандарты Программной Документации.
Стандарты ЕСПД были созданы для внедрения
в СССР операционной системы ОС ЕС ЭВМ
(пиратской копии системы OS IBM/360).
Фундамент программы АСУнизации страны (1969-91гг).
Стандарты ЕСПД морально устарели вместе с ЕС ЭВМ.
Основа ЕСПД - обязательное составление блок-схем
для документирования разрабатываемых программ.
В Европе и США блок-схемы не используются вообще.
После введения в Российской Федерации с 1 июля 2003
"Закона о техническом регулировании".
стандарты ЕСПД можно не использовать
для документирования и разработки программ
-
Стандарты ЕСКД
ЕСКД - Единые стандарты на конструкторскую документацию
на любую техническую продукцию: машины, механизмы,
приборы, радиотехнику, средства вычислительной техники.
Надежность технических изделий:
- отказоустойчивость
- ремонтопригодность
- живучесть.
Типология изделий:
- эскизный образец
- рабочий образец
- опытный образец
- серийный образец
Программная документация (по ЕСКД):
- проектная документация
- пользовательская документация
- учебные материалы
- инструкции по установке
-
Применения структурного проектирования
-
Победители и призеры олимпиад и чемпионатов по программированию
составляют алгоритмы и программы практически без ошибок.
Победители используют технологию структурного проектирования программ
с использованием псевдокода, инспекции и тестирования программ на ЭВМ.
C 1999г. российские студенты-программисты систематически побеждают
американские и европейские университетские команды програмистов.
Все победители и призеры чемпионатов и олимпиад используют
структурный псевдокод, а также инспекцию и тестирование программ.
В десятку лучших команд мира систематически входят 4-6 российских команд
каждый год, начиная с 1999г.
По условиям чемпионатов студенческие программы принимаются жюри,
если на всех тестах программы дают правильные результаты.
-
Технология доказательного программирования
Порядок разработки программ:
- Постановка задач
- Составление спецификаций
- Разработка алгоритмов
- Написание программ
- Инспекция программ
- Тестирование программ
- Анализ правильности
- Документирование программ
Доказательное программирование - составление
алгоритмов и программ для ЭВМ с тестированием и
доказательством их правильности.
Более 2000 студентов МИЭМ с 1983 по 1988гг. написали более 5000 программ
с доказательствами правильности по методике Каймина.
Все эти студенты использовали структурный псевдокод, инспекцию текстов
и испытания программ на ЭВМ. После чего писали доказательства правильности,
убедившись в их работоспособности на ЭВМ.
Статистика: 100% устранение всех алгоритмических ошибок.
Только доказательства правильности дают гарантии
отстутствия ошибок в программах.
C 2001 года МинОбороны Великобритании
не принимает программное обеспечение без гарантий
отсутствия в них ошибок.
Применения технологии проектирования программ
Рекомендуемая Литература:
- Каймин В.А.
"Информатика". М., ИНФРА-М, 2003.
- Нечаев А.М. "Программирование ЭВМ". М., МИЭМ, 2003.
- Иан Соммервилл
"Инженерия программного обеспечения" Киев, Вильямс, 2002.
- Липаев В.В. "Качество программных средств". М., МО РФ, 2002.
- Одинцов И. "Профессиональное программирование. Системный подход". СПб.: БХВ-Петербург, 2002.
Авторы курса:
профессор В.А.Каймин, доктор Computer science, академик МАИ
доцент Нечаев А.М., кандидат тех. наук, доцент МИЭМ
(С) В.А.Каймин, 1983-2009.
