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

UptoLike

Рубрика:

- 46 -

9.2. Свойства базовых конструкций:

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

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

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

Пусть P, Q и R предикаты над ИС, а S1 и S2 – обобщённые операторы, обла-

дающие соответственно свойствами {P} S1 {Q} и {Q} S2 {R}. Тогда для составно-

го оператора S1; S2 имеет место свойство {P} S1; S2 {R}.

Доказательство: Пусть для некоторого состояния информационной среды пе-

ред выполнением оператора S1 истинен предикат Р. Тогда в

силу свойства опера-

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

ставного оператора после выполнения оператора S1 будет выполняться оператор

S2, то предикат Q будет истинен и перед выполнением оператора S2. Следователь-

но, после выполнения оператора S2 в силу его свойства будет истинен предикат R,

а так как оператор S2 завершает выполнение составного

оператора (в соответствии

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

ставного оператора. Что и требовалось доказать. Например:

{n < m} n: = n + k; n: = 3*n {n < 3*(n + m)}.

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

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

Пусть P, Q, R − предикаты над ИС; S1 и S2 − обобщённые операторы со свой-

ствами {P,Q} S1 {R}, {¬ P, Q} S2 {R}.

Тогда для условного оператора

ЕСЛИ Р ТО S1 ИНАЧЕ S2 ВСЁ ЕСЛИ

справедливо

свойство:

{Q} ЕСЛИ Р ТО S1 ИНАЧЕ S2 ВСЁ ЕСЛИ {R}

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

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

предикат Q истинен. Если при этом истинен и предикат Р, то выполнение условно-

го оператора в соответствии с его семантикой сводится к выполнению S1. В силу

свойства оператора S1 после его выполнения (а в этом случае

– и после выполне-