2010/05/22 23:32:21

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

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

Содержание

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

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

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

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

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

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

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

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

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

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

Методология программирования

Методология программирования — это совокупность идей, понятий, принципов, способов и средств, определяющая стиль написания, отладки и сопровождения программ.

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

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

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

Технология программирования

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

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

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

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

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

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

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

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

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

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

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

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

См. также

Литература

Наур Наука программирования. М., МИР, 1080.
Турский М. Методология программирования. М., Мир. 1981.
Ершов А. П. Теоретическое программирование. М.,Наука,1980.
Дейкстра Э. Дисциплина программирования. — М.: Мир, 1978.
Криницкий Н. А. Равносильные преобразования программ. М.Радио и Связь. 1976в.
Андерсен Д. Правильность программного обеспечения. М, Мир, 1984.
Каймин В. А. основы доказательного программирования. М., МИЭМ, 1987.
Каймин В. А. Методы разработки программ на языках высокого уровня. М., МИЭМ, 1985.
Бабаев И. О., Герасимов М. А., Косовский Н. К., Соловьев И. П. Интеллектуальное программирование. Турбо-Пролог и Рефал-5 на персональных компьютерах. СПб, изд-во СпбГУ, 1992.
Синицын С. В., Налютин Н. Ю. Верификация программного обеспечения. М.:БИНОМ, 2008.
Каймин В. А., Питеркин В. М. «Основы информатики и ВТ». Пособие для студентов. М.,МИЭМ, 1985.
Каймин В.А и др. «Основы информатики и ВТ». Учебник для средних школ. М.,Просвещение. 1989.
Каймин В. А. Информатика. Учебное пособие для поступающих в вузы. М., Бридж. 1984.
Каймин В. А. Информатика. Учебник для студентов вузов. М.. ИНФРА-М, 1998—2010.
Каймин В. А. Информатика. Учебное пособие для подготовки к экзаменам. М, РИОР, 2004—2008.
Каймин В. А. Информатика. Учебное пособие для школьников. М.,Проспект, 207—2010.