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

программировании в связи с использованием более общих подходов к вопросам

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

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

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

В.А. Каймин

структурированных алгоритмов определяется и объясняется на языке элементарной математики и

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

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

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

— это автомат, который, полностью подчиняясь командам программы, демонстрирует некоторое

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

длительную историю, восходящую к началу существования электронной вычислительной тех­ники. Сейчас

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