|
Dasturni tekshirishning formal usullari
|
| bet | 1/3 | | Sana | 14.04.2024 | | Hajmi | 32.46 Kb. | | #194793 |
Bog'liq Olmos Shomirzayev 106b2e99-fa4b-4425-8da1-850c24872d36, Tijorat banklari, Neft hám gazdi jńynaw Ulıq, Muhammad ibn Muso al Xorazmiy,Nasriddin Tusiy, Jamshid G‘iyosiddin al Koshiy Ulug‘bek asarlarida arifmetikaning rivojlanishi haqida ma’lumotlar., Texnika xavfsizlik qoidalari, тех харита, 1-dekabr
MUHAMMAD AL-XORAZMIY NOMIDAGI TOSHKENT AXBOROT TEXNOLOGIYALARI UNIVERSITETI
SAMARQAND FILIALI
Kompyuter injiniringi fakulteti
107-guruh
Dasturni tekshirishning formal usullari
Mavzu: Dasturni deduktiv tahlil etish
Bajardi: Shomirzayev Olmos
Qabul qildi: MAVLONOV O. N.
Dasturni deduktiv tahlil etish
Reja:
1.Kirish:
Dastur haqida umumiy ma'lumot berish.
2. Deduktiv tahlilning asosiy konseptsiyasi:
Deduktiv tahlilning ma'nosi, asosiy xususiyatlari va qanday ishlaydi.
Ob'ektni aylanib o'tib, bir nechta buruq (slice) ko'rsatish.
3. Deduktiv tahlilning metodologiyasi:
Boshqa analitik metodlar bilan taqqoslash, nima uchun deduktiv tahlil foydalaniladi?
4. Deduktiv tahlilning muhimligi:
Nega deduktiv tahlil ahamiyatli?
5. Deduktiv tahlilning eng mashhur metodlari:
Ko'p ishlatiladigan deduktiv tahlil metodlari va ularning tushunchalari.
6. Deduktiv tahlilning afzalliklari va chegaralari:
Bu usulning yaxshi va yomon tomonlari.
7.Xulosa qismi:
Dastur haqida umumiy ma'lumot berish.
Kompyuter dasturlari zamonaviy jamiyatda asosiy rol o'ynaydi. Dasturiy ta'minot tizimlarining ishonchliligi iqtisodiy jihatdan muhim va bu avtomobil, aviatsiya yoki tibbiy dasturlar kabi xavfsizlik uchun muhim tizimlar uchun juda muhimdir. Shu bilan birga, dasturiy ta'minotdagi kamchiliklar ("xatolar") hali ham hisobga olinadi. deyarli muqarrar bo'lish; Xavfsizlik nuqtai nazaridan juda muhim bo'lgan barcha sohalarda, odatda, jo'natilgan dasturiy mahsulotlarda xatoliklar borligi qabul qilinadi. Bu elektrotexnika yoki mashinasozlik kabi kompyuter fanidan eskiroq va etukroq bo'lgan va noto'g'ri mahsulotlar istisno sifatida ko'rilgan fanlardan farq qiladi. normadan ko'ra. Ushbu dissertatsiya dasturiy ta'minot tizimlarining sifatini zararli usullar, ya'ni tavsiflash, loyihalash, ishlab chiqish va tahlil qilish usullari orqali yaxshilash haqida. matematik qat'iylik bilan dasturiy ta'minot tizimlari. Rasmiy usullar dasturiy ta'minot ishonchliligining barcha muammolarini sehrli tarzda hal qiladigan "kumush o'q" bo'lmasa-da, ular kelajakda an'anaviy dasturiy ta'minot muhandislik texnikasini to'ldiradigan va ba'zi hollarda o'rnini bosadigan doimiy ahamiyat kasb etishini kutish mumkin. Aniqrog'i, bu tezis manba kodida dasturiy ta'minotni tekshirish haqida daraja: maqsad - real dunyo dasturlash tilida yozilgan dasturiy ta'minot qismlarining to'g'riligini qat'iy ta'minlash. Aksincha, manba kodidan ko'ra mavhum dizaynga ko'proq yo'naltirilgan rasmiy usullarga misollar Z [Spivey, 1992], B va Event-B [Abrial, 1996; Hallerstede, 2009], Qotishma [Jekson, 2002] va Abstract State Machines [B¨orger and St¨ark, 2003]. To'g'rilik tushunchasining ma'nosi individual dastur uchun rasmiy tilda dasturning mo'ljallangan xatti-harakatini tavsiflovchi rasmiy spetsifikatsiya bilan belgilanadi. Tavsif butun funktsional xatti-harakatni qamrab olishi mumkin yoki u faqat ma'lum xususiyatlar bilan bog'liq bo'lishi mumkin. Keng qo'llaniladigan juda o'ziga xos rasmiy spetsifikatsiyalarning xilma-xilligi - garchi har doim ham shunday deb hisoblanmasa ham - asosiy dasturlash tillarining turlari: o'zgaruvchining turi ish vaqtida o'zgaruvchida saqlanishi kerak bo'lgan mo'ljallangan qiymatlarni cheklaydi. Pirs [2002] ta'kidlaganidek, "tipli tizimlar eng mashhur va eng yaxshi tasdiqlangan engil vaznli rasmiy usullardir".
Bir oz engilroq, ammo ayni paytda keng tarqalgan rasmiy spetsifikatsiya turi bu tasdiqlar, ya'ni dasturlash tilidagi mantiqiy ifodalar (yoki yanada ifodali tilda formulalar) bo'lib, ular dastur bajarilishi kodning ma'lum bir nuqtasiga yetganda har doim qoniqtirilishi kerak. . Formulalarni dastur nuqtalariga biriktirish g'oyasi birinchi marta Floyd tomonidan kiritilgan [1967]. Tasdiqlashlar odatdagi turdagi tizimlarga qaraganda murakkabroq xususiyatlarni ifodalashga imkon beradi. Ularning mashhurligiga misol sifatida, Hoare [2003a] o'sha paytda Microsoft Office kodida chorak millionga yaqin tasdiqlar mavjudligini taxmin qildi. Shartnoma asosida loyihalash standart dasturlash tillarini tasdiqlash mexanizmining kengaytmasidir. Bu yerda ob'ektga yo'naltirilgan dasturning protseduralari oldindan va keyingi shartlar orqali, sinflari esa variantlarda ob'ekt orqali ko'rsatiladi. Hoare [1969, 1972] kabi oldingi ishlarga asoslanib, "shartnoma bo'yicha dizayn" atamasi Meyer [1992, 2000] tomonidan Eif fel dasturlash tilini loyihalashda kiritilgan bo'lib, u dizayn tomonidan o'rnatilgan yordamga ega. - shartnoma shartlari. Protsedura va sinf spetsifikatsiyalari mijoz va protsedura yoki sinfni amalga oshiruvchi o'rtasidagi shartnomalar sifatida ko'rib chiqiladi, o'zaro mas'uliyatni belgilaydi va dasturni modullashtirishga yordam beradi. Spetsifikatsiya bo'yicha dasturiy ta'minotni tekshirish usullarini statik va dinamik usullarga bo'lish mumkin. Statik usullar manba kodida uni amalda bajarmasdan ishlaydi; Misol sifatida kompilyator tomonidan amalga oshiriladigan turdagi tekshiruvni keltirish mumkin. Bundan farqli o'laroq, dinamik usullar aniq kirish qiymatlari uchun dasturni bajarishga, ya'ni dasturni sinab ko'rishga asoslangan. Sinov (engil) rasmiy usul bo'lishi mumkin yoki hisoblanmasligi mumkin. Bu bugungi kunda dasturiy ta'minotning ishonchliligini o'rnatishning asosiy vositasi bo'lib, sanoat bunga ko'p kuch sarflashga odatlangan. Garchi test kelajakda ham muhim bo'lib qolsa ham, uning ta'sir doirasi qoniqarli emas: eng ahamiyatsiz dasturiy ta'minot tizimlaridan tashqari hamma uchun davlat maydoni shunchalik kattaki, to'liq sinovdan o'tkazish mutlaqo mumkin emas.
Shunday qilib, Dijkstra [1972] mashhur ta'kidlaganidek, "dastur sinovi xatolar mavjudligini ko'rsatish uchun ishlatilishi mumkin, lekin hech qachon ularning yo'qligini ko'rsatmaydi".
Tasdiqlashlar va shartnoma bo'yicha dizayn spetsifikatsiyalari bugungi kunda odatda dinamik ish vaqtini tekshirish uchun qo'llaniladi, ular test sinovi muvaffaqiyatli yoki yo'qligini ko'rsatadigan sinov oraclesi bo'lib xizmat qilishi mumkin. Bu tezis o'rniga bunday spetsifikatsiyalarni statik ravishda tekshirish haqida. Aniqrog'i, bu to'liq huquqli, og'ir vaznli statik tekshirish bilan bog'liq bo'lib, bu erda maqsad xatolar yo'qligini ko'rsatishdir. dasturda. Statik tekshirish usullari (oddiy turdagi tekshirishdan tashqari) engilroq lazzatlarda ham foydali bo'lishi mumkin, bunda maqsad keng qamrovli sinovdan ko'ra xatolarni ertaroq va arzonroq topishdir. Og'ir vaznli statik tekshiruv - hal qilib bo'lmaydigan muammo. Bu muammoning qanchalik qiyinligini ko'rsatishi mumkin, ammo bu amaliy ahamiyatga ega bo'lgan holatlarni hal qilish mumkin emas degani emas. Hoare tomonidan kompyuter fanlari bo'yicha tadqiqotlar uchun "katta muammo" sifatida ilgari surilgan statik tekshirish sohasidagi tasavvur [2003b,c], 21.2. KEY - bu tasdiqlarning to'g'riligini tekshiradigan "tekshirish kompilyatori" ni ishlab chiqishdir kabi, kompilyatorlar bugungi kunda turdagi tekshiruvni amalga oshiradilar. statik tekshirish shakli deduktiv tekshirishdir. Hoare [1969] tomonidan ishlab chiqilgan deduktiv tekshirish, shubhasiz, eng rasmiy tekshirish usuli hisoblanadi: dastur uning to'g'riligining mantiqiy isbotini yaratish orqali tekshiriladi. Statik dasturiy ta'minotni tekshirishning yana ikkita keng yondashuvi, bu erda mantiq rol o'ynashi yoki o'ynashi mumkin emas, lekin odatda rasmiy dalillar yo'q. yaratilgan, mavhum talqin [Cousot and Cousot, 1977] va ramziy dasturiy modelni tekshirish [Henzinger va boshq., 2003; Clarke va boshqalar, 2004; Ball va boshqalar, 2006]. Mavhum talqin avtomatlashtirishga erishish uchun yaqinlashish rolini ta'kidlaydi. Bu tezisda ham rol o'ynaydi, garchi asosiy e'tibor deduktiv tekshirishga qaratilgan bo'lsa. Dasturiy ta'minot modelini tekshirish g'oyasi cheklangan holat tizimlarining xossalari aniq holatni o'rganish orqali tekshiriladigan klassik model tekshiruvidan kelib chiqdi. Manba kodini tekshirish uchun ramziy dasturiy model tekshiruvi mavhum talqindagi kabi avtomatik abstraktsiya usullaridan foydalanishi mumkin. Deduktiv tekshirish, mavhum talqin qilish va dasturiy ta'minot modelini ramziy tekshirish o'rtasidagi chegaralar keskin emas, farqlash sabablari:
ma'lum darajada tarixiy. Shuni ta'kidlash kerakki, hatto deduktiv tekshirish, dasturda xatolik yo'qligini ishonchli isbotlashga qaratilgan bo'lsa ham, dastur mo'ljallangan tarzda ishlashiga mutlaq ishonch hosil qilish emas. Mutlaq ishonchga erishish mumkin emas, masalan, dasturning rasmiy spetsifikatsiyasi va insonning dastur aslida nima qilishi kerak bo'lgan niyati o'rtasida har doim bo'shliq mavjud. Deduktiv tekshirishning maqsadi - bu dasturiy ta'minotning to'g'riligiga bo'lgan ishonchni keskin, ammo baribir asta-sekin oshirish. Natijada, Beckert va Klebanov [2006] tomonidan batafsilroq ta'kidlanganidek, tekshirish tizimining o'zi uchun qandaydir tarzda qat'iy tekshirilishi foydalidir, lekin zarur emas; uning ishlashiga ishonchni boshqa vositalar bilan ham qozonish mumkin, masalan, paradoksal ko'rinishda, sinov orqali.
KEY
Ushbu tezis asosidagi tadqiqot KeyY loyihasining bir qismi sifatida amalga oshirildi [Beckert va boshq., 2007]. KeyY loyihasi 1998-yilda Karlsrue universitetida boshlangan va bugungi kunda Karlsrue texnologiya instituti, Goteborgdagi Chalmers texnologiya universiteti va Koblenz universiteti o‘rtasidagi hamkorlikdagi sa’y-harakatlardir. Uning asosiy mavzusi - ob'ektga yo'naltirilgan dasturiy ta'minotni deduktiv tekshirish. KeyY loyihasining asosiy dasturiy mahsuli Java tilida yozilgan dasturlarning toʻgʻriligini isbotlovchi tekshirish vositasi boʻlgan Key tizimidir.
[Gosling va boshq., 2000]. Aniqrog‘i, KeyY to‘liq Java Card tilini qo‘llab-quvvatlaydi
|
| |
