технология программирования 2 курс билеты / теоремы

Пусть S нек.обобщённый оператор над инф.средой S, а P и Q нек.предикаты над этой средой
{P}S{Q}-триада хоро, в кот.предикат P-наз.предусловием,а предикат Q-постусловием относительно оператора S.
Говорят что оператор S обладает св-вом {P}S{Q} всякий раз, когда перед. вып. оператора истинен предикат P,а после вып. оператора будет истинен предикат Q.
Теорема 1:
Пусть P-предикат над инф.средой., тогда имеет место с-во {P}{P}, пустой оператор не изм. сост. инф.среды.
Теорема 2:
Пусть инф.среда S состоит из перем. х и ост. части инф.среды R
|S=(x,R|S)
{Q(F(x,R|S),R|S}x:=F(x,R|S){Q(X,R|S)}
F(x,R|S)-нек. однознач. ф-ия
{П=0} П:=П+1 {П=1}
Теорема 3
ПУсть P и R предикат над инф.средой, а S1 и S2-обобщённфе операторы, кот. облад. соотв.св-ми
для I оп.-предусловие P, постусловие Q
{P}S1{Q}
для II оп.-предусловие Q ,постусловие R
{Q}S2{R}
Тогда для сост. опер. будет иметь место св-во:
{P}S1{Q}
=>{P}S1S2{R}
{Q}S2{R}
при. данной теор. явл. любой цикл и сприсваиванием {n<m}n:=n+k{n<m+k}
Теорема 4
Пусть P,Q,R- рпедикаты, а S1,S2-обобщ. операторы, облад. след. св-ми:
{P,Q}S1{R}; {-,P,Q}S2{R}
если P-истина, то вып.оператор S1, если P-ложь, вып. оператор S2
для этих опер. имеет место след. св-ва:
Если P,то S1 иначе S2
{Q}если Р,то S1 иначе S2, если {R}-{n<m+k}n:=3*П{ПБ3*(m+k)}
Теорема 5:
Q->Q1 и для опер. S иммет св-во:предусловие P,опер. S, опстусл. Q
{P}S{Q} тогда имеет место св-во: {P1}S{Q1}
Теорема 6:
Пусть I,P,Q,R-предикаты над инф. средой, для кот. справедливо, что P=>I(I,-,Q)=>R
S-обобщ. опер. облад. св-м:{I}S{I}
тогда для опер.цикла меет место св-во: предусловие P, пока предикат Q условие S,постусловие R
Пример:
пока m<>n выполнять
m:=m+1; p:=p*m
{p=n!}
{n>0,p=1,m=1} пока m<>n выполнять
m:=m+1; p=p*m
{p=n!}