"Kompyuter injiniring" fakulteti "Kampyuter tizimlar" kafedrasi "Dastur tekshirish farmal usullari ” fanidan 1-labaratoriya Mavzu: Ketma-ket dasturlarni deduktiv tekshirish

Рисунок 1. Общая схема формальной верификации 
Formal usulning umumiy sxemasi 1-rasm: dasturning rasmiy modeli 
yaratilgan; talablarning rasmiy modeli yaratiladi; dastur modelining talablar 
modeliga muvofiqligi rasmiy ravishda tekshiriladi; tekshirish natijalariga ko'ra 
haqiqiy dasturning haqiqiy talablarga muvofiqligi yoki mos kelmasligi to'g'risida 
(boshqacha aytganda, dasturda xatolarning yo'qligi yoki mavjudligi to'g'risida) 
xulosa qilinadi. Dastur modellari va talablari modellarini namoyish qilish uchun mos 
ravishda dasturlarning rasmiy spetsifikatsiyasi tillari (modellashtirish tillari) va 
talablarning rasmiy spetsifikatsiyasi tillari qo'llaniladi; bunday tillarning namunalari 
qo'llanmada muhokama qilinadi. 
Formal usullari dastur modellari turlari (cheklangan avtomatlar, Petri 
tarmoqlari, belgilangan o'tish tizimlari), talablar modellari turlari (dasturiy ta'minot 
shartnomalari, ishlab chiqarish qoidalari, vaqtinchalik bayonotlar), yozishmalar 
munosabatlari (ekvivalentlik, simulyatsiya, izlarni kiritish) va muvofiqlik bilan 
farqlanadi. tekshirish texnikasi (kosmik holatlarni o'rganish, ramziy tahlil, deduktiv 
xulosa). 
Quyida biz rasmiy tekshirish usullarining ekvivalentni tekshirish, modelni 
tekshirish va deduktiv tahlil kabi turlarini batafsil ko'rib chiqamiz. 
Ekvivalentlikni tekshirish. Ekvivalentlikni tekshirishda dastur modeli va 
talablar modeli bir xil (masalan, har ikkala model ham cheklangan avtomat, yoki har 
ikkala model ham Turing mashinalari) va ko'rib chiqilayotgan turdagi modellar 
uchun belgilangan ekvivalentlik munosabatlaridan biri yozishma munosabati 
sifatida ishlatiladi. Bajariladigan modellarning (avtomatlar, dasturlar va boshqalar) 
ekvivalentligini tekshirishda talablar modeli mos yozuvlar modeli yoki mos 
yozuvlar dasturlari deb nomlanadi. 

---

Kirish va chiqish o'zgaruvchilari bir xil bo'lgan ikkita (deterministik) ketma-
ket dasturlar, agar ularning domenlari bir-biriga to'g'ri keladigan bo'lsa (funktsional) 
ekvivalent deb aytiladi (bitta dastur uchun tegishli bo'lgan har qanday kirish 
ma'lumoti boshqasiga tegishli bo'lsa) va har qanday tegishli kirish ma'lumotlari 
uchun ular bir xil qaytaradilar natijalar ... 
1.2-misol. Quyidagi 1.1-jadvalda ikkita Evklid1 va Evklid2 dasturlari 
keltirilgan, ularning har biri x va y ning ikkita kirish tamsayı o'zgaruvchilariga ega, 
x> 0 va y> 0 va bitta chiqish tamsayı o'zgaruvchisi GCD: 
Evklid algoritmining ikkita tatbiqi 
// Evklid1.cpp : 
#include

using
namespace
std; 
int
main() 
{ 
int
x =120; 
int
y = 18; 
cout 
<<
"x= "
<<
x 
<<
" y="
<<
y 
<<
endl; 
while
(x!= y) 
{ 
if
(x > y) x = x - y; 
else
y = y - 
x; 
} 
cout 
<<
"NOD="
<<
x 
<<
endl; 
return
0; 
} 
// Evklid2.cpp : 
#include

using
namespace
std; 
int
main() 
{ 
int
x = 120; 
int
y = 18; 
int
z; 
cout 
<<
"x= "
<<
x 
<<
" y="
<<
y 
<<
endl; 
while
(y != 0) 
{ 
z = x; 
x = y; 
y = z % y; 
} 
cout 
<<
"NOD="
<<
x 
<<
endl; 
return
0; 
} 
Evklid1 va Evklid2 dasturlarining ekvivalentligini ko'rish juda oson - ikkalasi 
ham ikkita tabiiy sonning eng katta umumiy bo'luvchisini (GCD) hisoblashadi (bu 
Evklid algoritmining turli xil dasturlari). Ularning ekvivalentligini qanday rasmiy 
ravishda isbotlash mumkin? 
Matematik jihatdan x = c * n, y = c * m va boshqalarni isbotlash mumkin 

