Выполнение операторов программы – результаты и допущения
Вычисление выражений
Приоритет операций:
↑ (возведение в степень)
+, - (знак)
*, / (умножение, деление)
+, - (сложение, вычитание)
<, >, =, ≤, ≥, ≠ (операции отношения)
not (записывается также в виде 
)
and (записывается также в виде 
)
or (записывается также в виде 
)
(логическая импликация)
Пример. Массив Y описан для значений индекса только от 1 до 10.
Значения переменных n = 11, х = 3
Пусть требуется вычислить значение выражения (n ≤ 10 and Y[n]=x )
11 ≤ 10 and Y[11]=3
ложно and (не определено = 3)
ложно and не определено
ложно
Выполнение оператора присваивания
x := E(x, y,…)
Аксиома
х′- значение переменной x до выполнения оператора присваивания
х′′- значение переменной x после выполнения оператора присваивания
x′′ = E(x′, y′,…)
y′′ = y′
Основы доказательства корректности
Формулируется математическая теорема о результатах выполнения сегмента программы:
Если условие V (предусловие) истинно непосредственно перед выполнением сегмента программы, тогда после выполнения сегмента тоже истнинно будет условие P (постусловие)
{V} S {P}
V есть предусловие для постусловия P по отношению к оператору S
Оператор частично корректный, если выполнение оператора приводит к получению правильного результата, когда бы он ни завершился.
Оператор полностью корректный, если для частично корректного оператора доказано, что его выполнение действительно заканчивается.
Правила вывода
Правило вывода Р1 – усиление предусловия и ослабление постусловия
Правило вывода А1 – получение предусловия оператора присваивания
{?} x:=E {P}
V = PxE
Чтобы получить предусловие для заданного постусловия Р по отношению к заданному оператору присваивания x:=E, подставим выражение (Е) вместо переменной с именем х всюду, где это имя встечается в постусловии Р.
Правило вывода А2 – Проверка предусловия оператора присваивания
{V} x:=E {P}
Если 
То
{V} x:=E {P}
Правило вывода IF1 - Проверка предусловия условного оператора
Если
{V and B} S1 {P} и
{V and not B} S2 {P}
то
{V} if B then S1 else S2 endif {P}
Правило вывода IF2 – Получение предусловия условного оператора
Если
{V1} S1 {P} и
{V2} S2 {P}
то
{(V1 and B) or (V2 and not B)} if B then S1 else S2 endif {P}
Правило вывода IF3 –Условный оператор
Если
{V1} S1 {P} и
{V2} S2 {P}
то
{V1 and V2 }if B then S1 else S2 endif {P}
Правило вывода IF4 – Условный оператор
Если
{V1 and B} S1 {P} и
{V2 and not B} S2 {P}
то
{V1 and V2 }if B then S1 else S2 endif {P}
Правило вывода S1 – Последовательность операторов
Если
{V} S1 {P1} и
{P1} S2 {P}
то
{V} (S1; S2) {P}
Правило вывода W1 – Цикл с условием продолжения без инициализации
Если
{I and B} S {I}
то
{I} while B do S endwhile {I and not B)
Условие I называют инвариантом цикла.
Правило вывода W2 – Цикл с условием продолжения с инициализацией
Пусть задано условие I (инвариант цикла)
Если
{V} инициализация {I} и
{I and B} S {I} и
{I and not B} P
то
{V} (инициализация; while B do S endwhile ){P}
Чтобы доказать частичную корректность цикла с условием продолжения с помощью праила вывода W2, необходимо:
1. найти инвариант цикла I,
2. доказать, что {V} инициализация {I},
3.доказать, что {I and B} S {I},
4. доказать, что {I and not B} P
Для доказательства, что цикл полностью корректный необходимо дополнительно показать, что цикл завершается.
Правило вывода DC1 – разделяй и властвуй
Если
{V1} S{P1} и
{V2} S {P2}
то
{V1 and V2 } S { P1 and P2 }
Правило вывода DC2 – разделяй и властвуй
Если
{V1} S{P1} и
{V2} S {P2}
то
{V1 orV2 } S { P1 or P2 }
Правило вывода DC3 – разделяй и властвуй
Если
{V} S{P1} и
{V} S {P2}
то
{V } S { P1 and P2 }
Правило вывода DC4 – разделяй и властвуй
Если
{V} S{P1} и
{V} S {P2}
то
{V } S { P1 or P2 }
