Анализа коректности алгоритама

Делови текста у наствку су преузети из скрипте “Програмирање 2”, аутора Предрага Јаничића и Филипа Марића.

Исправност тј. коректност је суштинска особина алгоритама и програма. Иако се некада у пракси користе програми за које се зна да понекад могу да дају и нетачне резултате, то најчешће није случај и од програма се захтева да буде практично апсолутно непогрешив.

Једно од централних питања у развоју програма је питање његове исправности (коректности). Софтвер је у данашњем свету присутан на сваком кораку: софтвер контролише много тога — од банковних рачуна и компоненти телевизора и аутомобила, до нуклеарних електрана, авиона и свемирских летелица. У свом том софтверу неминовно су присутне и грешке. Грешка у функционисању даљинског управљача за телевизор може бити тек узнемирујућа, али грешка у функционисању нуклеарне електране може имати разорне последице. Најопасније грешке су оне које могу да доведу до великих трошкова, или још горе, до губитка људских живота. Неке од катастрофа које су општепознате су експлозија ракете Ариане 1996. узрокована конверзијом броја из шездесетчетворобитног реалног у шеснаестобитни целобројни запис која је довела до прекорачења, затим пад сателита Криосат (енгл. Cryosat) 2005. године услед грешке у софтверу због које није на време дошло до раздвајања сателита и ракете која га је носила коштао је Европску Унију око 135 милиона евра, затим грешка у нумеричком копроцесору процесора Pentium 1994. узрокована погрешним индексима у петљи for у оквиру софтвера који је радио дизајн чипа, као и пад орбитера послатог на Марс 1999. узрокован чињеницом да је део софтвера користио метричке, а део софтвера енглеске јединице. Међутим, фаталне софтверске грешке и даље се непрестано јављају и оне коштају светску економију милијарде долара. Ево неких од најзанимљивијих:

• Не нарочито опасан, али веома занимљив пример грешке је грешка у програму Microsoft Excel 2007 који, због грешке у алгоритму форматирања бројева пре приказивања, резултат израчунавања израза 77.1 * 850 приказује као 100 000 (иако је интерно коректно сачуван).

• У Лос Анђелесу је 14. септембра 2004. године више од четиристо авиона у близини аеродрома истовремено изгубило везу са контролом лета. На срећу, захваљујући резервној опреми унутар самих авиона, до несреће ипак није дошло. Узрок губитка везе била је грешка прекорачења у бројачу милисекунди у оквиру система за комуникацију са авионима. Да иронија буде већа, ова грешка је била откривена раније, али пошто је до открића дошло када је већ систем био испоручен и инсталиран на неколико аеродрома, његова једноставна поправка и замена није била могућа. Уместо тога, препоручено је да се систем ресетује сваких 30 дана како до прекорачења не би дошло. Процедура није испоштована и грешка се јавила после тачно \(2^{32}\) милисекунди, односно 49,7 дана од укључивања система.

• Више од пет процената пензионера и прималаца социјалне помоћи у Немачкој је привремено остало без свог новца када је 2005. године уведен нови рачунарски систем. Грешка је настала због тога што је систем, који је захтевао десетоцифрени запис свих бројева рачуна, код старијих рачуна који су имали осам или девет цифара бројеве допуњавао нулама, али са десне уместо са леве стране како је требало.

• Једна бака у Америци је на свој 106. рођендан добила позив да мора да крене у школу, јер је систем бележио године помоћу две цифре.

• Компаније Dell и Apple морале су током 2006. године да корисницима замене више од пет милиона лаптоп рачунара због грешке у дизајну батерије компаније Sony која је узроковала да се неколико рачунара запали.

Облици испитивања коректности

У развијању техника верификације програма, потребно је најпре прецизно формулисати појам коректности тј. исправности програма. Исправност програма почива на појму спецификације. Спецификација је, неформално, опис жељеног понашања програма који треба написати. Спецификација се обично задаје у терминима предуслова тј. услова које улазни параметри програма задовољавају, као и постуслова тј. услова које резултати израчунавања морају да задовоље. Када је позната спецификација, потребно је верификовати програм, тј. доказати да он задовољава спецификацију.

Коректност се огледа кроз два аспекта:

парцијална коректност:

свака вредност коју алгоритам израчуна за улазне параметре који задовољавају спецификацију (тј. предуслов) мора да задовољи спецификацију (тј. постуслов).

