Содержание |
Идея доказательного программирования впервые была высказана академиком А. П. Ершовым, а первый учебник по доказательному программированию был написан В. А. Кайминым. В 1987 году апробирован в рамках курса алгоритмизация и программирования в 1980—1988 годах.
Учебное изложение основ доказательного программирования с примерами разработки алгоритмов и программ на языках Бейсик и Паскаль с доказательствами правильности изложены в учебниках информатики Каймина и для школ, и для вузов.
Математические основы программирования
Математические основы доказательного программирования — это математическая семантика структурированных алгоритмов, заложенная в трудах Флойда, Дейкстры, Ершова и Каймина, а также базовых учебниках информатики Каймина для вузов и школ с описаниями методов анализа правильности структурированных алгоритмов и программ на языках Бейсик, Паскаль, Си, JavaScript и т. д.
В аксиоматике Флойда семантика структурированных алгоритмов описывается с помощью пред- и пост- условий на языке формальной математической логики с инвариантами цикла, плохо понятных как математикам, так и программистам.Бизнес переходит на российское ПО, но отнюдь не массово
В базовых учебниках информатики для вузов и школ семантика структурированных алгоритмов определяется и объясняется на языке элементарной математики и языке математического анализа, изучаемого в технических, математических и экономических вузах и факультетах.
Инварианты циклов в процедурах анализа структурированных алгоритмов заменены на индуктивные утверждения, которые доказываются и обосновываются с помощью математической индукции по индуктивной схеме от частных примеров к общим случаям и утверждениям.
Анализ правильности сложных алгоритмов и программ проводится по частям — блокам и вспомогательным алгоритмам с помощью вспомогательных пред- и пост- утверждений и вспомогательных лемм, как это делается в стандартных курсах и учебниках математического анализа.
Применимость техники математического анализа была перенесена Кайминым на анализ структурированных программ на языках Бейсик, Си и остальных современных языках структурного программирования, использующих циклы, и описана расширенная аксиоматика Флойда—Каймина, в которых для анализа циклов с несколькими выходами используются полуинварианты по точкам выхода из циклов.
Методология программирования
Методология программирования — это совокупность идей, понятий, принципов, способов и средств, определяющая стиль написания, отладки и сопровождения программ.
Методология — система принципов, методов, способов и средств теоретической, практической и производственной деятельности людей, научных и производственных коллективов; в то же время методология является учением о таких системах понятий и деятельности людей.
Программирование — процесс создания компьютерных программ и программного обеспечения для компьютеров и сетей ЭВМ с помощью систем и языков программирования. Программирование сочетает в себе элементы искусства науки, инженерии и ремесла.
Технология программирования — это технология разработки программ и программного обеспечения ЭВМ, отвечающей требованиям высокой надежности и качества, отвечающего требования заказчиков и потребностям пользователей программной продукции.
Технология программирования
Технологии программирования — технологии разработки программ для ЭВМ, которые будут использоваться людьми для решения различных задач на ЭВМ.
Разработка ПО — это род деятельности (профессия) и процесс, направленный на создание и поддержание работоспособности, качества и надежности программного обеспечения, используя технологии, методологию и практики из информатики, управления проектами, математики, инженерии и других областей знания.
Технологии доказательного программирования
Технология доказательного программирования состоит в обязательном структурном проектировании программ с использованием русскоязычного псевдокода и тщательном тестировании разработанных программ на ЭВМ с последующим анализом и доказательством правильности алгоритмов на псевдокоде.
Для доказательства правильности алгоритмов и программ используется математическая семантика структурированных алгоритмов и программ, разработанная и описанная В. А. Кайминым в книгах «Основы доказательного программирования» (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.
Ссылки
- Технологии доказательного программирования
- Методология программирования в Питере
- Концепция доказательного программирования
- Научные основы доказательного программирования
- Информатика для Школ и Вузов
- Информатика: Экзамены на ЭВМ
- Олимпиады по информатике и программированию
- Методы обучения программированию
- Опыт обучения программированию
- Математическая Логика
- Логика в Информатике
- Парадигмы программирования