Кіріспе

Компьютерлік бағдарламалауда посткондиция – кодтың белгілі бір бөлігі орындалғаннан кейін немесе формальды сипаттамадағы операциядан кейін міндетті түрде орындалуы тиіс шарт немесе предикат. Посткондициялар кейде кодтың ішіндегі мәлімдемелер арқылы тексеріледі. Көбінесе посткондициялар әсер ететін код бөлігінің құжаттамасына енгізіледі. Мысалы: Факториалдың нәтижесі әрқашан бүтін сан болады және 1-ге тең немесе одан үлкен болады. Сондықтан, енгізілген санның факториалын есептейтін бағдарламада есептеуден кейін нәтиже бүтін сан болуы және ол 1-ге тең немесе одан үлкен болуы керек. Тағы бір мысал: енгізілген санның квадрат түбірін есептейтін бағдарламада нәтиже сан болуы керек және оның квадраты енгізілген санға тең болуы керек.

Нысанға бағдарланған бағдарламалаудағы постшарттар

Кейбір бағдарламалық жасақтаманы жобалау тәсілдерінде постшарттар, алғы шарттармен және сынып инварианттарымен бірге, келісімшарт арқылы бағдарламалық жасақтама құру әдісінің құрамдас бөліктері болып табылады. Кез келген процедура үшін постшарт – процедура орындалуын аяқтағаннан кейін кепілдірілетін қасиеттердің сипаттамасы. Процедураның келісімшартымен байланысты, постшарт потенциалды шақырушыларға процедура алғы шартын қанағаттандыратын күйде шақырылған жағдайда, постшартта жарияланған қасиеттердің қамтамасыз етілетініне сенім береді.

Кейінгі шарттар мен мұрагерлік

Мұрагерлік болған жағдайда, ұрпақ кластар (кіші кластар) мұраға алған процедураларды олардың келісімшарттарымен, яғни алғы және кейінгі шарттарымен бірге алады. Бұл, мұраға алған процедуралардың кез келген іске асырылуы немесе қайта анықталуы олардың мұраға алған келісімшарттарына сәйкес болуы керек дегенді білдіреді. Қайта анықталған процедураларда кейінгі шарттар өзгертілуі мүмкін, бірақ олар күшейтілуі керек. Яғни, қайта анықталған процедура клиентке ұсынатын мүмкіндіктерді арттыра алады, бірақ оларды азайта алмайды.