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

To'g'rilik shartlarini chiqarish qoidalari tizimi.
Umumiy to'g'rilik formulasidan foydalanib, siz avtomatik ravishda qurishingiz mumkin dasturlash tili uchun S(x: y) operatorining to'g'riligi formulasi dastur mantig'i qurilgan. To'g'rilikning yakuniy formulasi uzoq va murakkab bo'ladi hatto qisqa dasturlar uchun ham; u s(x: y) dasturidan uzunroq bo'ladi. Ixtisoslashuv har xil turdagi operatorlar uchun umumiy to'g'rilik formulalari quyidagilarga imkon beradi dekompozitsiya qilish oddiy formulalar.
Ushbu bo'limda quyidagilar uchun to'g'rilik shartlarini chiqarish qoidalari tizimi aniqlanadi turli operatorlar. Biroq, ushbu qoidalarning dalillari chiqarib tashlanadi [5], [6] va [7] asarlari.
Predikat argumentlari sifatida quyida keltirilgan qoidalarda quyidagilar qo'llaniladi o'zgaruvchilar. Argument pozitsiyalarida foydalanish mumkinligini ko'rsatish qiyin emas ifodalarning old shartlari old shartlardan kelib chiqishi sharti bilan iboralar predikatlar.
Aytaylik, b(x: z) va C(z: y) operatorlari o'zlariga nisbatan to'g'ri xususiyatlari [PB, QB] va [PC, QC]. Keyin haqiqatlar quyidagi qoidalardir:
RP:Corr(t, a, B(x: y), PB(x), QB(x, y)); Cos(t, a, C(x: y), PC(x), QC(x, z));
P (x) r (x)*B (x) & P*C (x); QB(x, y) & QC(x, z)va q(x, y, z)
Corr(t, A, B(x: y) || C(x: z), P(x), Q (x, y, z))
RS:Corr(t, a, B(x: z), PB(x), QB(x, z)); Corr(t, a, C(z: y), kompyuter(z), QC(z, y));
P (x) r (p)*B(x) va z QB (x, z) va b (x) va b (x) va b (x) va b (x)*C (z)); P(x) & z qb(x, z) & QC(z, y) z q(x, y) Corr (t, A, B(x, z); C(z, y), P(x), Q (x, y))
RC:Corr(t, a, B(x: y), PB(x), QB(x, y)); Corr(t, A, C(x: y), PC(x), QC(x, y));
P (x) & E-X)*B (x); P(x)*C (x);
P(x) & E & QB(x, y) r(x, y); P(x) & r(x, y) r (x, y)r (x, y) r (x, y)
Corr (t, A, agar(E) B(x: y) boshqa C(x, y), P(x), Q (x, y))
To'g'rilik shartlarini yaratish algoritmi
Algoritmning vazifasi to'g'rilik shartlarini avtomatik ravishda chiqarishdir predikat dasturi. P tilida predikat dasturi to'plam bilan ifodalanadi predikat ta'riflari. Bunday dasturning to'g'riligi har birining to'g'riligidir muayyan predikat. Shuning uchun, vazifa to'g'ri shartlarni xulosa qilish uchun kamayadi predikat ta'riflari:
A (x: y) pre P(x) { S(x: y); } post Q(x, y)
Predikatning to'liq to'g'riligi formulasini isbotlash:
Corr (t, a, S(x:y), P (x), Q(x, y)) ,
xulosa daraxtini qurish orqali tasvirlangan xulosa qoidalaridan foydalangan holda amalga oshiriladi 2-bo'lim Hosil bo'lgan to'g'rilik shartlari bu daraxtning barglari. Barglar bo'lgan formulalarning haqiqati daraxt va qoidalarning haqiqati to'liq to'g'rilik formulasining haqiqati.
Formulaning turi qo'llanilishi kerak bo'lgan qoidani belgilaydi. Ichida xulosa qilish jarayonida ikki xil formulalar mavjud: bu to'liq to'g'rilik sharti operator
Corr (s (x: y), P (x), Q(x, y))
va mantiqiy formula
A1 & A2 & ... & Bir Va B
bu erda oddiy mantiqiy bayonotlar ham, mantiqlar ham Ai va B vazifasini bajarishi mumkin operatorlar l(S(x: y)).
Agar formula birinchi shaklga ega bo'lsa, unda tizim ham qo'llaniladi umumiy holat uchun qoidalar (Q) yoki to'g'ri holat uchun qoidalar tizimi (r) operatorlari ostida. Bundan tashqari, q qoidalari tizimi ustuvorroqdir, ya'ni. uni qo'llash birinchi navbatda amalga oshiriladi.
Agar formulalar ikkinchi shaklga ega bo'lsa, unda uning tarkibida yoki yo'qligini tekshirish kerak operatorlarning mantiqlari L(S (x: y)). Agar mavjud bo'lmasa, bu yakuniy formuladir (to'g'rilik shartlaridan biri) va u lemma shaklida tuziladi. Ammo agar unda bo'lsa mantiq mavjud, keyin ushbu bayonotning xulosasi quyidagicha davom ettirilishi kerak parchalanish qoidalari tizimlari L(S (x: y)) (F). Xulosa qilishning keyingi maqsadi istisno operatorning mantiqiy formulasidan.
To'g'rilik shartlarini yaratish algoritmining to'g'riligi to'g'rilikdir har bir qo'llaniladigan qoida va dastur shaklida chiqishni amalga oshirishning to'g'riligi C++. Xulosa qoidalarining haqiqati [5], [6] va [7] asarlarida isbotlangan. Kelajakda barcha dalillarni bitta hujjatda to'plash kerak. Dasturning to'g'riligi jeneratör sinov orqali amalga oshiriladi. Ayni paytda dasturning ishlashi ikki o'nlab testlarda sinovdan o'tkazildi.
Xulosa
Asarda to'liq to'g'riligini isbotlashga imkon beradigan yondashuv tasvirlangan predikat dasturlari. To'g'rilik shartlarini chiqarish qoidalari tizimi qurilgan. Ilgari ushbu tizimga kiritilgan qoidalar tarqoq holda mavjud bo'lib, turli xillarda tasvirlangan va ba'zan turli nomlar ostida ishlaydi. Ba'zi qoidalarni umumlashtirish kerak edi rekursiv holat.
Ushbu qoidalar tizimi asosida generator ishlab chiqildi va amalga oshirildi predikat dasturlash tizimidagi to'g'rilik formulalari. Jeneratör imkon beradi manba kodli dasturlar uchun to'g'ri shartlarni avtomatik ravishda shakllantirish P. tili generator doirasida keyinchalik soddalashtirish ham amalga oshirildi mantiqning eng oddiy qonunlaridan foydalangan holda olingan to'g'rilik shartlari va mantiqiy algebra. Jeneratör predikat dasturlash tizimining bir qismidir va avtomatik ravishda chaqirilishi mumkin.