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

Dasturning to'g'riligi
Aytaylik, dastur umuman a(x: y) ning asosiy predikatiga mos keladi s(x: y) operatori bo'lgan [P(x), Q(x, y)] spetsifikatsiyasi. Keyin, to'g'rilik dasturlar quyidagi shartlar bilan belgilanadi: birinchidan, P(x) old shart bo'lishi kerak s(x: y) operatori bajarilishidan oldin to'g'ri bo'lishi kerak, ikkinchidan, q(x, y) postkonditsiyasi bo'lishi kerak s(x: y) operatorining bajarilishidan keyin va uchinchidan, operatorning bajarilishidan keyin to'g'ri bo'ling S (x: y) har doim tugaydi. Ushbu to'g'rilik shartlari quyidagicha shakllantiriladi quyidagi bayonotlar [6]:
P(x) & L(S(x: y))  Q(x, y) P(x)  y L(S(x: y))
Birinchi bayonot qisman to'g'rilik sharti deb ataladi, ikkinchisi esa–dasturni tugatish sharti. Ularning birlashishi umumiy (yoki) shartni belgilaydi s(x: y) operatorining spetsifikatsiyaga nisbatan to'liq) to'g'riligi [P(x), Q(x, y)]:
Corr(s(x:y), P(x), Q(x, y)) i P(x) I [L(S(x:y)) I Q(x, y)] & I y L(S (x: y))
Keyinchalik, "to'g'rilik" atamasi umumiy ma'noda ishlatiladi to'g'rilik.
Rekursiv ravishda aniqlangan predikatning to'g'riligi.
Ba'zilar uchun quyidagi induksion dalil sxemasi qo'llaniladi o'zboshimchalik bilan tasdiqlash W (z): balandligi t balandligi x [(balandligi y balandligi x m(y) < M (t) balandligi (y)) balandligi (t)] balandligi y balandligi x (y).
O'lchov deb nomlangan m funktsiyasi x ni tabiiy sonlar to'plamiga aylantiradi standart tartib nisbati <. Aytaylik, rekursiv predikatning ta'rifi mavjud A:
A (x: y) pre P(x) { K(x: y); } post Q(x, y)
K(x: y) operatori ichida a predikatining rekursiv chaqiruvi mavjud. Induksiya sxemasiga muvofiq rekursiv predikatning to'g'riligi mumkin quyidagi formula bilan aniqlanishi kerak:
A(u:y), P(x), Q(x, y))) I Corr(K(x:y), P(x), Q(x, y)) i Corr(K(x:y), P(x), Q (x, y))
Induktiv taxminni bildiradigan formulani kiritamiz t argumentlar to'plami:
Induct(t, A) $$ u m(u) < m(t) $$ Corr(A(u :y), P(x), Q (x:y))
Shunday qilib, rekursiv predikatning to'g'riligi formula bilan aniqlanadi:
Corr(t, a, K(x: y), P(x), Q(x, y)) rr(k(x: y), P(x), Q(x, y)) rr(T, A)Rr (K (x: y), P (x), Q (x, y))
Floydning yondashuviga rioya qilgan holda, biz predikat chaqiruvidagi old shartlarni o'zgartirib, ularni qo'shamiz kabi monotonlikni tekshirish:
P*(x) или m (x) < m (t) & P (x)
Bu erda t predikatning rekursiv ta'rifining rasmiy parametrlari, x esa haqiqiydir rekursiv qo'ng'iroq parametrlari.
Natijada, rekursivning to'g'riligini isbotlashning indüksiyon sxemasi a predikatining ta'riflari qoida bilan ifodalanadi:
R0: Corr (t, A, K (x:y), P (x), Q(x, y))/
Corr(a, P(x), Q(x, y))
Keyin, operator ichida rekursiv qo'ng'iroq bo'lmasa, biz rozi bo'lamiz K kirish Corr(t, a, K(x:y), P(x), Q(x, y)) Corr(K(x:y), P(x), Q (x, y)) ga teng bo'ladi. В rekursiv bo'lmagan qo'ng'iroq holatida p*(x) yozuvi p(x) ga teng.