Quyidagi kod ikkita tasdiqni o'z ichiga oladi, x> 0 va x> 1va ular haqiqatan ham ijro paytida ko'rsatilgan nuqtalarda to'g'ri keladi

Dasturiy kodlarni tekshiruvchi kompilyator dasturini yaratish.
Tafsilotlar


Quyidagi kod ikkita tasdiqni o'z ichiga oladi, x> 0 va x> 1va ular haqiqatan ham ijro paytida ko'rsatilgan nuqtalarda to'g'ri keladi:
x = 1;tasdiqlash x > 0;x++;tasdiqlash x > 1;
Dasturchilar dasturlarni belgilashga yordam berish va dasturning to'g'riligi to'g'risida mulohaza yuritish uchun tasdiqlardan foydalanishlari mumkin. Masalan, a old shart- kod qismining boshiga qo'yilgan tasdiq - dasturchi kod bajarilishini kutadigan holatlar to'plamini belgilaydi. A keyingi shart- oxirida joylashtirilgan - ijro oxirida kutilgan holatni tavsiflaydi. Masalan: x> 0 {x ++} x> 1.
Yuqoridagi misolda foydalanilgan tasdiqlarni kiritish uchun yozuv ishlatilgan C. A. R. Hoare uning 1969 yilgi maqolasida.^[1] Ushbu yozuvni mavjud bo'lgan asosiy dasturlash tillarida ishlatib bo'lmaydi. Biroq, dasturchilar tomonidan tekshirilmagan tasdiqlarni o'z ichiga olishi mumkin sharh xususiyati ularning dasturlash tilining. Masalan, ichida C:
x = 5;x = x + 1;// {x> 1}
Izohga kiritilgan qavslar sharhning ushbu ishlatilishini boshqa foydalanishlardan ajratib olishga yordam beradi.
Kutubxonalar tasdiqlash xususiyatlarini ham taqdim etishi mumkin. Masalan, C-da C99-ni qo'llab-quvvatlaydigan glibc-dan foydalaning:
# shu jumladan int f(bekor){ int x = 5; x = x + 1; tasdiqlash(x > 1);}
Bir nechta zamonaviy dasturlash tillari tekshirilgan tasdiqlarni o'z ichiga oladi - bayonotlar tekshiriladi ish vaqti yoki ba'zan statik ravishda. Agar tasdiqlash ish vaqtida noto'g'ri deb baholansa, tasdiqlash muvaffaqiyatsiz bo'ladi, bu odatda bajarilish bekor qilinadi. Bu mantiqiy nomuvofiqlik aniqlangan joyga e'tiborni qaratadi va aks holda olib keladigan xatti-harakatlardan afzal bo'lishi mumkin.
Tasdiqlardan foydalanish dasturchini dasturni ishlab chiqishda, ishlab chiqishda va u haqida fikr yuritishga yordam beradi.
Foydalanish
 
Kabi tillarda Eyfel, tasdiqlar dizayn jarayonining bir qismini tashkil qiladi; kabi boshqa tillar C va Java, ulardan faqat taxmin paytida ish vaqtidagi taxminlarni tekshirish uchun foydalaning. Ikkala holatda ham, ular ish paytida haqiqiyligini tekshirishlari mumkin, lekin odatda ularni bostirish mumkin.