заустављање

алгоритам мора да се заустави за све улазе који задовољавају спецификацију (тј. предуслов).

Већина алгоритама које ћемо проучавати у овом курсу биће потпуни тј. заустављаће се за све допуштене улазе. За заустављајуће парцијално коректне алгоритме кажемо да су тотално коректни. Интересантно, доказано је да не постоје алгоритми којима би се испитивала горе наведена својства алгоритама.

Поступак показивања да је програм исправан назива се верификовање програма. Два основна приступа верификацији су:

динамичка верификација

подразумева проверу исправности у фази извршавања програма, најчешће путем тестирања;

статичка верификација

подразумева анализу изворног кода програма, често коришћењем формалних метода и математичког апарата.

Систематично тестирање је сигурно најзначајнији облик постизања високог степена исправности програма. Тестирањем на већем броју исправних улаза и упоређивањем добијених и очекиваних резултата може се открити велики број грешака. Нагласимо и да се тестирањем не може показати да је програм коректан, већ само да није коректан. Наиме, практично никада није могуће испитати понашање програма баш на свим исправним улазима. Већ програм који сабира два 32-битна броја има \(2^{32}\cdot 2^{32} = 2^{64}\) исправних комбинација улазних параметара и исцрпно тестирање оваквог програма би трајало годинама. Зато се исцрпно тестирање скоро никада не спроводи, већ се програми тестирају тако да се улази бирају пажљиво, тако да покрију различите гране током извршавања програма. Обично се додатно посебно тестира понашање програма на неким граничним улазима (енгл. edge cases, corner cases), јер програми понекада не обрађују све специјалне случајеве како би требало. Многи системи за учење програмирања (такозвани грејдери, енгл. grader) оцењују ученичка решења тестирањем на већем броју тест-примера и савет почетницима је да током учења обавезно користе овакве системе.

О методама статичке верификације биће више речи у наставку овог поглавља.

Неке честе грешке у програмима

Сваки исправан програм мора да буде заснован на исправном алгоритму. Дакле, од неисправног алгоритма није могуће направити исправан програм и основна ствар приликом писања исправних програма је да се обезбеди исправност алгоритма који се примењује. Са друге стране, алгоритми се описују често на апстрактнијем нивоу него што су сами програми, и многи детаљи се занемарују. Зато се услед детаља имплементације од исправног алгоритма може добити неисправан програм. Наведимо неке честе грешке.

• Једна од најчешћих грешака представља грешка прекорачења (енгл. overflow). Наиме, ако се у имплементацији одабере бројевни тип података којим се не могу исправно представити сви подаци, тада програм даје неисправне резултате. Чест је случај да програмер одабере тип података који може да репрезентује исправно и улазне и излазне вредности, међутим, дешава се да међурезултати не могу да се репрезентују исправно, што се теже примети, а доводи до грешке.

• Честа грешка је прекорачење граница низа (енгл. buffer overflow). На пример, ако смо у низу одвојили место за 30 бројева, онда је могуће уписивати вредности само на позиције \(0, 1, \ldots, 29\). Нарочито је критична позиција \(30\) (тј. у општем случају позиција \(n\) за низ од \(n\) елемената). Пошто у савременим програмским језицима бројање позиција у низовима креће од нуле, на позицију \(n\) није могуће уписивати вредности. У језику C++ се не врши провера опсега пре приступа елементима низа (тј. вектора) и одговорност је програмера да обезбеди да се не приступа ван граница - у супротном је понашање програма недефинисано, што значи да програм може да настави да ради неисправно и после одређеног броја инструкција да буде прекинут од стране оперативног система, али и да грешка може да прође неопажено. Уколико у петљи у низ уписујемо податке чији број не знамо унапред, неопходно је да пре сваког уписа проверимо да ли се упис врши унутар граница низа (или да користимо неки облик низа који допушта аутоматско проширивање додавањем нових елемената).

