|
9.4. Dasturning bajarilishining to'liqligi.
SSda yuzaga kelishi mumkin bo'lgan xatolarga yo'l qo'ymaslik uchun bizni qiziqtirishi mumkin bo'lgan dasturning xususiyatlaridan biri uning to'liqligi, ya'ni. unda ma'lum bir dastlabki ma'lumotlar bilan aylanishning yo'qligi. Biz ko'rib chiqqan tizimli dasturlarda faqat takroriy konstruktsiya aylanma manba bo'lishi mumkin. Demak, dasturning to`liqligini isbotlash uchun sikl operatorining tugatilishini isbotlay olish kifoya. Buning uchun quyidagi foydalidir.
9.7 teorema. Axborot muhitining holatiga bog'liq bo'lgan va quyidagi shartlarni qanoatlantiradigan butun son funksiyasi F bo'lsin:
(1) agar Q predikati axborot muhitining berilgan holati uchun to'g'ri bo'lsa, uning qiymati ijobiy bo'ladi;
(2) S operatorining bajarilishi natijasida axborot muhitining holati o'zgarganda u kamayadi.
Keyin sikl operatorining bajarilishi
WHILE Q DO S ALL WHILE tugallanadi.
Isbot. Tsikl operatori bajarilgunga qadar axborot muhitining holati bo'lsin va F (is) = k bo'lsin. Agar Q (is) predikati noto'g'ri bo'lsa, sikl operatorining bajarilishi tugaydi. Agar Q (bo'lsa) to'g'ri bo'lsa, u holda teorema gipotezasiga ko'ra k> 0 bo'ladi. Bunda S operatori bir yoki bir necha marta bajariladi. S operatori har bir bajarilgandan so'ng teorema gipotezasiga ko'ra, F funksiyaning qiymati kamayadi va S operatori bajarilishidan oldin Q predikati rost bo'lishi kerak (sikl operatorining semantikasiga ko'ra), hozirgi vaqtda F funksiyaning qiymati musbat bo'lishi kerak (teorema shartlariga ko'ra). Demak, F funksiyaning butun qiymati tufayli bu sikldagi S operatori k martadan ortiq bajarilishi mumkin. Teorema isbotlangan.
Masalan, yuqorida ko'rib chiqilgan sikl operatori misolida 9.7-teorema shartlari f (n, m) = n-m funksiya bilan qanoatlantiriladi. m = 1 sikl operatorini bajarishdan oldin bu siklning tanasi (n-1) marta bajariladi, ya'ni. bu tsikl bayonoti tugaydi.
9.5. Dasturning xossasini isbotlashga misol.
Dasturni tekshirishning tasdiqlangan qoidalariga asoslanib, tayinlash operatorlari va bo'sh operatorlardan tashkil topgan va tuzilgan dasturlashning uchta asosiy kompozitsiyasidan foydalangan holda dasturlarning xususiyatlarini isbotlash mumkin. Buning uchun dastur strukturasini tahlil qilib, uning oldindan belgilangan oldindan va keyingi shartlaridan foydalanib, tahlilning har bir bosqichida tegishli tekshirish qoidasini qo'llash kerak. Takroriy kompozitsiyadan foydalanganda siz mos keladigan pastadirni tanlashingiz kerak bo'ladi.
Misol tariqasida mulkni isbotlaylik (9.4). Ushbu dalil quyidagi bosqichlardan iborat bo'ladi.
(1-qadam). n> 0 => (n> 0, p - har qanday, m - har qanday).
(2-qadam). Voqea sodir bo'ladi
(n> 0, p - har qanday, m - har qanday) p: = 1 (n> 0, p = 1, m - har qanday).
9.2 teorema bo'yicha.
(3-qadam). Voqea sodir bo'ladi
(n> 0, p = 1, m - har qanday) m: = 1 (n> 0, p = 1, m = 1).
9.2 teorema bo'yicha.
(4-qadam). Voqea sodir bo'ladi
(n> 0, p - har qanday, m - har qanday) p: = 1; m: = 1 (n> 0, p = 1, m = 1).
2 va 3-bosqichlarning natijalarini hisobga olgan holda 9.3-teorema bo'yicha.
Predikat p = m ekanligini isbotlaylik! tsiklning invariantidir, ya'ni. (p = m m:=m+1; p:=p*m {p=m!}.!}
(5-qadam). Bu sodir bo'ladi (p = m m:=m+1 {p=(m-1)!}.!}
9.2 teorema bo'yicha, agar old shartni (p = ((m + 1) -1) ko'rinishda ifodalasak..!}
(6-qadam). Bu sodir bo'ladi (p = (m-1) p:=p*m {p=m!}.!}
9.2 teorema bo'yicha, agar old shartni (p * m = m) ko'rinishda ifodalasak.!}
(7-qadam). Tsiklning o'zgarmasligi mavjud
(p = m m:=m+1; p:=p*m {p=m!}.!}
5 va 6-bosqichlarning natijalarini hisobga olgan holda 9.3-teorema bo'yicha.
(8-qadam). Voqea sodir bo'ladi
(n> 0, p = 1, m = 1) WHILE m / = n DO
m: = m + 1; p: = p * m
HAZIR HAMMA (p = n.!}
9.6-teorema bo'yicha, 7-bosqich natijasiga ko'ra va (n> 0, p = 1, m = 1) => p = m !; (p = m !, m = n) => p = n !.
(9-qadam). Voqea sodir bo'ladi
(n> 0, p - har qanday, m - har qanday) p: = 1; m: = 1;
WHILE m / = n QILADI
m: = m + 1; p: = p * m
HAZIR HAMMA (p = n.!}
3 va 8-bosqichlarning natijalarini hisobga olgan holda 9.3-teorema bo'yicha.
(10-qadam). (9.4) xossa 1 va 9-bosqichlar natijalari bo‘yicha 9.5-teoremaga mos keladi.
Do'stlaringiz bilan baham: |
