Понятие частичной и полной корректности программы, правила вывода – общий вид, правила консеквенции

Любой оператор или изменяет состояние вычислений… или анализирует и принимает решение…

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

Задача: описать соотношения и правила вывода, которые позволят определить эффект воздействия простого оператора на состояние вычислений и выделить свойства составного оператора из свойств входящих в него простых операторов.

На структурной схеме нахождения div и mod определены состояния вычислений с помощью соотношений, которые должны выполняться для входных и промежуточных величин.

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

Спецификация программы и правила вывода

Спецификация программы: S

{ P} S { Q } (1) -Q

Если соотношение P – истинно перед выполнением S, то после завершения выполнения S, будет истинно выражение Q. …

Если S - это программа, корректность которой мы должны установить, то необходимо доказать нотацию (1), где P – соотношение, которому должны удовлетворять входные данные, а Q – выходные.

Для задачи поиска div и nod:

{(x ≥ 0) ^ (y > 0)} S {(x = q * y + r) ^ (0 ≤ r < y)}

Соотношение (1) определяет частичную корректность программы, так как S может не завершаться, точка выхода может не достигаться. Завершаемость S необходимо доказать, тогда будет доказана полная корректность.

Проектирование должно начинаться с определения спецификации {P} S {Q}, которой должна удовлетворять проектируемая программа, при каких условиях она должна работать (предусловие P) и какие результаты должны быть получены, каким условиям должны удовлетворять выходные данные (постусловие Q).

Процесс проектирования сверху вниз определяет спецификации {Pi} Si {Qi} для компонент программы Si

Проектирование программы осуществляется одновременно с доказательством корректности этих спецификаций.

Представим структурную схему алгоритма поиска div и mod с учетом ее декомпозиции.

Представим блок-схему этого алгоритма с учетом его декомпозиции

x>=0, y>0 x>=0, y> 0

s1 q = 0;

r>=0 s1 r = x;

s3

x=q*y+r, 0<= r<y x=q*y+r, r>=0

x=q*y + r, r>=y

S3 r = r – y;

s2 q = q + 1;

x = q * y +r , r>=O

Правила вывода

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

H1,H2,…Hn

H

Если над чертой истинные выражения, то и под чертой выражение будет истинным.

Первое правило консеквенции:

{P} S {R}, R Q

{P} S {Q}

Например:

{(x > 0) ^ (y > 0)} S {(z + u * Y = x * y) ^ (u = 0)},

(z + u * Y = x * y) ^ (u = 0) (z = x * y)

{(x > 0) ^ (y > 0)} S {(z = x * y)}

Второе правило консеквенции:

P R, {R} S {Q}

{P} S {Q}

Например:

((x = y * q + r) ^ (r > y)) (x = y * (1 + q) + (r – y),

{x = y * (1 + q) + (r – y)} r = r – y { x = y * (1 + q) + r}

{(x = y * q + r) ^ (r > y)} r = r – y { x = y * (1 + q) + r}

Правила вывода для операторов: пустого, присваивания, составного.

Правила вывода для операторов языка программирования

Правила вывода для структурных операторов