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

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

Доказа́тельное программи́рование — использовавшаяся в 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. Концепция доказательного программирования