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

Категория: Устройства и комплектующие
Нажмите для полного просмотра!
Доказательное программирование, слайд №1Доказательное программирование, слайд №2Доказательное программирование, слайд №3Доказательное программирование, слайд №4Доказательное программирование, слайд №5Доказательное программирование, слайд №6Доказательное программирование, слайд №7Доказательное программирование, слайд №8Доказательное программирование, слайд №9
Скачать
Вы можете ознакомиться и скачать презентацию на тему Доказательное программирование. Доклад-сообщение содержит 9 слайдов. Презентации для любого класса можно скачать бесплатно. Если материал и наш сайт презентаций Mypresentation Вам понравились – поделитесь им с друзьями с помощью социальных кнопок и добавьте в закладки в своем браузере.

Слайды и текст этой презентации

Слайд 1


Доказательное программирование Выполнил: ст. гр. ПИ-21 Львов В. Проверила: Процюк М.П.
Описание слайда:
Доказательное программирование Выполнил: ст. гр. ПИ-21 Львов В. Проверила: Процюк М.П.

Слайд 2


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

Слайд 3


Доказательное программирование, слайд №3
Описание слайда:

Слайд 4


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

Слайд 5


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

Слайд 6


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

Слайд 7


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

Слайд 8


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

Слайд 9


Спасибо за внимание! Спасибо за внимание!
Описание слайда:
Спасибо за внимание! Спасибо за внимание!

Скачать

Похожие презентации
Mypresentation.ru
Загрузить презентацию