• Честа грешка је необраћање пажње на специјалне случајеве. На пример, ако у низу тражимо први елемент који задовољава неки услов, неопходно је да обезбедимо да програм коректно ради и у случају када ниједан елемент не задовољава тај услов. Треба пажљиво прецизирати да ли функција тада треба да врати број елемената низа или, на пример, -1, и треба осигурати да се у коду који позива ову функционалност добро реагује на ситуацију у којој тражени елемент не постоји. Специјални случајеви најчешће настају када неке вредности не постоје (када је неки скуп чије елементе разматрамо празан), затим када су улазне вредности у неком специјалном односу (на пример, да ли геометријски програм исправно ради ако су унете тачке колинеарне) и слично. При том, треба пажљиво прецизирати спецификацију задатка и одредити који специјални случајеви јесу, а који нису допуштени спецификацијом. Поново је потребно обратити пажњу на то да иако улазни параметри понекада не могу бити у неком специјалном односу, то не значи да међурезултати неће бити у том односу, па је онда потребно програме ипак прилагодити да обрате пажњу на све специјалне случајеве.

Индуктивно-рекурзивна конструкција

Кључна идеја у конструкцији алгоритама је то да је конструкција алгоритама веома тесно повезана са доказивањем теорема математичком индукцијом. Математичка индукција, у свом основном облику, је следећи начин доказивања особина природних бројева. Нека је \(P\) произвољно својство које се може формулисати за природне бројеве. Тада важи

\[(P(0) \wedge (\forall n)(P(n) \Rightarrow P(n+1))) \Rightarrow (\forall n)(P(n))\]

Дакле, да бисмо доказали да сваки природан број има неко својство \(P\) (тј. да бисмо доказали \((\forall n)(P(n))\)), довољно је да докажемо да нула има то својство (тј. \(P(0)\)) и да докажемо да чим неки број има то својство, има га и његов следбеник (тј. да докажемо \((\forall n)(P(n) \Rightarrow P(n+1))\)). Прво тврђење се назива база индукције, а друго индуктивни корак. Приницип математичке индукције је прилично јасан – на основу базе знамо да 0 има својство \(P\), на основу корака да њен следбеник тј. 1 има својство \(P\), на основу корака да његов следбеник тј. 2 има својство \(P\) итд. Интуитивно нам је јасно да на овај начин можемо стићи до било ког природног броја, који сигурно мора имати својство \(P\). База се може формулисати и за веће вредности од нуле, али онда само можемо да тврдимо да елементи који су већи или једнаки од базе имају својство \(P\).

Основни приступ конструкције алгоритама је тзв. индуктивни тј. рекурзивни приступ. Он у свом основном облику подразумева да се решење проблема веће димензије проналази тако што умемо да решимо проблем истог облика, али мање димензије и да од решења тог проблема добијемо решење проблема веће димензије (у напреднијим облицима је могуће и да се решава већи број проблема мање димензије). Притом за почетне димензије проблема решење морамо да израчунавамо директно, без даљег свођења на проблеме мање димензије. Ако се приликом свођења димензија проблема увек смањује, конструисани алгоритми ће се увек заустављати.

• Имплементација алгоритма може бити таква да променљиве унутар петље итеративно ажурирају своје вредности кренувши од вредности које представљају решења елементарних проблема, па до крајњих вредности које представљају решења задатог проблема. Пошто је ово прилично слично принципу математичке индукције, кажемо да је алгоритам дефинисан индуктивно.

• Имплементација може бити таква да функција која решава полазни проблем сама себе позива да би решила проблем истог облика, али мање димензије (осим у случају елементарних проблема, који се директно решавају) и тада кажемо да је алгоритам дефинисан рекурзивно.

Индуктивна конструкција лежи у основни практично свих итеративних алгоритама које смо до сада разматрали. На пример, алгоритам израчунавања збира серије бројева (на пример, збира елемената неког низа) почива на томе да знамо да израчунамо збир празне серије (то је 0) и да ако знамо збир серије од \(k\) елемената, тада умемо да израчунамо и збир серије која се добија проширивањем те серије додатним \(k+1\)-вим елементом (то радимо тако што дотадашњи збир увећамо за тај нови елемент).

    int zbir = 0;
    for (int i = 0; i < a.size(); i++)
        zbir = zbir + a[i];

Дакле, и у овом алгоритму имамо индуктивну базу (која одговара иницијализацији променљиве пре уласка у петљу) и индуктивни корак (који одговара телу петље, у ком се ажурира вредност резултујуће променљиве, у овом случају збира). База може одговарати и случају једночланог (а не обавезно празног) низа, али тада не можемо да гарантујемо да ће алгоритам радити исправно у случају празног низа. То одговара варијанти алгоритма у којој збир иницијализујемо на први елемент низа, па га увећавамо редом за један по један елемент од позиције 1 надаље.

