Бағдарламалар мен олардың ерекшеліктерін дәлелдеудің формальды тәсілдері

Алгоритм верификациясы

Верифика́ция (лат тілінен алғанда verus — «шынайы» facere — «жасау») сөзін адамның жұмыс жасау ортасына сай көптеген мағынасын алуға болады. Мысалға:

Верификация — тексеріс, тексерушілік, неше түрлі дәлел мен теоретикалық анықтамалар арқылы программалар, алгоритмдер, процедураларды растау әдісі, ол әдіс көбіне эталонды растаулармен салыстыра жүргізіледі. Ол принцип алғашқыда вена үйірмесінде қарастырылды.

Верификация — эталонды шарттарды өте отырып оларды өорытынды өніммен салыстыру әдісі.

Дәлелдеу, растау процесі кезінде құбылыстар немесе заттар тексерісі кезінде негізінен қолданылатын түсініктер:

§ Гипотеза — постулаттар, түсініктер, дәлелдеулерді негізге ала отырып шыққан толық расталмаған және ойлаулар арөылы ғана жеткізіліп отырған ұғымдар.

§ Концепция — растайтын дәлелі бар не жоқ модель.

§ Теория — алдын ала берілген растауларға сене отырып жасалған максималды түрде жақын түсінік..

1. Алгоритм дұрыстығы.

Бағдарламалар мен олардың ерекшеліктерін дәлелдеудің формальды тәсілдері

БҚ анализінің дәстүрді тәсілдері бағдарламаның дұрыстығын дәлелдеумен байланысты(бағдарлама верификациясы). Бұл бағытқа П. Наура мен Р. Флоидтың жұмыстары бастау берген болды. Онда индуктивті немесе аралық тұжырымдамалық деп бағдарлама нүктесіне жазып қою идеясы түйінделген болатын және индуктивті тұжырымдар сәйкестігіне құрылған бағдарламаның жеке бөлігінің дұрыстығын дәлелдеу мүмкіндігі көрсетілді.(яғни оның алғышарты мен соңғы шартының сәфйкестігі).

Ч. Хоор верификация теориясына іргелі үлес қосты, ол бағдарламаның бөлігінің дұрыстығына кейбір логикалық жүйеде шығару арқылы жүргізу туралы идеялар айтқан болатын, ал Э. Дейкстра болса, бір уақытта алғышарт пен соңғы шарттың сәйкестігін және аяқталуын білдіретін әлсіз алғышарт түсінігін енгізді. Бағдарламаның дұрыстығын дәлелдеу тәсілдері белгілі бір дәрежеде бағдарламалауға пайдасын тигізді. Бұл тәсілдердің бағдарламаның орындалу жолы туралы ойлау тәсілдерін көрсететіні, бағдардамада түсініктеме қалдырудың ыңғайлы жүйесін беретіні және бағдарламалау тілдерінің құрылымдары мен семантикалары арасында өзара байланыс орнататыны айқындалды. Егер бағдарламаның әр түрлі қасиеттерін дәлелдеу немесе бағдарламаларды дәлелдеу теоремасы ретінде «бағдарлама анализі» терминінің кең түсінікті мағынасын қабылдасақ, онда тәсілдердің құндылығы анықталады. Жеке жағдайда бағдарламаның шығыс деректірінің мәндерінің өзгеруін, бағдарлама орындалуы кезінде операциялар санын, циклдың, қолданысқа түспеген бағдарлама бөлігінің бар болуын зерттеуге болады. Осылай, кейбір жеке жағдайларда верификация тәсілдері бағдарламалық кемшіліктерді анықтау үшін де қолданыла береді.

Кейбір логикалық жүйеде шығару түріндегі формалды дәлелдеме толық сенімді, алайда дәлелдемелер өте ұзақ және жиі түсініксіз болады.