Кіріспе
Компьютерлік бағдарламалауда, кодтың орындалуының белгілі бір нүктесінде предикаттың әрқашан дұрыс екенін күтілетін жайт – компьютерлік бағдарламалау түсінігі. Компьютерлік бағдарламалауда, әсіресе императивті бағдарламалау парадигмасын қолданғанда, нақтылау (assertion) – бұл программаның бір нүктесіне байланысты, код орындалғанда әрқашан дұрыс болуға тиіс предикат (көбінесе бағдарлама айнымалыларын қолданып логикалық тұжырым ретінде берілген, жағдай кеңістігіндегі Бульдік мәнді функция). Нақтылаулар бағдарламашыға кодты түсінуге, компиляторға оны құрастыруға немесе бағдарламаға өзінің қателіктерін табуға көмектеседі. Соңғы жағдайда кейбір бағдарламалар орындалу кезінде предикатты тексеру арқылы нақтылауды растайды. Егер ол дұрыс болмаса – нақтылау сәтсіздігі – бағдарлама өзін бұзылған деп есептейді және әдетте қасақана құлайды немесе нақтылау қатесін тудырады.
the computer programming concept
In computer programming, specifically when using the imperative programming paradigm, an assertion is a predicate (a Boolean valued function over the state space, usually expressed as a logical proposition using the variables of a program) connected to a point in the program, that always should evaluate to true at that point in code execution. Assertions can help a programmer read the code, help a compiler compile it, or help the program detect its own defects. For the latter, some programs check assertions by actually evaluating the predicate as they run. Then, if it is not in fact true – an assertion failure – the program considers itself to be broken and typically deliberately crashes or throws an assertion failure exception.
Қолданылуы
Эйфель сияқты тілдерде нақтылаулар жобалау процесінің бөлігі болып табылады, ал C және Java сияқты басқа тілдерде олар тек орындалу кезіндегі шарттарды тексеру үшін қолданылады. Екі жағдайда да оларды орындалу кезінде тексеруге болады, бірақ көбінесе оларды өшіруге де болады.
Келісім-шарт бойынша жобалаудағы мәлімдемелер
Асерциялар құжаттаманың бір түрі ретінде жұмыс істей алады: олар кодтың орындалуына дейін күтілетін күйін (алғышарттары) және орындалғаннан кейін күтілетін күйін (постшарттары) сипаттай алады; сондай-ақ, олар кластың инварианттарын анықтай алады. Eiffel тіліне мұндай асерцияларды енгізеді және класты құжаттау үшін оларды автоматты түрде шығарып алады. Бұл келісімшарт бойынша жобалау әдісінің маңызды бөлігі болып табылады. Бұл тәсіл тілде тікелей қолдау көрсетілмесе де пайдалы: түсініктемелердегі асерцияларға қарағанда асерция операторларын пайдаланудың артықшылығы – бағдарлама әр орындалғанда асерцияларды тексеруге мүмкіндік береді; егер асерциялар енді орындалмаса, қате туралы хабар беріледі. Бұл кодтың асерциялармен үйлесімсіздікке түсуіне жол бермейді.
Даму кезеңіндегі мәлімдемелер
Даму циклы барысында бағдарламашы әдетте бағдарламаны күәландыруларды (assertion) қосып іске қосады. Күәландыру сәтсіз болған жағдайда бағдарламашыға мәселе туралы дереу хабар беріледі. Көптеген күәландыру жүзеге асырулар бағдарламаның орындалуын тоқтатады: бұл пайдалы, себебі бағдарлама күәландыру талабы бұзылғаннан кейін жұмысын жалғастырса, оның жай-күйі бұзылып, мәселенің себебін анықтау қиындауы мүмкін. Күәландыру сәтсіздігі туралы берілген ақпаратты (мысалы, сәтсіздік орны және, мүмкін, стек ізбеталы, тіпті қоршаған орта өзекті сақтауды қолдайтын болса немесе бағдарлама жөндеу құралында іске қосылса, толық бағдарлама жай-күйі) пайдалана отырып, бағдарламашы әдетте мәселені шеше алады. Осылайша, күәландырулар қателерді жоюда өте қуатты құрал болып табылады.
Өндірістік ортадағы мәлімдемелер
Бағдарлама өндіріске енгізілген кезде, олардың тудыратын қосымша шығындар мен жанама әсерлерді болдырмау үшін, тексерулер әдетте өшіріледі. Кейбір жағдайларда, C/C++ тіліндегі макростар арқылы жасалған тексерулер сияқты, орналастырылған кодта тексерулер мүлдем болмайды. Ал Java сияқты басқа жағдайларда, тексерулер орналастырылған кодта қалады және қателерді жою үшін өрісте қосылуы мүмкін. Тексерулер компиляторға белгілі бір шектен шығу жағдайының іс жүзінде орын алмайтынын хабарлау үшін де қолданылуы мүмкін, соның арқасында басқа жағдайда мүмкін болмас еді деген оптимизациялар жасауға болады. Мұндай жағдайда, тексерулерді өшіру өнімділіктің төмендеуіне әкелуі мүмкін.
Құжаттарды бұғаттау
Көптеген тілдер тұжырымдамаларды жаһандық түрде, кейде дербес қосуға немесе өшіруге мүмкіндік береді. Тұжырымдамалар көбінесе әзірлеу кезінде қосылады және соңғы сынақ кезінде, сондай-ақ клиентке жіберілгенде өшіріледі. Тұжырымдамаларды тексермеу, тұжырымдамаларды бағалауға кеткен шығындарды болдырмайды (тұжырымдамалардың жанама әсерлері жоқ деп есептегенде), сонымен бірге қалыпты жағдайда бірдей нәтижеге қол жеткізеді. Ерекше жағдайларда тұжырымдамаларды тексеруді өшіру бағдарламаның қатеге тоқтап қалуының орнына жұмысын жалғастыруы мүмкін. Кейде мұндай жағдай қажет болады. C, YASS және C++ сияқты кейбір тілдер препроцессорды пайдаланып тұжырымдамаларды компиляция кезінде толығымен жоюға мүмкіндік береді. Сол сияқты, Python интерпретаторын "O" ("оптимизациялау" үшін) аргументімен іске қосу Python кодты генератордың тұжырымдамалар үшін байт-кодты жасамауына себеп болады. Java-да тұжырымдамаларды қосу үшін орындалу кезіндегі қозғалтқышқа опция берілуі керек. Егер бұл опция берілмесе, тұжырымдамалар орындалмайды, бірақ олар JIT компиляторымен орындалу кезінде оңтайландырылмаса немесе бағдарламашы қолмен әр тұжырымдаманы if (false) шартының артына орналастырмаса, кодта қалады. Бағдарламашылар тілдің тұжырымдамаларды тексеру механизмін айналып өту арқылы немесе өзгерту арқылы кодқа әрқашан белсенді болатын тексерулерді енгізе алады.
Тарих
1947 жылы фон Нейман мен Голдстайн IAS машинасының дизайны туралы баяндамаларында олар ағындық диаграммалардың ерте нұсқасын қолдана отырып алгоритмдерді сипаттады, онда олар мынадай мәлімдемелерді қосты: «C ағындық диаграмманың белгілі бір нүктесіне жеткен кезде бір немесе бірнеше байланысты айнымалылар міндетті түрде белгілі бір көрсетілген мәндерге ие болуы мүмкін, немесе белгілі бір қасиеттерге ие болуы мүмкін, немесе бір-бірімен сәйкес келуі мүмкін. Бұдан әрі, мұндай нүктеде осы шектеулердің дұрыстығын көрсетуге болады. Осы себепті, мұндай шектеулердің жарамдылығы расталатын әрбір аймақты біз арнайы қораппен белгілейміз, оны мәлімдемелер қорабы деп атаймыз». Бағдарламалардың дұрыстығын дәлелдеудің мәлімдемелік әдісін Алан Тьюринг қолдады. 1949 жылғы 24 маусымда Кембриджде өткен «Үлкен ретті тексеру» атты баяндамасында Тьюринг былай деді: «Үлкен ретті қалай тексеруге болады? Тексерушінің жұмысын қиындатпау үшін бағдарламашы жеке-жеке тексеруге болатын және бағдарламаның дұрыстығын оңай анықтауға мүмкіндік беретін бірқатар нақты мәлімдемелер жасауы керек».