Invariantqa tiykarlanǵan programmalastırıw

Invariantqa tiykarlanǵan programmalastırıw — bul haqıyqıy programma operatorlarınan aldın specifikaciyalar hám invariantlar jazılatuǵın programmalastırıw metodologiyası. Programmalastırıw procesi dawamında invariantlardı jazıp alıwdıń bir qatar artıqmashılıqları bar: ol baǵdarlamashıdan programmanıń minez-qulqı haqqındaǵı niyetlerin onı haqıyqıy ámelge asırmastan aldın anıq aytıwın talap etedi hám invariantlar orınlanıw waqtında keń tarqalǵan programmalastırıw qátelerin anıqlaw ushın dinamikalıq túrde bahalanıwı múmkin. Bunnan tısqarı, eger jetkilikli dárejede kúshli bolsa, invariantlar programma operatorlarınıń formal semantikasına tiykarlanıp programmanıń durıslıǵın dálillew ushın qollanılıwı múmkin. Áhmiyetli emes programmalardı tolıq tekseriw ushın ádette kúshli formal dálillew sisteması menen baylanısqan birlesken programmalastırıw hám specifikaciya tili talap etiledi. Bul jaǵdayda dálillewlerdiń joqarı dárejeli avtomatlastırılıwı da múmkin.

Kópshilik qollanıwdaǵı programmalastırıw tillerinde tiykarǵı shólkemlestiriwshi strukturalar — for ciklleri, while ciklleri hám if operatorları sıyaqlı basqarıw aǵımı blokları. Bunday tiller invariantlarǵa birinshi orın beretuǵın programmalastırıw ushın ideal bolmawı múmkin, sebebi olar baǵdarlamashını invariantlardı jazıwdan aldın basqarıw aǵımı haqqında sheshimler qabıl etiwge májbúrleydi. Bunnan tısqarı, kópshilik programmalastırıw tillerinde specifikaciyalar hám invariantlar jazıw ushın jaqsı qollap-quwatlaw joq, sebebi olarda kvantifikator operatorları joq hám ádette joqarı dárejeli qásiyetlerdi ańlatıw múmkin emes.

Programmanı onıń dálili menen birge islep shıǵıw ideyası E.W. Deykstra-dan kelip shıqqan. Programma operatorlarınan aldın invariantlardı jazıwdı M.H. van Emden, J.C. Reynolds hám R-J Bek hár túrli formalarda qarastırǵan.