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

8.4. Dastur modulini boshqarish.

Dasturiy ta'minot modulini boshqarish uchun quyidagi usullar qo'llaniladi:

modul matnini statik tekshirish;
oxirigacha kuzatish;
dastur modulining xususiyatlarini isbotlash.
Modul matnini statik tekshirishda moduldagi xatolarni topish uchun ushbu matn boshidan oxirigacha o‘qiladi. Odatda, bunday tekshirish uchun modul ishlab chiqaruvchisidan tashqari, bir yoki hatto bir nechta dasturchilar jalb qilinadi. Bunday tekshirish paytida aniqlangan xatolarni darhol tuzatmaslik tavsiya etiladi, lekin modul matnini o'qish tugagandan so'ng.
Kuzatuv dinamik modul boshqaruvining bir turi hisoblanadi. Bu, shuningdek, ma'lum testlar to'plami bo'yicha modulning bajarilishini (modulning ishlash mantig'idan kelib chiqadigan ketma-ketlikda operator tomonidan operator) qo'lda aylantiradigan bir nechta dasturchilarni o'z ichiga oladi.
Keyingi ma'ruza dasturlarning xususiyatlarini isbotlashga bag'ishlangan. Bu erda shuni ta'kidlash kerakki, bu usul hali ham juda kam qo'llaniladi.

15. 
    Ma'ruza uchun adabiyotlar 8.
    
16. 
    8.2. E. Deykstra. Strukturaviy dasturlash bo'yicha eslatmalar // W. Dahl, E. Dijkstra, K. Hoore. Strukturaviy dasturlash. - M .: Mir, 1975 .-- S. 24-97.
    

8.3. N. Virt. Tizimli dasturlash. - M .: Mir, 1977 .-- S. 94-164.

17. 
    Ma’ruza 9. Dastur xossalarini isbotlash
    
18. 
    Dasturni asoslash tushunchasi. Dastur xossalarini rasmiylashtirish, Xur triadasi. Belgilash operatori, shartli va qo'shma operatorlarning xususiyatlarini o'rnatish qoidalari. sikl operatorining xossalarini o'rnatish qoidalari, sikl o'zgarmasligi tushunchasi. Dasturning bajarilishining to'liqligi.
    
19. 
    9.1. Dasturlarni asoslash. Dastur xususiyatlarini rasmiylashtirish.
    
20. 
    Dasturiy ta'minotning ishonchliligini oshirish uchun dasturlarni etkazib berish juda foydali Qo'shimcha ma'lumot, undan foydalanish bilan siz PSni boshqarish darajasini sezilarli darajada oshirishingiz mumkin. Bunday ma'lumotlar dasturlarning turli qismlari bilan bog'langan norasmiy yoki rasmiylashtirilgan bayonotlar shaklida ko'rsatilishi mumkin. Biz bunday bayonotlarni dasturning mantiqiy asosi deb ataymiz. Dasturlarning norasmiy asoslari, masalan, muayyan qarorlar qabul qilish sabablarini tushuntirishi mumkin, bu xatolarni qidirish va tuzatishni, shuningdek, dasturlarni saqlashda o'rganishni sezilarli darajada osonlashtiradi. Rasmiylashtirilgan asoslar dasturlarning ba'zi xususiyatlarini qo'lda isbotlash va ularni avtomatik ravishda boshqarish (o'rnatish) imkonini beradi.
    

Hozirda dasturlarni rasmiy asoslashda foydalanilayotgan tushunchalardan biri bu Hoor triadalaridan foydalanishdir. S IS, P va Q axborot muhiti bo'yicha qandaydir umumlashtirilgan operator bo'lsin - bu muhit bo'yicha ba'zi predikatlar (bayonotlar). Keyin (P) S (Q) yozuvi Hoor triadasi deb ataladi, bunda P predikati oldindan shart, Q predikati esa S operatoriga nisbatan keyingi shart deb ataladi. Operator (xususan, dastur) S. (P) S (Q) xossaga ega bo‘lganligi aytilgan bo‘lsa, agar S operatori bajarilgunga qadar har doim P predikati rost bo‘lsa, bu S operator bajarilgandan keyin Q predikati rost bo‘ladi.
Dastur xususiyatlariga oddiy misollar:
(9.1) (n = 0) n: = n + 1 (n = 1),
(9.2) (n
(9.3) (n<3*(m+k)},<="" p="">
(9.4) (n> 0) p: = 1; m: = 1;
WHILE m / = n QILADI

21. 
    Xayr
    

S dasturining xossasini isbotlash uchun dasturlash tilining oddiy operatorlarining xossalari (bu yerda biz faqat bo‘sh operator va tayinlash operatori bilan cheklanamiz) va boshqaruv tuzilmalari (kompozitsiyalari) xossalaridan foydalaniladi, ular yordamida dastur oddiy operatorlardan qurilgan (biz bu erda tuzilgan dasturlashning uchta asosiy tarkibi bilan cheklanamiz, sakkizinchi ma'ruzaga qarang). Ushbu xususiyatlar odatda dasturni tekshirish qoidalari deb ataladi.

22.