---

Biroq, avtomatik tekshirish haqida gapiradigan bo'lsak, kompyuter qanday 
qilib dastur nima bilan shug'ullanishini, uning "ma'nosi" ni qanday qilib "tushunishi" 
kerakligi aniq emas. 
Siz boshqa yo'ldan borishingiz mumkin - taqqoslangan dasturlarning ma'nosini 
o'rganmasdan, ekvivalent o'zgarishlarni qo'llagan holda, boshqasiga (yoki har 
birining uchdan biriga) o'zgartirishga harakat qiling. 
 
Ketma-ket dasturlar, yani alg'oritmlar, deduktiv tekshirishni amalga oshirish 
uchun quyidagi usullardan foydalanish mumkin: 
Test qilish: Ketma-ket dasturni o'zgartirishsiz yoki kuchli testlar yordamida 
sinab ko'ring. Bu, dasturning asosiy funktsiyalarini va xususiyatlari tekshirilgan 
holda dasturda biron bir xatolik yoki nomutanosiblik borligini aniqlashga yordam 
beradi. 
Kode analiz qilish: Ketma-ket dasturda kodning barcha qismlarini tekshirib, 
ushbu kodda xatolik yoki nomutanosibliklarni aniqlash mumkin. Bu, xususiyati 
dastur kichik bo'lsa va biron bir test qilish mumkin bo'lmagan vaqt uchun foydali 
bo'ladi. 
Debug qilish: Debug oynasi yordamida ketma-ket dasturda sodir bo'lgan 
xatoliklarni topish va ularni tuzatish mumkin. Debug oynasida, dasturning har bir 
qadamini bajarishni to'xtatib, o'zini tekshirish va muammolarni aniqlash mumkin. 
Kodni tiklash: Ketma-ket dasturda kodni to'g'rilash yordamida kodda xatolik 
yoki nomutanosibliklarini aniqlab, ularni tuzatish mumkin. Buni qilish uchun 
dasturning qayta yozilishini talab qilish kerak bo'ladi. 
Formal verifikatsiya: Ketma-ket dasturda biron bir xatolik qolmaganini 
tasdiqlash uchun formal verifikatsiya yordamidan foydalanish mumkin. Bu usulda, 
dasturning ishlashini ko'rsatuvchi matematik modellari ishlatiladi. 
Bu usullar ketma-ket dasturlarni deduktiv tekshirish uchun foydalaniladigan 
eng mashhur usullardir. Ushbu usullarning har biri biror xil natijalarga erishishga 
yordam beradi. 
Deduktiv tekshirish, dasturlarning to'g'ri ishlashi uchun lozim bo'lgan shartlar 
va ehtimollar to'g'risida chora-tadbirlar amalga oshirish yordamida, dasturlarning 
xato yoki muammo qolmaganligini tasdiqlash usuli hisoblanadi. 
Deduktiv tekshirishning boshqa ma'nolari ham mavjud, shu jumladan, 
matematik 
modellarda 
yoki 
tizimlarda 
muhim 
natijalarga 
erishishda 
foydalaniladigan ma'lumotlar yoki aniq xususiyatlarga asoslangan tasdiqlash usuli. 
Bu usulda, dasturning to'g'ri ishlashi uchun kerakli bo'lgan barcha shartlar va 
ehtimollar aniqlanib, dastur yaratuvchisi tomonidan aniqlangan testlar yordamida, 
dastur to'g'ri ishlashi haqida aniqligi tasdiqlanadi. 

