ТЕХНОЛОГИЯ ДОКАЗАТЕЛЬНОГО ПРОГРАММИРОВАНИЯ

Доказательное программирование - разработка алгоритмов и программ без ошибок
и доказательства правильности (доказательствами отсутствия ошибок).

СОДЕРЖАНИЕ КУРСА

  1. Введение

    Программа - совокупность данных и команд, предназначенных для функционирования ЭВМ.
    Программный продукт - надежные программы для работы пользователей на ЭВМ.

    Требования к программным продуктам:

    • Надежность - отсутствие сбоев и отказов в работе ЭВМ
      при выполнении программ.
    • Функциональность - наличие у программ определенного набора функций.
    • Правильность - правильность результатов при выполнении программ на ЭВМ.

    Программист - профессионал должен уметь разрабатывать программы без ошибок.
    Э.Дийкстра: только доказательства правильности гарантируют отсутствие ошибок в программах.
  2. Технология разработок IBM

    Порядок разработки программ/"Каскад"/:

    • Выявление требований к программной продукции
    • Структурное Проектирование программ
    • Кодирование программной продукции
    • Тестирование и Испытания программ на ЭВМ
    • Документирование и Внедрение программ.

    В настоящее время корпорация IBM
    в своих разработках использует
    Технологию "CleanRoom",
    созданную по заказу МинОбороны США:
    Обеспечивает удаление более 90% ошибок.
    Статистика: 2-3 ошибки на 1000 операторов.

  3. Технология разработок MicroSoft

    Порядок разработки продукта /"Спираль"/:

    • версия 0.1 (альфа-версия)
    • версия 1.0 (бета-версия)
    • версия 2.0 (первый релиз)
    • версия 3.0 (третий релиз)

    Обеспечение качества:

    • тщательное тестирование на ЭВМ
    • "обратная связь" с клиентами
  4. Отладка программ на ЭВМ

    Отладка программ - процесс поиска и исправления
    ошибок в программах на ЭВМ

    Особенности отладки программ:

    • Количество ошибок в программах - заранее неизвестно.
    • Продолжительность отладки программ - заранее неизвестна.
    • Количество ошибок в "программном продукте" неизвестно.
    • Гарантии качества и надежности программ отсутствуют.
    Дийкстра: Тестирование программ не гарантирует отсутствие ошибок.

    Статистика IT-проектов в США

    • 25% проектов завершаются успешно
    • 25% превышают время разработок (в 2-3 раза)
    • 25% превышают бюджет разработок (в 2-3 раза)
    • 25% завершаются полным провалом
    Основная причина: срывов ошибки и дефекты в программной продукции

    Официальная статистика:

    в российских разработках программного обеспечения
    2-3 ошибки на 100 операторов.

    Дийкстра: Гарантии в отсутствии ошибок могут дать
    только доказательства правильности программ.
  5. Стандарты ЕСПД

    ЕСПД - Единые Стандарты Программной Документации.
    Стандарты ЕСПД были созданы для внедрения
    в СССР операционной системы ОС ЕС ЭВМ
    (пиратской копии системы OS IBM/360).
    Фундамент программы АСУнизации страны (1969-91гг).

    Стандарты ЕСПД морально устарели вместе с ЕС ЭВМ.
    Основа ЕСПД - обязательное составление блок-схем
    для документирования разрабатываемых программ.
    В Европе и США блок-схемы не используются вообще.

    После введения в Российской Федерации с 1 июля 2003
    "Закона о техническом регулировании".
    стандарты ЕСПД можно не использовать
    для документирования и разработки программ

  6. Стандарты ЕСКД

    ЕСКД - Единые стандарты на конструкторскую документацию
    на любую техническую продукцию: машины, механизмы,
    приборы, радиотехнику, средства вычислительной техники.

    Надежность технических изделий:

    • отказоустойчивость
    • ремонтопригодность
    • живучесть.

    Типология изделий:

    • эскизный образец
    • рабочий образец
    • опытный образец
    • серийный образец

    Программная документация (по ЕСКД):

    • проектная документация
    • пользовательская документация
    • учебные материалы
    • инструкции по установке

  7. Применения структурного проектирования


  8. Технология побед на Олимпиадах и Чемпионатах

    Победители и призеры олимпиад и чемпионатов по программированию
    составляют алгоритмы и программы практически без ошибок.

    Победители используют технологию структурного проектирования программ
    с использованием псевдокода, инспекции и тестирования программ на ЭВМ.

    C 1999г. российские студенты-программисты систематически побеждают
    американские и европейские университетские команды програмистов.

    Все победители и призеры чемпионатов и олимпиад используют
    структурный псевдокод, а также инспекцию и тестирование программ.

    В десятку лучших команд мира систематически входят 4-6 российских команд
    каждый год, начиная с 1999г.

    По условиям чемпионатов студенческие программы принимаются жюри,
    если на всех тестах программы дают правильные результаты.

  9. Технология доказательного программирования

    Порядок разработки программ:

    • Постановка задач
    • Составление спецификаций
    • Разработка алгоритмов
    • Написание программ
    • Инспекция программ
    • Тестирование программ
    • Анализ правильности
    • Документирование программ

    Доказательное программирование - составление
    алгоритмов и программ для ЭВМ с тестированием и
    доказательством их правильности.

    Более 2000 студентов МИЭМ с 1983 по 1988гг. написали более 5000 программ с доказательствами правильности по методике Каймина.

    Все эти студенты использовали структурный псевдокод, инспекцию текстов
    и испытания программ на ЭВМ. После чего писали доказательства правильности,
    убедившись в их работоспособности на ЭВМ.
    Статистика: 100% устранение всех алгоритмических ошибок.
    Только доказательства правильности дают гарантии
    отстутствия ошибок в программах.

    C 2001 года МинОбороны Великобритании
    не принимает программное обеспечение без гарантий
    отсутствия в них ошибок.

    Применения технологии проектирования программ

Рекомендуемая Литература:

  1. Каймин В.А. "Информатика". М., ИНФРА-М, 2003.
  2. Нечаев А.М. "Программирование ЭВМ". М., МИЭМ, 2003.
  3. Иан Соммервилл "Инженерия программного обеспечения" Киев, Вильямс, 2002.
  4. Липаев В.В. "Качество программных средств". М., МО РФ, 2002.
  5. Одинцов И. "Профессиональное программирование. Системный подход". СПб.: БХВ-Петербург, 2002.
Авторы курса:
профессор В.А.Каймин
, доктор Computer science, академик МАИ
доцент Нечаев А.М., кандидат тех. наук, доцент МИЭМ

(С) В.А.Каймин, 1983-2009.

Hosted by uCoz