Доказательное программирование

Доказательное программирование

Доказательное программирование

Доказа́тельное программи́рование — использовавшаяся в 1980-х годах в академических кругах технология разработки программ для ЭВМ с доказательствами правильности — доказательствами отсутствия ошибок в программах (понимая, в рамках данной теории, ошибки как несоответствия между программой и реализуемым ею алгоритмом).

Содержание

Актуальность

В настоящее время теория доказательного программирования утратила актуальность в промышленном программировании в связи с использованием более общих подходов к вопросам надёжности программного обеспечения и смещением внимания к ошибкам других типов, не рассматриваемых в данной теории. Так, действующий стандарт ГОСТ Р 51904-2002 требует контролировать 23 вида ошибок в программах, из которых методами доказательного программирования выявляются и устраняются только несколько простейших. К часто встречающимся в настоящее время, но не контролируемым методами доказательного программирования, ошибкам — относятся, в частности, ошибки в интерфейсах аппаратных/программных средств, некорректное поведение циклов обратной связи вне программы, некорректная реакция на переходные процессы в аппаратуре или аппаратные отказы, нарушения разбиения ПО и пр.[1]

С другой стороны, к этому подходу примыкают и частично пересекаются с ним такие известные подходы, как защищённое программирование (лёгшее в основу языка Pascal), технологии верификации программ [2], контрактное программирование (язык Eiffel) и т.д.

История

Идея доказательного программирования впервые была высказана академиком А. П. Ершовым, а первый учебник по доказательному программированию был написан В. А. Кайминым. В 1987 году апробирован в рамках курса алгоритмизация и программирования в 1980—1988 годах. Учебное изложение основ доказательного программирования с примерами разработки алгоритмов и программ на языках Бейсик и Паскаль с доказательствами правильности изложены в учебниках информатики Каймина и для школ, и для вузов.

Математические основы доказательного программирования

Математические основы доказательного программирования — это математическая семантика структурированных алгоритмов, заложенная в трудах Флойда, Дейкстры, Ершова и Каймина, а также базовых учебниках информатики Каймина для вузов и школ с описаниями методов анализа правильности структурированных алгоритмов и программ на языках Бейсик, Паскаль, Си, JavaScript и т. д.

В аксиоматике Флойда семантика структурированных алгоритмов описывается с помощью пред- и пост- условий на языке формальной математической логики с инвариантами цикла, плохо понятных как математикам, так и программистам.

В базовых учебниках информатики для вузов и школ семантика структурированных алгоритмов определяется и объясняется на языке элементарной математики и языке математического анализа, изучаемого в технических, математических и экономических вузах и факультетах.

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

Анализ правильности сложных алгоритмов и программ проводится по частям — блокам и вспомогательным алгоритмам с помощью вспомогательных пред- и пост- утверждений и вспомогательных лемм, как это делается в стандартных курсах и учебниках математического анализа.

Применимость техники математического анализа была перенесена Кайминым на анализ структурированных программ на языках Бейсик, Си и остальных современных языках структурного программирования, использующих циклы, и описана расширенная аксиоматика Флойда—Каймина, в которых для анализа циклов с несколькими выходами используются полуинварианты по точкам выхода из циклов.

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

Технология доказательного программирования состоит в обязательном структурном проектировании программ с использованием русскоязычного псевдокода и тщательном тестировании разработанных программ на ЭВМ с последующим анализом и доказательством правильности алгоритмов на псевдокоде.

Для доказательства правильности алгоритмов и программ используется математическая семантика структурированных алгоритмов и программ, разработанная и описанная В. А. Кайминым в книгах «Основы доказательного программирования» (1987) и «Методы разработки программ на языках высокого уровня».

Методы обучения программированию

Первые попытки применить подход IBM к подготовке математиков-программистов с первого курса были предприняты в МИЭМ на факультете Прикладной математики в 1980 году.

Методика обучения была основана на использовании русского языка для описания алгоритмов и кодирования соответствующих программ на языках Фортран, Бейсик, Паскаль, Си, ПЛ/1 и т. д.

Через год лучшие студенты стали завершать отладку программ размером 500—600 операторов с первого или второго пуска на ЕС ЭВМ, а еще через два года все студенты ФПМ стали писать программы с доказательствами правильности.

Методика обучения элементам программирования на основе псевдокода была заложена в учебник по информатике студентов МИЭМ в 1985 году, а затем для средних школ, разошедшийся миллионным тиражом [3].

Основы алгоритмизации во всех российских учебниках информатики до сих пор используют лексику родного русского языка для описания семантики основных алгоритмических конструкций.

Примечания

  1. ГОСТ Р 51904-2002
  2. П.Грогоно, Программирование на языке Pascal, М.:Мир, 1982, с.295, Тестирование и верификация

См. также

Литература

  1. Синицын С. В., Налютин Н. Ю. Верификация программного обеспечения. М.:БИНОМ, 2008.
  2. Каймин В. А. Информатика. Учебное пособие для школьников. М.,Проспект, 207—2010.

Ссылки

  1. Технологии доказательного программирования
  2. Методология программирования в Питере
  3. Концепция доказательного программирования

Wikimedia Foundation. 2010.

Смотреть что такое "Доказательное программирование" в других словарях:

  • Парадигма (программирование) — Парадигма программирования  это совокупность идей и понятий, определяющая стиль написания программ. Парадигма, в первую очередь, определяется базовой программной единицей и самим принципом достижения модульности программы. В качестве этой единицы …   Википедия

  • Формальная верификация — формальное доказательство соответствия или несоответствия формального предмета верификации его формальному описанию. Предметом выступают алгоритмы, программы и другие доказательства. Из за рутинности даже простой формальной верификации и… …   Википедия

  • Логика в компьютерных науках — Логика в информатике это направления исследований и отрасли знания, где логика применяется в информатике и искусственном интеллекте. Логика оказалась гораздо более эффективной в информатике, чем это было в математике[1]. Включаются следующие… …   Википедия

  • Логика в информатике — Логика в информатике  это направления исследований и отраслей знания, где логика применяется в информатике и искусственном интеллекте. Логика очень эффективна в этих областях[1]. Содержание 1 Область применения …   Википедия

  • Парадигма программирования — Парадигмы программирования Агентно ориентированная Компонентно ориентированная Конкатенативная Декларативная (контрастирует с Императивной) Ограничениями Функциональная Потоком данных Таблично ориентированная (электронные таблицы) Реактивная …   Википедия

  • Логический язык программирования — Логическое программирование парадигма программирования, основанная на автоматическом доказательстве теорем, а также раздел дискретной математики, изучающий принципы логического вывода информации на основе заданных фактов и правил вывода.… …   Википедия

  • Язык логического программирования — Логическое программирование парадигма программирования, основанная на автоматическом доказательстве теорем, а также раздел дискретной математики, изучающий принципы логического вывода информации на основе заданных фактов и правил вывода.… …   Википедия

  • Процесс разработки программного обеспечения — Разработка программного обеспечения Процесс разработки ПО Шаги процесса Анализ • Проектирование • Программирование • …   Википедия

  • Языки программирования — Язык программирования  формальная знаковая система, предназначенная для записи программ. Программа обычно представляет собой некоторый алгоритм в форме, понятной для исполнителя (например, компьютера). Язык программирования определяет набор… …   Википедия

  • Логика — Гр …   Википедия


Поделиться ссылкой на выделенное

Прямая ссылка:
Нажмите правой клавишей мыши и выберите «Копировать ссылку»