|
9.2. Oddiy operatorlarning xossalari.
Bo'sh operator uchun quyidagilar to'g'ri keladi
9.1 teorema. P axborot muhitiga nisbatan predikat bo'lsin. Keyin (P) (P) xossasi o'rinli bo'ladi.
Bu teoremaning isboti yaqqol ko'rinib turibdi: bo'sh operator axborot muhitining holatini (semantikasiga muvofiq) o'zgartirmaydi, shuning uchun uning old sharti bajarilgandan keyin ham to'g'ri bo'lib qoladi.
Topshiriq operatori qanoatlantiradi
9.2 teorema. IS axborot muhiti X o'zgaruvchidan va RIS axborot muhitining qolgan qismidan iborat bo'lsin:
Keyin mulk
(Q (F (X, RIS), RIS)) X: = F (X, RIS) (Q (X, RIS)),
Bu erda F (X, RIS) - bir qiymatli funktsiya, Q - predikat.
Isbot. Tayinlash operatori bajarilishidan oldin Q (F (X0, RIS0), RIS0) predikati rost bo'lsin, bu erda (X0, RIS0) IS axborot muhitining qandaydir ixtiyoriy holati, keyin tayinlash operatori bajarilgandan keyin predikat. Q (X, RIS) to'g'ri bo'ladi, shuning uchun X qanday qilib F qiymatini oladi (X0, RIS0) va RIS holati bu tayinlash operatori tomonidan o'zgartirilmaydi va shuning uchun bu tayinlash operatori bajarilgandan keyin bu holda
Q (X, RIS) = Q (F (X0, RIS0), RIS0).
Axborot muhiti holatini tanlashning o'zboshimchaligi tufayli teorema isbotlangan.
9.1-misol tayinlash operatorining xossalariga misoldir.
9.3. Strukturaviy dasturlashning asosiy tuzilmalarining xossalari.
Endi strukturali dasturlashning asosiy tuzilmalarining xossalarini ko'rib chiqamiz: ketma-ketlik, tarmoqlanish va takrorlash.
Suksessiyaning xossalari quyidagilar bilan ifodalanadi
9.3 teorema. P, Q va R axborot muhiti bo‘yicha predikatlar, S1 va S2 esa xossalarga ega umumlashtirilgan operatorlar bo‘lsin.
(P) S (Q) va (Q) S2 (R).
Keyin birikma operatori uchun
S1; S2<.blockquote>
mulk egalik qiladi
(P) S1; S2 (R).
Isbot. S1 operatori bajarilgunga qadar axborot muhitining ba'zi holati uchun P predikati to'g'ri bo'lsin.U holda S1 operatorining xossasi tufayli u bajarilgandan so'ng Q predikati rost bo'ladi.S2 bayonining bajarilishi. Shuning uchun S2 operatori bajarilgandan so'ng o'z xossasiga ko'ra R predikati rost bo'ladi va S2 operatori kompozit operatorning bajarilishini tugatganligi uchun (semantikasiga ko'ra), R predikati to'g'ri bo'ladi. isbotlash uchun zarur bo'lgan ushbu kompozit operatorning bajarilishi.
Misol uchun, agar (9.2) va (9.3) xossalari mavjud bo'lsa, unda mavjud
joylashuvi va mulki
(n<3*(m+k)}.<="" p="">
Tarmoqlanish xossasi quyidagilarni ifodalaydi
9.4 teorema. P, Q va R axborot muhiti bo‘yicha predikatlar, S1 va S2 esa xossalarga ega umumlashtirilgan operatorlar bo‘lsin.
(P, Q) S1 (R) va (`P, Q) S2 (R).
Keyin shartli operator uchun
AGAR P BO'LSA S1 BOSHQA S2 HAMMA IF
mulk egalik qiladi
(Q) AGAR P BO'LSA S1 BOSHQA S2 HAMMA AGAR (R).
Isbot. Shartli operator bajarilishidan oldin axborot muhitining ma'lum bir holati uchun Q predikati rost bo'lsin.Agar P predikati ham rost bo'lsa, u holda shartli operatorning semantikasiga muvofiq bajarilishi operatorning bajarilishiga qisqaradi. S1. S1 operatorining xossalari tufayli, u bajarilgandan so'ng (va bu holda, shartli operator bajarilgandan keyin) R predikati rost bo'ladi.Agar shart operatori bajarilishidan oldin, P predikati noto'g'ri bo'lsa. (va Q hali ham to'g'ri), keyin shartli operatorning semantikasiga muvofiq bajarilishi S2 operatorining bajarilishiga qisqartiriladi. S2 operatorining xossasi tufayli, u bajarilgandan so'ng (va bu holda - va shartli operator bajarilgandan keyin) R predikati to'g'ri bo'ladi.Shunday qilib, teorema to'liq isbotlangan.
Takrorlash konstruktsiyasining xususiyatiga o'tishdan oldin, u keyingi uchun foydali ekanligini ta'kidlash kerak
9.5 teorema. P, Q, P1 va Q1 oqibatlar o'rinli bo'lgan axborot muhitiga nisbatan predikatlar bo'lsin
P1 => P va Q => Q1,
va S operator uchun (P) S (Q) xossasi o‘rinli bo‘lsin. Keyin (P1) S (Q1) xossa o‘rinli bo‘ladi.
Bu teorema xossaning zaiflashuv teoremasi deb ham ataladi.
Isbot. S operatori bajarilgunga qadar axborot muhitining qandaydir holati uchun P1 predikati to'g'ri bo'lsin. U holda P predikati ham to'g'ri bo'ladi (P1 => P implikatsiyasi tufayli). Demak, S operatorining xossasi tufayli u bajarilgandan so'ng Q predikati rost bo'ladi, demak Q1 predikati (Q => Q1 implikatsiyasiga ko'ra) bo'ladi. Bu teoremani isbotlaydi.
Takrorlash xossasi quyidagilarni ifodalaydi
9.6 teorema. I, P, Q va R oqibatlar o'rinli bo'lgan axborot muhitiga predikatlar bo'lsin
P => I va (I, `Q) => R,
va (I) S (I) xossaga ega S umumlashtirilgan operator bo‘lsin.
Keyin tsikl operatori uchun
WHILE Q HAMMANI QILADI
mulk egalik qiladi
(P) Q HAZIR HAMMANI QILADI (R).
I predikat sikl operatorining invarianti deyiladi.
Isbot. Bu teoremani isbotlash uchun xossani isbotlash kifoya
(I) Q HAMMANI QILADI (I, `Q)
(9.5-teorema bo'yicha ushbu teorema shartlariga ta'sir qilish asosida). Tsikl operatori bajarilgunga qadar axborot muhitining qandaydir holati uchun I predikati rost bo'lsin.Agar bu holda Q predikati yolg'on bo'lsa, u holda sikl operatori bo'sh operatorga (semantikasiga muvofiq) ekvivalent bo'ladi. ) va 9.1 teoremaga ko'ra, tsikl operatori bajarilgandan so'ng, (I , `Q) bayonoti. Agar sikl operatori bajarilgunga qadar Q predikati rost bo'lsa, sikl operatori o'z semantikasiga ko'ra S birikma operatori sifatida ifodalanishi mumkin; WHILE Q HAMMANI QILADI
S operatorining xususiyati tufayli, u bajarilgandan so'ng, I predikati rost bo'ladi va sikl operatorining xususiyatini isbotlash uchun dastlabki holat yuzaga keladi: I predikat tsikl operatori bajarilishidan oldin rost, lekin boshqasi uchun ( o'zgartirilgan) axborot muhitining holati (buning uchun Q predikati to'g'ri yoki noto'g'ri bo'lishi mumkin). Agar sikl operatorining bajarilishi tugasa, u holda matematik induksiya usulini chekli bosqichlarda qo'llagan holda, (I, `Q) bayoni bajarilgunga qadar to'g'ri bo'ladigan holatga kelamiz. Va bu holatda, yuqorida isbotlanganidek, bu gap sikl operatori bajarilgandan keyin ham to'g'ri bo'ladi. Teorema isbotlangan.
Masalan, (9.4) misoldagi sikl operatori xossaga ega
m: = m + 1; p: = p * m
HAZIR HAMMA (p = n.!}
Bu 9.6 teoremadan kelib chiqadi, chunki bu sikl operatorining invarianti p = m predikatdir! va xulosalar to'g'ri (n> 0, p = 1, m = 1) => p = m! va (p = m !, m = n) => p = n!
Do'stlaringiz bilan baham: |
