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

UptoLike

Рубрика:

- 47 -

ния условного оператора) будет истинен предикат R. Если же перед выполнением

условного оператора предикат Р будет ложен (а Q, по-прежнему, истинен), то вы-

полнение условного оператора в соответствии с его семантикой сводится к выпол-

нению S2. В силу же свойства оператора S2 после его выполнения (а в этом случае

– и после выполнения условного

оператора) будет истинен предикат R. Таким об-

разом, теорема доказана.

Для дальнейшего рассмотрения нам будет необходима такая логическая операция

как импликация (от латинского implicatio – сплетение), которая обозначается P => Q.

Если P истинно, то оно следует из любого высказывания Q. Если P ложно,

то из него следует любое Q.

Рассмотрим теорему об ослаблении свойств или

теорему 5 [1]:

Пусть:

P, Q, P1, Q1 – предикаты над ИС, для которых справедливы импликации: P1 => P,

Q => Q1 и пусть для оператора S имеет место свойство {P} S {Q}. Тогда имеет ме-

сто свойство: {P1} S {Q1}.

Доказательство:

Пусть для некоторого состояния ИС перед выполнением оператора S истинен

предикат Р1. Тогда, в силу исходной импликации (P1 => P), будет истинен преди-

кат Р. Следовательно, в соответствие со свойствами S после его выполнения будет

истинен предикат Q. А значит в силу исходной импликации (Q => Q1) будет исти-

нен предикат Q1. То есть теорема доказана.

Свойство повторения выражает

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

Пусть: I, P, R, Q – предикаты над информационной средой, для которых спра-

ведливы импликации:

P => Q