VCGen билан дастурий маҳсулотларни текшириш
Ushbu laboratoriya ishi dasturiy ta'minotni tekshirishga bag'ishlangan bo'lib, xususan, Java dasturlash tilida yozilgan kodlarni OpenJML yordamida tekshirishga qaratilgan. Ishda VCGen (Verification Condition Generation) texnikasi, uning ishlash prinsipi va kodlarni tekshirishdagi roli tushuntiriladi. Shuningdek, C dasturlash tilida VCC vositasidan foydalanish va JML (Java Modeling Language) yordamida kodlarni izohlash orqali tekshirish usullari ham ko'rsatib berilgan. Misollar orqali bu texnikalarning amalda qanday qo'llanilishi va natijalari ko'rsatilgan.
Asosiy mavzular
- VCGen bilan dasturiy mahsulotlarni tekshirish: Ushbu mavzu dasturiy ta'minotni tekshirishning asosiy usullaridan biri bo'lgan VCGen (Verification Condition Generation) haqida ma'lumot beradi. Uning qanday ishlashi, dasturiy kodlarning xususiyatlarini aniqlashda tutgan o'rni va uni amalga oshirish jarayoni misollar bilan tushuntirilgan.
- JML (Java Modeling Language) orqali kodlarni tekshirish: Bu mavzu Java dasturlash tilida yozilgan kodlarni JML (Java Modeling Language) yordamida qanday tekshirish mumkinligini ko'rsatadi. JML ning asosiy kalit so'zlari (requires, ensures, invariant, loop_invariant va boshqalar) va ularning kodda qanday qo'llanilishi tushuntiriladi.
- VCC (Verifying C Compiler) orqali C kodlarini tekshirish: Ushbu mavzu C dasturlash tilida yozilgan kodlarni VCC (Verifying C Compiler) vositasi yordamida tekshirishga bag'ishlangan. VCC ning qanday ishlashi va uni dasturiy ta'minotni tekshirishda qo'llash bo'yicha misollar keltirilgan.
- Haore uchligi: Dasturiy ta'minotni tekshirishda keng qo'llaniladigan Haore uchligi {P} S {Q} konsepsiyasi, ya'ni dastlabki shart (P), bajariladigan operatsiya (S) va yakuniy shart (Q) tushuntiriladi va unga misollar keltiriladi.