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

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

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

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

Методы обучения доказательному программированию
Первые попытки применить подход IBM к подготовке математиков-программистов с первого курса были предприняты в МИЭМ на факультете Прикладной математики в 1980 году.
Методика обучения была основана на использовании русского языка для описания алгоритмов и кодирования соответствующих программ на языках Фортран, Бейсик, Паскаль, Си, ПЛ/1 и т. д.
Через год лучшие студенты стали завершать отладку программ размером 500—600 операторов с первого или второго пуска на ЕС ЭВМ, а еще через два года все студенты ФПМ стали писать программы с доказательствами правильности.

Методы обучения доказательному программированию
Современному машинному программированию свойствен эмпирический подход. ЭВМ — это автомат, который, полностью подчиняясь командам программы, демонстрирует некоторое поведение. Эмпирический характер программирования означает, что правильность программы определяется путем апостериорного (последующего за программированием) наблюдения за поведением машины, исполняющей данную программу. Этот процесс испытания получил название отладки программы и повсюду признается не только неотъемлемым, но и самым трудоемким этапом на пути ее создания.

Поиски систематических методов программирования, обладающего свойством доказательности, имеют уже достаточно длительную историю, восходящую к началу существования электронной вычислительной тех­ники. Сейчас уже можно говорить о создании научных основ доказательного программирования, которые должны стать опорой специальной под­готовки программистов и новой технологической дисциплины программирования. В эту работу внесли вклад ученые из разных стран, в частности , Р. Берсталл, Э. Дейкстра, Дж. Маккарти, М. Нива и др.