---

Deduktiv tekshirishning muhim asosiy qismi, lozim bo'lgan shartlar va 
ehtimollar aniqlash va to'g'ri ishlash uchun testlar yaratishdir. Bu testlar odatda katta 
sonli ma'lumotlar to'plamidan tashkil topgan holda, dasturning barcha 
funktsiyalarini tekshirish uchun yaratiladi. 
Deduktiv tekshirish, dasturlarning to'g'ri ishlashiga nisbatan yuzaga keladigan 
har qanday muammolarni aniqlashga yordam beradi va dasturni yaxshilash uchun 
zarur bo'lgan o'zgarishlarni belgilashga imkon beradi. 
Deduktiv tekshirishda bir necha sinflarga bo'linadi, masalan, funksiyalar, 
klaslar, sinfdagi obyektlar va h.k. Shu sababli, quyidagi C++ kodida deduktiv 
tekshirishni ko'rsatishning yalpi darajasini ko'rsataman: 
#include  
using namespace std; 
bool isEqual(int a, int b) { 
if (a == b) { 
return true; 
} else { 
return false; 
} 
} 
int main() { 
int x = 3; 
int y = 4; 
bool result; 
result = isEqual(x, y); 
if (result == true) { 
cout << "x va y o'zaro teng." << endl; 
} else { 
cout << "x va y o'zaro teng emas." << endl; 
} 
return 0; 
} 
Deduktiv tekshirishda bir necha sinflarga bo'linadi, masalan, funksiyalar, 

---

klaslar, sinfdagi obyektlar va h.k. Shu sababli, quyidagi C++ kodida deduktiv 
tekshirishni ko'rsatishning yalpi darajasini ko'rsataman: 
c 
Copy code 
#include  
using namespace std; 
bool isEqual(int a, int b) { 
if (a == b) { 
return true; 
} else { 
return false; 
} 
} 
int main() { 
int x = 3; 
int y = 4; 
bool result; 
result = isEqual(x, y); 
if (result == true) { 
cout << "x va y o'zaro teng." << endl; 
} else { 
cout << "x va y o'zaro teng emas." << endl; 
} 
return 0; 
} 
Bu kodda, isEqual nomli bir funktsiya yaratilgan. Bu funktsiya ikkita butun 
sonni qabul qilib, ularning qiymatlari bir-biriga teng ekanligini aniqlaydi. Agar 
ikkisi bir-biriga teng bo'lsa, true qiymati qaytariladi; aks holda false qiymati 
qaytariladi. 
Dasturda, x va y o'zgaruvchilariga mos qiymatlar ta'qdim etiladi. result 
o'zgaruvchisi isEqual funktsiyasini chaqiradi va isEqual funktsiyasidan qaytgan 
qiymatni saqlaydi. 
So'nggi qadamda, result o'zgaruvchisining qiymati tekshiriladi. Agar true 

---

qiymati qaytgan bo'lsa, x va y o'zaro teng ekanligini tasdiqlash uchun cout operatori 
yordamida ma'lumot konsolga chiqariladi. Aks holda, x va y o'zaro teng emasligini 
tasdiqlash uchun ma'lumot konsolga chiqariladi. 
Bu kod, deduktiv tekshirishning asosiy qismlarini ko'rsatadi, shu jumladan, 
funktsiyalar yaratish, amallar chaqirish va yordamchi o'zgaruvchilardan 
foydalanish.