8-ma'ruza. Dasturiy ta'minot modulini ishlab chiqish


Dasturning bajarilishining to'liqligi



Download 112,44 Kb.
bet9/50
Sana07.04.2022
Hajmi112,44 Kb.
#534692
1   ...   5   6   7   8   9   10   11   12   ...   50
Bog'liq
Modullar

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.

    1. 9.5. Dasturning xossasini isbotlashga misol.

    2. 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.


    1. Download 112,44 Kb.

      Do'stlaringiz bilan baham:
  • 1   ...   5   6   7   8   9   10   11   12   ...   50




    Ma'lumotlar bazasi mualliflik huquqi bilan himoyalangan ©hozir.org 2024
    ma'muriyatiga murojaat qiling

    kiriting | ro'yxatdan o'tish
        Bosh sahifa
    юртда тантана
    Боғда битган
    Бугун юртда
    Эшитганлар жилманглар
    Эшитмадим деманглар
    битган бодомлар
    Yangiariq tumani
    qitish marakazi
    Raqamli texnologiyalar
    ilishida muhokamadan
    tasdiqqa tavsiya
    tavsiya etilgan
    iqtisodiyot kafedrasi
    steiermarkischen landesregierung
    asarlaringizni yuboring
    o'zingizning asarlaringizni
    Iltimos faqat
    faqat o'zingizning
    steierm rkischen
    landesregierung fachabteilung
    rkischen landesregierung
    hamshira loyihasi
    loyihasi mavsum
    faolyatining oqibatlari
    asosiy adabiyotlar
    fakulteti ahborot
    ahborot havfsizligi
    havfsizligi kafedrasi
    fanidan bo’yicha
    fakulteti iqtisodiyot
    boshqaruv fakulteti
    chiqarishda boshqaruv
    ishlab chiqarishda
    iqtisodiyot fakultet
    multiservis tarmoqlari
    fanidan asosiy
    Uzbek fanidan
    mavzulari potok
    asosidagi multiservis
    'aliyyil a'ziym
    billahil 'aliyyil
    illaa billahil
    quvvata illaa
    falah' deganida
    Kompyuter savodxonligi
    bo’yicha mustaqil
    'alal falah'
    Hayya 'alal
    'alas soloh
    Hayya 'alas
    mavsum boyicha


    yuklab olish