VCGen билан дастурий маҳсулотларни текшириш

Ushbu laboratoriya ishi dasturiy ta'minotni tekshirish uchun VCGen vositasidan foydalanishni o'rganishga bag'ishlangan. Unda dasturiy kodlarni JML (Java Modeling Language) orqali izohlash, tekshirish shartlarini generatsiyalash va tasdiqlash jarayonlari tushuntiriladi. Misollar orqali VCGen ning ishlash prinsipi, jumladan, 'requires', 'ensures', 'loop_invariant' kabi JML kalit so'zlari va ularning dasturiy kodni tekshirishdagi roli ko'rsatib berilgan. Shuningdek, C dasturlash tilida VCC vositasidan foydalanish ham qisqacha yoritilgan.

Asosiy mavzular

VCGen bilan dasturiy mahsulotlarni tekshirish: Dasturiy ta'minot tekshiruvchilari (program verification) dasturiy ta'minotni aniqlangan xususiyatlarga mos kelishini ta'minlash uchun ishlatiladi. VCGen (Verification condition generation) esa dastur xususiyatlarini (specifications) matbuot shartlariga aylantirish orqali dasturni tekshirishga yordam beradi. Ushbu jarayon dasturiy kodga JML izohlarini qo'shish, tekshirish shartlarini generatsiyalash va ularni avtomatlashtirilgan teorema isbotlagichlar yordamida tekshirishni o'z ichiga oladi.
JML (Java Modeling Language) xususiyatlari: JML Java dasturlash tilida dasturiy kodni tekshirish uchun ishlatiladigan izohlar tizimidir. U 'requires' (dastlabki shart), 'ensures' (natijaviy shart), 'loop_invariant' (tsikl invariant) kabi kalit so'zlar yordamida dasturiy kodning turli xususiyatlarini va shartlarini ifodalash imkonini beradi. Ushbu izohlar VCGen kabi vositalar tomonidan dasturni avtomatik tekshirish uchun ishlatiladi.
VCC (Verifying Compiler) va C dasturlash tilida tekshirish: VCC C dasturlash tilida dasturiy ta'minotni tekshirish uchun mo'ljallangan vositadir. U ham JML kabi dasturiy kodga maxsus izohlar qo'shish orqali ishlaydi. Laboratoriya ishida VCC ning ishlatilishi va uning C kodlarini tekshirishdagi rolini ko'rsatuvchi qisqa misol keltirilgan.