Bajardi : Ki103-19-gurux Ziyotov Sherjon Tekshirdi : Mahudov R. Z. Samarqand -2023 Mavzu

O`ZBEKISTON RESPUBLIKASI AXBOROT TEXNOLOGIYALARI VA KOMMUNIKATSIYALARINI RIVOJLANTIRISH VAZIRLIGI
MUHAMMAD AL-XORAZMIY NOMIDAGI
TOSHKENT AXBOROT TEXNOLOGIYALARI
UNIVERSITETI SAMARQAND FILIALI

"Kompyuter injiniring" fakulteti

"Dasturni formal tekshirishning formal usullari” fanidan

1-Labaratoriya ishi

Mavzu: Ketma-ket dasturlarni deduktiv tekshirish.

Bajardi :Ki103-19-gurux
Ziyotov Sherjon
Tekshirdi : Mahudov R.Z.
Samarqand -2023
Mavzu: Ketma-ket dasturlarni deduktiv tekshirish.
Reja:

1. 
   Predikatlarni hisoblash
   
2. 
   Operator mantig'i
   
3. 
   Dasturning to'g'riligi
   
4. 
   Rekursiv ravishda aniqlangan predikatning to'g'riligi.
   
5. 
   To'g'rilik shartlarini chiqarish qoidalari tizimi.
   
6. 
   To'g'rilik shartlarini yaratish algoritmi
   
7. 
   Xulosa.
   

Kirish
Sinov xatolarni topishning yagona usuli emas. Kompleks xatolarni aniqlash va dastur sifatini nazorat qilishning turli usullari sifatida belgilanadi dasturiy ta'minotni tekshirish. Tasdiqlash ko'pchilikni o'z ichiga oladi statik tahlil, ekspertiza va rasmiy usullar kabi usullar. Bittasi rasmiy usullar deduktiv tekshirish hisoblanadi. bilan sinovdan farqli o'laroq deduktiv tekshirish barcha xatolarni aniqlay oladi. Biroq, bu juda murakkab va mashaqqatli usul. Deduktiv tekshirishdan foydalanish faqat quyidagi hollarda oqlanadi xatolik yuqori bo'lgan ilovalar: aerokosmik sanoatda, energetikada, tibbiyotda va boshq.
Deduktiv tekshirish dasturning to'g'riligini tekshirishni amalga oshiradi rasmiy spetsifikatsiya tilida yozilgan spetsifikatsiyasiga nisbatan. Shartlar dasturning to'g'riligi avtomatik ravishda mantiqiy formulalar yordamida yaratiladi va mantiqiy qoidalar tizimini qo'llash orqali dasturning xususiyatlari. Shart dasturning to'g'riligi odatda a shaklida bo'ladi B, bu erda B-belgilangan bayonet dasturning spetsifikatsiyasi va dastur uchun to'g'ri bo'lgan a formulasi undan olinadi tilning rasmiy (operatsion, denotatsion, ...) semantikasidan foydalanish dasturlash. To'g'rilik shartlarini isbotlash quyidagilar yordamida amalga oshiriladi ba'zi avtomatik isbotlash tizimlari. Uning qo'llanilishi, aksincha "qo'lda" dalillar, nisbatan dasturning to'g'riligini kafolatlaydi xususiyatlari.
Ushbu ishda quyidagilar uchun to'g'rilik shartlarini avtomatik ravishda yaratish tasvirlangan predikat dasturlash tilidagi dasturlar p [3].
Predikat dasturlash tili p Medu chegarasida joylashgan funktsional va mantiqiy tillar. P tili dasturlar sinfini belgilaydi, emas tashqi muhit bilan o'zaro aloqada bo'lish. Ushbu dasturlar funktsiyalarni amalga oshiradi, kirish o'zgaruvchilarining qiymatlarini natijalar qiymatlariga ko'rsatish. Ijro dasturlar har doim yakunlanishi kerak, chunki cheksiz ijro etish befoyda. Ushbu sinf hech bo'lmaganda diskret va vazifalar uchun dasturlarni o'z ichiga oladi hisoblash matematikasi. Predikat dasturlarining spetsifikatsiyasi quyidagilar bilan amalga oshiriladi old shart va keyingi shartlardan foydalanish.