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

Predikatlarni hisoblash
Quyida olingan bir nechta asosiy ta'riflar keltirilgan nazariyalari predikatlarni hisoblash. Ushbu ish bilan yanada shaffof aloqa qilish uchun, ta'riflar biroz soddalashtirildi. Ushbu material batafsilroq va to'liqroq tasvirlangan [12].
Xulosa qoidasi shaklning rasmiy yozuvi deb ataladi: (Φ0, Φ1, …, Φn) /Γ
bu erda Φi va Γ formulalar, Φi esa posilkalar, Γ esa xulosa.
Keling, induktiv ravishda formulalar daraxti tushunchasini aniqlaymiz:
1) har qanday formula daraxtdir.
2) Agar D0, D1,..., Dn daraxtlari va s formulasi bo'lsa, unda.
(D0, D1, …, Dn)/S
- shuningdek, daraxt. S formulasi daraxtning ildizidir.
D formula daraxti, agar uning o'tishlari bo'lsa, C formulasini chiqarish daraxti deb ataladi xulosa qoidalarini qo'llash va b ning ildizi C.
Daraxt barglari bo'lgan formulalarning haqiqati va qoidalarning haqiqati quyidagilarga olib keladi ildiz formulasining haqiqati C.
Operator mantig'i
P tilidagi dastur predikatlarning ta'riflari to'plamidir. Predikatning ta'rifi:
A(x: y) pre P(x) { S(x: y); } post Q(x, y),
bu erda A-aniqlanadigan predikatning nomi, s-operator va x va y-bir-biriga mos kelmaydigan o'zgaruvchilar to'plamlari, argumentlar va natijalar mos ravishda. A(x: y) predikatining spetsifikatsiyasi ikkita mantiqiy formula bilan berilgan: amalga oshirilayotgan funktsiyani aniqlash doirasini cheklaydigan p(x) old shart dastur va argumentlar va natijalarning qiymatlarini bog'laydigan Q(x, y) postkonditsiyasi. S(x: y) operatorining mantig'i l(s(x: y)) ga bog'liq bo'lgan mantiqiy bayonotdir operator o'zgaruvchilarining qiymatlari. Operatorning mantig'i uning aniq ekvivalenti [6].
Keling, asosiy operatorlar uchun mantiqlarni aniqlaymiz. E ifodasi, x ga bog'liq, o'zgaruvchini o'z ichiga olmaydi a, tayinlash operatorining mantig'i a: = E:
L(a := E(x))  R(x) & a = E(x)
bu erda R (x) eng zaif predikat bo'lib, uning haqiqatida e ifodasi aniqlanadi. Masalan, L (c: \ u003d a / b) \ u003d b 0 & c \ u003d a / b ga teng.
Keling, ketma-ketlikni aniqlaydigan b; C operatorining l(B; C) mantig'ini tuzamiz b va C operatorlarini l(B) va L(C) mantiqlari orqali bajarish. Ma'lum bo'lishicha, bu zarur
operatorni hisoblash bilan bog'liq bo'lmagan holatni alohida ko'rib chiqing. Uchun operatorlar orasidagi bog'lanishlarning fiksatsiyasi o'zboshimchalik bilan a operatori quyidagicha tasvirlanadi A (x: y), bu erda x va y o'zgaruvchilar to'plamlari operatorning argumentlari va natijalarini bildiradi, shunga ko'ra.
B; C operatori o'rniga biz superpozitsiya operatorini ko'rib chiqamiz B(x: z); C(z: y) va parallel operator b(x: y) || C (x: z). Uchinchisi ko'rib chiqiladi shartli bayonot if(E) B(x: y) else C (x: y), bu erda mantiqiy ifoda e bog'liq bo'lishi mumkin x dan.x, y va z to'plamlari kesishmaydi va x to'plami bo'sh bo'lishi mumkin deb taxmin qilinadi. Ushbu operatorlarning mantiqlarini aniqlang:
L(B(x: z); C(z: y))  z L(B(x: z)) & L(C(z: y))
L(B(x: y) || C(x: z))  L(B(x: y)) & L(C(x: z))
L(if (E) B(x: y) else C(x: y))  (E  L(B(x: y))) & (E  L(C(x: y)))
Dastur mantig'i rasmiy operatsion tizimga mos kelishi kerak ixtiyoriy b(x: y) operatori va sobit qiymatlar uchun P. tilining semantikasi o'zgaruvchan to'plamlar x va y uning mantig'i D(B (x: y)) to'g'ri va faqat qachon x qiymatlari to'plamidagi b(x: y) operatorining har qanday bajarilishi tugallanadi va ijro natijalari y to'plamining qiymatlari hisoblanadi. b(x: y) operatorining tugashi formula y l(b(x: y)).