Рекурзивна имплементација израчунавања збира елемената низа може бити следећа (у њој се приликом решавања проблема димензије \(n > 0\) експлицитно захтева решавање проблема димензије \(n-1\)).

int zbir(int a[], int n) {
    if (n == 0)
       return 0;
    else
       return zbir(a, n-1) + a[n-1];
}

Дефинисање алгоритама индуктивно-рекурзивом конструкцијом је у веома тесној вези са доказивањем њихове коректности. Иако постоје формални оквири за доказивање коректности императивних програма (пре свега Хорова логика), ми ћемо се бавити искључиво неформалним доказима и веза између логике у којој вршимо доказивање и (императивног) програмског језика у којем се програм изражава биће прилично неформална.

Рецимо и да ћемо приликом доказивања коректности програма обично игнорисати ограничења записа бројева у рачунару и подразумеваћемо да је опсег бројева неограничен и да се реални бројеви записују са максималном прецизношћу. Дакле, нећемо обраћати пажњу на грешке које могу настати услед прекорачења или поткорачења вредности током извођења аритметичких операција (иако реално то често може бити узрок грешака у програмима).

Доказ коректности рекурзивних функција

Проблем: Дефинисати функцију која одређује минимум непразног низа бројева и доказати њену коректност.

Алгоритам се веома једноставно конструише индуктивно-рекурзивном конструкцијом. Димензија проблема у овом примеру је број елемената низа.

База:

Ако низ има само један елемент, тада је тај елемент уједно и минимум.

Корак:

У супротном, претпоставимо да некако умемо да решимо проблем за мању димензију и на основу тога покушајмо да добијемо решење за цео низ. Дакле, претпоставимо да је дужина низа \(n > 1\) и да умемо да нађемо број \(m\) који представља минимум првих \(n-1\) елемената низа. Минимум целог низа дужине \(n\) је мањи од бројева \(m\) и преосталог, \(n\)-тог елемента низа (ако бројање креће од \(0\), то је елемент \(a_{n-1}\)).

На основу овога можемо дефинисати рекурзивну функцију.

#include <iostream>
using namespace std;

int min2(int a, int b) {
    return a < b ? a : b;
}

int minNiza(int a[], int n) {
    if (n == 1)
       return a[0];
    else {
       int m = minNiza(a, n-1);
       return min2(m, a[n-1]);
    }
}

int main() {
    int a[] = {3, 5, 4, 1, 6, 2, 7};
    int n = sizeof(a) / sizeof(int);
    cout << minNiza(a, n) << endl;
}

Рецимо и да смо уместо дефинисања функције min2 за одређивање минимума два броја могли користити и функцију std::min из заглавља <algorithm>. Ипак, у овим програмима нећемо користити специфичне могућности језика C++, да бисмо нагласили да технике које у овом поглављу уводимо нису ни по чему специфичне за тај језик.

Примећујемо огромну сличност између рекурзивне конструкције алгоритма и индуктивног доказа његове коректности. Стога слободно можемо да кажемо да су рекурзија и индукција “две стране исте медаље” (индукцију користимо као технику доказивања, а рекурзију као технику дефинисања функција тј. конструкције алгоритама).

Рецимо и да је овај облик коришћења математичке индукције мало нестандардан, јер се не користи директно индукција по природним бројевима, већ се користи индукција по структури рекурзивне функције у којој се, из претпоставке да сваки рекурзивни позив враћа коректан резултат, доказује да функција враћа коректан резултат. Таква теорема индукције се може доказати на основу класичне математичке индукције по броју рекурзивних позива, под претпоставком да се докаже да се рекурзивна функција увек зауставља.

Доказ коректности итеративних алгоритама - инваријанте петље

Један од основних појмова у анализи и разумевању итеративних програма су инваријанте петљи. То су логички услови који важе непосредно пре петље, затим након сваког извршавања наредби у телу петље и непосредно након извршавања целе петље. Корисне инваријанте су оне које гарантују коректност алгоритма који та петља имплементира. Инваријанте суштински описују значење свих променљивих унутар петље. Илуструјмо појам инваријанте на једном једноставном примеру.

