рефераты конспекты курсовые дипломные лекции шпоры

Раздел Программирование
/
Правила верификации К. Хоара.

Реферат Курсовая Конспект

Выберите учебное заведение

Правила верификации К. Хоара.

Правила верификации К. Хоара. - раздел Программирование, Математические основы программирования. Теория схем программ. Семантическая теория программ Сформулируем Правила (Аксиомы) К.хоара, Которые Определяют Предусловия Как До...

Сформулируем правила (аксиомы) К.Хоара, которые определяют предусловия как достаточные предусловия, гарантирующие, что исполнение соответствующего оператора при успешном завершении приведет к желаемым постусловиям.

A1. Аксиома присваивания: { Ro } x := Е { R }

Неформальное объяснение аксиомы: так как x после выполнения будет содержать значение Е, то R будет истинно после выполнения, если результат подстановки Е вместо x в R истинен перед выполнением. Таким образом, R_o = R(x) при x = E. Для R_o вводится обозначение: R_o = R^x_Е (у Вирта) или R_x→Е (у Дейкстры), что означает, что x заменяется на Е.

Аксиома присваивания будет иметь вид:{R^x_Е} x := Е {R}.

Сформулируем два очевидных правила монотонности.

A2. Если известно: { Q } S { P } и { P } => { R }, то { Q } S { R }

A3. Если известно: { Q } S { P } и { R } => { Q }, то { R } S { P }

Пусть S - это последовательность из двух операторов S1; S2 (составной оператор).

A4. Если известно:{ Q } S1 { P1 } и { P1 } S2 { R }, то { Q } S { R }.

Это правило можно сформулировать для последовательности, состоящей из n операторов.

Сформулируем правило для условного оператора (краткая форма).

A5. Если известно:

{ Q AND B } S1 { R } и { Q NOT B } => { R },то { Q } if B then S1 { R }.

Правило A5 соответствует интерпретации условного оператора в языке программирования.

Сформулируем правило для альтернативного оператора (полная форма условного оператора).

A6. Если известно: { Q AND B } S1 { R } и { Q NOT B } S2 { R },то { Q } if B then S1 else S2 { R }.

Сформулируем правила для операторов цикла.

Предусловия и постусловия циклаuntil удовлетворяют правилу:

A7. Если известно: { Q AND NOT B } S1 { Q }, то { Q }repeat S1 until B { Q AND NOT B }

Правило отражает инвариантность цикла. В данном случае единственная операция - это выполнение шага цикла при условии истинности Q вначале.

Предусловия и постусловия цикла while удовлетворяют правилу:

A8. Если известно: { Q AND B } S1 { Q } , то { Q } while Bdo S1 { Q AND NOT B }

Правила A1 - A8 можно использовать для проверки согласованности передачи данных от оператора к оператору, для анализа структурных свойств текстов программ, для установления условий окончания цикла и для анализа результатов выполнения программы.

Пример 2.12. Пусть надо определить частное q и остаток r от деления x на y.

Входные данные x, y и выходные данные q, r Î Nat, причем y > 0.

Задать(x,y); /* x,y получают конкретные значения X,Y */

r := x; q := 0;

while y £ r do

Развернуть

Открыть в широком формате

– Конец работы –

Эта тема принадлежит разделу:

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

Следуя А П Ершову мы употребляем термин теоретическое программирование в качестве названия математической дисциплины изучающей синтаксические... В настоящее время сложились следующие основные направления исследований... Математические основы программирования Основная цель исследований развитие математического аппарата...

Если Вам нужно дополнительный материал на эту тему, или Вы не нашли то, что искали, рекомендуем воспользоваться поиском по нашей базе работ: Правила верификации К. Хоара.

Что будем делать с полученным материалом:

Если этот материал оказался полезным ля Вас, Вы можете сохранить его на свою страничку в социальных сетях:

Все темы данного раздела:

Программа как формализованное описание процесса обработки данных
Целью программирования является описание процессов обработки данных (в дальнейшем - просто процессов). Данные - это представление фактов и идей в формализованном виде, пригодном для п

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

Стандартные схемы программ
1.2.1. Базис класса стандартных схем программ Стандартные схемы программ (ССП) характеризуются базисом и структурой схемы. Базис класса фиксирует символы, из которых строятся схем

Свойства и виды стандартных схем программ
1.3.1. Эквивалентность, тотальность, пустота, свобода ССП S в базисе В тотальна (пуста), если для любой интерпретации I базиса В программа (S, I) останавливается (зацикливает

Моделирование стандартных схем программ
1.4.1. Одноленточные автоматы Конечный одноленточный (детерминированный, односторонний) автомат обнаруживают ряд полезных качеств, используемых в теории схем программ для установлен

Рекурсивные схемы
1.5.1. Рекурсивное программирование Среди упомянутых выше методов формализации понятия вычислимой функции метод Тьюринга — Поста основан на уточнении понятия процесса вычислений, для чего

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

Обогащенные и структурированные схемы
1.7.1 Классы обогащенных схем Выделяют следующие классы обогащенных схем: класс счетчиковых схем, класс магазинных схем, класс схем с массивами. Классы счетчиковых и магази

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

Преобразователь предикатов.
Э. Дейкстра рассматривает слабейшие предусловия, т.е. предусловия, необходимые и достаточные для гарантии желаемого результата. «Условие, характеризующее множество всех начальных состояний

Языки формальной спецификации.
Языки и методы формальной спецификации, как средство проектирования и анализа программного обеспечения появились более сорока лет назад. За это время было немало попыток разработать как универсальн

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

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

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

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

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

Основные определения
4.2.1. Теоретико-множественное определение сетей Петри Пусть мультимножество это множество, допускающее вхождение нескольких экземпляров одного и того же элемента. Сеть

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

Then begin
X1:=X1*Y; end; X2:=X2*Y; Y:=Y-1; end; write(X1); write(X2); endРисунок 4.5.

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