Технология программирования. - 43 стр.

UptoLike

Рубрика:

- 45 -

Доказательство свойств программы S базируется на свойствах простых опера-

торов языка программирования (пустой оператор и оператор присваивания) и

свойствах базовых элементов структурного программирования (следование, раз-

ветвление и повторение). Эти свойства обычно называют правилами верификации

программ или правилами подтверждения правильности программ.

9.1. Свойства пустого оператора и оператора присваивания

Для пустого оператора справедлива

теорема 1

[1]:

Пусть Р – предикат над IS. Имеет место свойство: {P}{P}.

Доказательство очевидно, так как пустой оператор не изменяет состояние IS по

своей семантике. Другими словами, его предусловие сохраняет истинность и после

его выполнения.

Для оператора присваивания справедлива

теорема 2 [1]:

Пусть IS состоит из переменной Х и оставшейся части RIS

IS = (X, RIS).

Тогда имеет место свойство

{Q(F(X, RIS), RIS)} X: = F(X, RIS) {Q(X, RIS)},

где F(X, RIS) – некоторая

однозначная функция,

Q – предикат.

Доказательство: Пусть (ХØ, RISØ) – некоторое произвольное состояние IS и

пусть перед выполнением оператора присваивания предикат Q(F(XØ, RISØ), RISØ)

истинен. Тогда после выполнения оператора присваивания будет истинен предикат

Q(X, RIS), так как Х получит значение F(XØ, RISØ), а состояние RIS не изменяется

данным оператором присваивания, и, следовательно, после выполнения этого опе-

ратора присваивания Q(X, RIS) = Q(F(XØ, RISØ), RISØ). В силу произвольности

выбора

состояния информационной среды теорема доказана.