Toshkent axborot texnologiyalar universiteti 010-19 guruh statik tahlil amaliy ish karimov mirsirojiddin

3.
Ramziy ijro - bu dasturni mavhum tarzda bajarish usuli bo'lib, bitta mavhum bajarilish orqali 
ma'lum bir bajarish yo'lini baham ko'radigan dasturning bir nechta mumkin bo'lgan kirishlarini 
qamrab oladigan kod. Amalga oshirish ushbu kiritishlarni ramziy ma'noda ko'rib chiqadi va 
atamalar bilan ifodalangan natijani "qaytaradi" ushbu kirish qiymatlarini ifodalovchi ramziy 
konstantalarorqali Ramziy ijro mavhum talqinga qaraganda kamroq umumiydir, chunki u 
hamma narsani o'rganmaydi Biroq, ramziy ijro ko'pincha yaqinlashishdan qochishi mumkin 
Tahlil tugatilishini ta'minlash uchun AI taxminan bo'lishi kerak bo'lgan joylar. Bu shuni 
anglatadiki, ramziy ijro yolg'on ogohlantirishlardan qochishi mumkin; ramziy bajarish orqali 
topilgan har qanday xato ifodalaydi dastur orqali haqiqiy, amalga oshirilishi mumkin bo'lgan yo'l 
va (biz yaxshi ko'rib turganimizdek) sinov ishi bilan guvoh bo'lishi mumkin bu xatoni ko'rsatadi.
Ramziy ijro dastlab 1970-yillarda taklif qilingan, ammo u avtomatlashtirilgan teoremaga 
tayangan.isbotlash va o'sha davrning algoritmlari va texnik vositalari keng foydalanishga tayyor 
emas edi. SAT/SMTbilan yechish boʻyicha soʻnggi yutuqlar va 40 yillik Mur qonuni apparat 
vositalariga tatbiq etilgan boʻlsa, ramziy ijro endi boshqa koʻplab vaziyatlarda amaliy boʻlib, 
dasturda keng qoʻllaniladi.WHILE da biz dasturlarni ramziy ravishda baholash qoidalarini 
yozishimiz mumkin. Qoidalarni a ga yozamiz Biz ilgari yozgan katta bosqichli semantikaga 
o'xshash uslub, lekin ramziy qadriyatlarni o'z ichiga oladi va saqlaydi yo'l sharoitlarini kuzatib biz 
arifmetik ifodalar va mantiqiy predikatlar uchun ramziy analoglarni aniqlashdan boshlaymiz. 
Bizramziy predikatlarni qo'riqchi deb ataydi va g meta o'zgaruvchisidan foydalanadi, chunki ular 
qo'riqchiga aylanadi.ramziy baholovchi o'rganadigan yo'llar. Ushbu analoglar oddiy versiyalar 
bilan bir xil, bundan mustasno o'zgaruvchilar o'rniga ramziy konstantadan foydalanamiz