Размотримо следећу, класичну имплементацију алгоритма за одређивање минимума непразног низа бројева.

#include <iostream>
#include <algorithm>
using namespace std;

int min2(int a, int b) {
    return a < b ? a : b;
}

int minNiza(const vector<int>& a) {
    int m = a[0];
    for (int i = 1; i < a.size(); i++)
        m = min2(m, a[i]);
    return m;
}

int main() {
    vector<int> a{3, 5, 4, 1, 6, 2, 7};
    cout << minNiza(a) << endl;
}

У сваком кораку петље, део низа чији минимум знамо постаје дужи за по један елемент. Алгоритам креће од префикса низа дужине \(1\) и поставља променљиву m на вредност првог елемента низа \(a_0\). У сваком кораку петље, претпостављамо да променљива \(m\) садржи вредност минимума првих \(i\) елемената низа, а онда у телу петље обрађени део низа проширујемо додајући \(i+1\)-ви елемент низа, на позицији \(i\). Минимум проширеног низа се израчунава као минимум минимума првих \(i\) елемената низа (чија је вредност смештена у променљивој m) и додатног елемента низа \(a_i\). Након извршавања тела петље, део низа чији минимум је познат је проширен на \(i+1\) елемент. На крају петље је \(i\) једнако дужини низа, па променљива m садржи минимум целог низа.

    int n = a.size();
    int m = a[0];
    int i = 1;
    while (i < n) {
        m = min2(m, a[i]);
        i++;
    }

Ако размотримо структуру претходног разматрања, можемо установити да смо идентификовали логичке услове који су испуњени непосредно пре и непосредно након сваког извршавања тела петље. Такви услови се називају инваријанте петље. Да бисмо доказали да је неки услов инваријанта петље, довољно је да докажемо:

1. да тај услов важи пре првог уласка у петљу и

2. да из претпоставке да тај услов важи пре неког извршавања тела петље и да је услов петље испуњен докажемо да тај услов важи и након извршавања тела петље.

Те две чињенице нам, на основу индуктивног аргумента, гарантују да ће услов бити испуњен пре и после сваке итерације петље, као и након извршавања целе петље (ако се она икада заустави), тј. да ће тај услов бити инваријанта петље (тај доказ се може спровести класичном математичком индукцијом на основу броја извршавања тела петље). Приметимо да први корак одговара доказивању базе индукције, а други доказивању индуктивног корака.

Свака петља има пуно инваријанти, међутим, од интереса су нам само оне инваријанте које у комбинацији са условом прекида петље (под претпоставком да петља није прекинута наредбом break) имплицирају услов који нам је потребан након петље. Ако је петља једина у неком алгоритму, обично је то онда услов коректности самог алгоритма. Дакле, након доказа леме која чини основу доказа да је неки услов инваријанта петље, потребно је да докажемо и

3. да из тога да инваријанта важи након завршетка петље и да услов петље није испуњен следи коректност алгоритма.

Дакле, општа структура анализе програма коришћењем инваријанти се може описати на следећи начин.

<incijalizacija>
// ovde vazi <invarijanta>
while (<uslov>) 
   // ovde vaze i <uslov> i <invarijanta>
   <telo>
   // ovde vazi <invarijanta>
// ovde ne vazi <uslov>, a vazi <invarijanta>

У наставку ћемо виде још неколико примера примене технике инваријанте петље на доказ коректности алгоритама. Мора се признати да када се техника користи потпуно формално, да би се доказала коректност већ написаног програмског кода, то не делује нарочито инспиришуће (поготово, ако су програми једноставни и ако је једноставно интуитивно разумети разлоге њихове коректности). Ретко када се у практичном програмирању коректност заиста доказује потпуно формално (осим у случају софтвера који може да угрози велики број живота, попут, на пример, софтвера који управља метро-системом у Паризу, који јесте у потпуности формално верификован). Међутим, аргументе и инваријанте на којима коректност почива програмер често “проврти по глави”. Видећемо и да се техника инваријанти може употребити и пре него што је програм написан у циљу извођења програмског кода из спецификације. Јасне инваријанте често једнозначно указују на то како програмски кôд треба да изгледа и на тај начин помажу у процесу програмирања.

Задаци који су одабрани нису ни по чему посебни – они ће бити поновљени у поглављима у којима се уводе опште програмерске технике које се у њима примењују.