Invariant — tizim yoki algoritmning belgilangan bosqichlarida doimo rost bo‘lishi kerak bo‘lgan xususiyat. Masalan, bank hisobidagi mavjud balans ruxsat etilgan overdraft chegarasidan past tushmasligi, binary search’da qidirilayotgan qiymat ehtimoli qolgan interval ichida bo‘lishi invariantdir. Invariant konkret bitta natijadan ko‘ra tizim holatiga qo‘yilgan umumiy qoidadir.
Turlari
Class invariant obyekt public operatsiyadan oldin va keyin yaroqli holatda bo‘lishini belgilaydi. Loop invariant siklning har iteratsiyasi boshida yoki oxirida rost bo‘ladi va algoritm to‘g‘riligini isbotlashga yordam beradi. Database invariant unique constraint, foreign key yoki check constraint orqali saqlanishi mumkin.
| Invariant turi | Misol |
|---|---|
| Obyekt | start <= end |
| Collection | Barcha IDlar noyob |
| Loop | Qayta ishlangan prefix saralangan |
| Database | Order total manfiy emas |
| Distributed | Bitta term’da ko‘pi bilan bitta leader |
| Security | Ruxsatsiz principal maxfiy obyektni o‘qimaydi |
Invariantning amal qilish nuqtasi aniq. Obyekt method ichida vaqtincha yaroqsiz holatga o‘tishi mumkin, lekin tashqaridan kuzatiladigan transaction chegarasida qoida tiklanadi.
Precondition va postcondition
Precondition operatsiya boshlanishidan oldin caller ta’minlashi kerak bo‘lgan shart. Postcondition muvaffaqiyatli tugagandan keyingi kafolat. Invariant esa bir nechta operatsiya bo‘ylab saqlanadigan xususiyat.
Masalan, withdraw(amount) uchun amount > 0 precondition; qaytgan balans avvalgisidan amountga kamayishi postcondition; balans overdraft limitidan past bo‘lmasligi invariant bo‘lishi mumkin. Bu ajratish xatoni qaysi boundary buzganini ko‘rsatadi.
Kodda ifodalash
Type system ayrim invariantlarni compile time’da ifodalaydi: nullable va non-null type, enum yoki bounded wrapper. Constructor yaroqsiz obyekt yaratilishini taqiqlaydi. Runtime assertion ichki mantiq buzilishini tez aniqlaydi.
Foydalanuvchi inputini faqat debug assertion bilan tekshirish to‘g‘ri emas, chunki assertion o‘chirilishi mumkin. Validatsiya normal error qaytaradi; invariant buzilishi esa dastur defecti sifatida alohida signal beradi.
Database constraint bir nechta application instance o‘rtasida markaziy himoya beradi. Faqat application-level “avval tekshir, keyin yoz” concurrency race’iga uchrashi mumkin. Constraint va transaction invariantni atomic boundary’da saqlaydi.
Testlash
Example-based test ma’lum input va outputni tekshiradi. Property-based testing ko‘p generatsiyalangan inputda invariantni sinaydi. Stateful model-based test random commandlar ketma-ketligidan keyin balans, ownership yoki ordering qoidasini tekshiradi.
Invariant juda umumiy bo‘lsa xato holatni ham o‘tkazadi. “Natija null emas” sort algoritmi uchun yetarli emas; natija saralangan va kirishdagi elementlar multisetini aynan saqlashi kerak. Bir nechta mustaqil property birgalikda kuchli oracle hosil qiladi.
Concurrency
Invariant har bir individual thread ichida saqlansa ham interleaving uni buzishi mumkin. Ikki transaction bir xil seat bo‘shligini o‘qib, ikkalasi ham band qilishi double booking keltiradi. Isolation, lock, atomic compare-and-set yoki unique constraint zarur.
Distributed tizimda network partition sabab global invariantni darhol saqlash availability bilan ziddiyatga kirishi mumkin. Escrow, ownership partitioning yoki consensus kritik invariantni boshqaradi. Eventual consistency barcha qoidani kechiktirish mumkin degani emas.
Kuzatuv
Production’da invariant check buzilsa metric va strukturali log chiqaradi. Barcha requestda qimmat global scan qilish o‘rniga transaction paytidagi lokal constraint yoki sample audit ishlatilishi mumkin. Background consistency checker tarixiy buzilishlarni topadi.
Invariant repair avtomatik bo‘lsa qaysi canonical manba to‘g‘ri ekani aniqlanishi kerak. Noto‘g‘ri “tuzatish” dalilni yo‘qotishi mumkin; audit trail va ta’sirlangan obyektlar saqlanadi.
Bog‘liq tushunchalar
Assertion, Precondition, Postcondition, Property-based testing, Database constraint, Transaction, Formal verification