Једно од централних питања у развоју програма је питање његове исправности (коректности). Софтвер је у данашњем свету присутан на сваком кораку: софтвер контролише много тога — од банковних рачуна и компоненти телевизора и аутомобила, до нуклеарних електрана, авиона и свемирских летелица. У свом том софтверу неминовно су присутне и грешке. Грешка у функционисању даљинског управљача за телевизор може бити тек узнемирујућа, али грешка у функционисању нуклеарне електране може имати разорне последице. Најопасније грешке су оне које могу да доведу до великих трошкова, или још горе, до губитка људских живота. Крупне софтверске грешке и даље се непрестано јављају и оне коштају светску економију милијарде долара. Неки примери софтверских грешака који су изазвали велике проблеме описани су у додатку @sec:primeri_bagova.
Поступак показивања да је програм исправан назива се верификовање програма. Међутим, често се показује да питање шта уопште значи да је програм исправан није увек очигледно. На пример, да ли је наредна функција која израчунава степен исправна?
double stepen(double x, int n) {
double s = 1.0;
for (int i = 0; i < n; i++)
s *= x;
return s;
}Који је резултат следећих позива stepen(2.0, 10), stepen(-2.0, 10), stepen(2.0,-10), stepen(0.0, 0), stepen(1e200, 2)? Да ли су ти резултати исправни? Да ли је уопште дозвољено да изложилац буде негативан или да се израчунава \(0^0\)? Да ли резултат \((10^{200})^2\) може уопште да се исправно запише помоћу типа double? Све ово треба прецизирати да би се уопште могло дискутовати да ли је ова имплементација степеновања исправна.
Дакле, пре програма потребно је најпре прецизно формулисати појам исправности програма. Исправност програма почива на појму спецификације. Спецификација је, интуитивно, опис жељеног понашања програма који треба написати. Спецификација је обично ствар договора између наручиоца програма (корисника) и тима програмера који програм развијају. Веома важно је да се пре саме имплементације што прецизније договори шта је очекивано понашање програма. Често се спецификација мења и прецизира током развоја програма.
Спецификација се обично задаје у терминима предуслова тј. услова које улазни параметри програма морају да задовоље, као и постуслова тј. услова које резултати израчунавања морају да задовоље. У примеру функције степеновања предуслов може захтевати да је вредност броја \(n \geq 0\) и да ако је \(n=0\), тада је \(x \neq 0\), а постуслов да функција враћа вредност \(x^n\). Када је позната спецификација, потребно је верификовати програм, тј. доказати да он задовољава спецификацију. Приказана имплементација је исправна у односу на ову спецификацију само ако се занемаре проблеми прецизности и опсега записа реалних бројева у рачунару.
У оквиру верификације програма, веома важно питање је питање заустављања програма. Парцијална коректност подразумева да неки програм, уколико се заустави, даје коректан резултат (тј. резултат који задовољава спецификацију). Тотална коректност подразумева да се програм за све (спецификацијом допуштене) улазе зауставља, као и да су добијени резултати коректни.
Два основна приступа верификацији су:
динамичка верификација која подразумева проверу исправности у фази извршавања програма, најчешће путем тестирања;
статичка верификација која подразумева анализу изворног кода програма, често коришћењем формалних метода и математичког апарата.
О сваком од њих ће бити више речи у наставку.
Синтаксичке грешке у програмима су најмање опасне и најлакше отклоњиве, јер их пријављује компилатор и програм није могуће покренути док се све синтаксичке грешке не исправе.
Неке грешке (на пример, дељења нулом или покушаја приступа недозвољеном делу меморије) могу довести до насилног прекида извршавања (синтаксички исправног) програма (каже се понекада да “апликација пуца”). Много опасније су логичке грешке тј. ситуације у којима се програми успешно компилира, покреће и извршава али не ради оно што је од њега очекивано тј. даје погрешне резултате. Грешка може бити и у самој спецификацији тј. програм може да ради тачно оно што је од програмера захтевано, али то може бити другачије од онога што корисник очекује или што је желео. Веома важна група грешака су оне које су везане за безбедност и сигурност тј. грешке услед којих злонамерни корисници могу неовлашћено доћи у посед неких података или ресурса.
Наведимо и неколико најчешћих узрока грешака на нивоу имплементације и савете како да се оне заобиђу.
Грешке прекорачења. Чест разлог грешака у програмима је коришћење неодговарајућих типова података, тј. типова који узрокују да се услед прекорачења или поткорачења добију нетачни резултати израчунавања. Стога је увек пожељно имати у виду могуће распоне вредности улазних података и на основу њих проверити да ли су распони свих међурезултата и завршних резултата такви да могу да се представе одабраним типовима променљивих. У склопу провере граничних вредности, пожељно је увек укључити и намјање и највеће могуће вредности улазних величина.
Провера граничних вредности. Велики број грешака јавља се на границама опсега петље, граничним индексима низа, граничним вредностима аргумената аритметичких операција и слично. Због тога је тестирање на граничним вредностима изузетно важно и програм који пролази такве улазне величине често је исправан и за друге. На пример, ако се тестира програм који учитава један ред текста у неки низ, требало би проверити да ли програм исправно ради када је на улазу празан ред (тј. ред који садржи само карактер '\n'). Другом границом могу се сматрати улазни редови који су веома дуги (дужи од броја елемената низа у који се учитавају подаци) или пре чијег краја се налази крај тока података. Стога би требало проверити и да ли се програм исправно понаша при учитавању редова који су дуги колико и низ у који се учитавају подаци или краћи за један карактер, дужи за један карактер и слично.
Проверавање пре-услова. Да би неко израчунавање имало смисла често је потребно да важе неки пре-услови. На пример, ако је потребно израчунати просечан број поена \(n\) студената, питање је шта радити уколико је \(n\) једнако \(0\) и понашање програма треба да буде спецификовано и тестирано у таквим ситуацијама. Могуће је, на пример, да се ако је \(n\) једнако \(0\), врати \(0\) као резултат. Могуће је и да се, ако је \(n\) једнако \(0\), не дозволи израчунавање просека. У овом другом приступу, пре кода за израчунавање просека може да се наведе наредба assert(n > 0);, која у фази развоја програма узрокује да се пријави порука о томе да предуслов захтеван спецификацијом није био испуњен.
Проверавање успешности позива функција. Чест извор грешака током извршавања програма је непроверавање оних повратних вредности функција које указују на то да ли је функција успешно урадила оно што што је требало. На пример, функције за алокацију меморије, функције за рад са датотекама итд., нарочито ако потичу из програмског језика C, кроз своју повратну вредност обавештавају програмера да ли је дошло до неке грешке. Повратне вредности ових функција указују на потенцијални проблем и уколико се игноришу – проблем ће само постати већи. Слично, многе функције у језику C++ доводе до изузетака ако не могу успешно да изврше свој задатак. Те изузетке би требало “ухватити” и обрадити тј. учинити оно што је могуће да програм настави са радом или да бар кориснику пријави јасну поруку о томе зашто је дошло до грешке и зашто је извршавање програма морало бити прекинуто.
Динамичко верификовање програма подразумева проверавање исправности у фази извршавања програма. Најчешћи вид динамичког верификовања програма је тестирање.
Најзначајнија врста динамичког испитивања исправности програма је тестирање. Тестирање може да обезбеди висок степен поузданости програма, али најчешће не може да докаже да је програм у потпуности коректан.
Нека тврђења о програму је могуће тестирати, док нека није. На пример, тврђења попут “програм за овај улаз враћа овај излаз” или “програм има просечно време извршавања пола секунде” су (у принципу) проверива тестовима. Међутим, тврђење “просечно време извршавања програма је добро” сувише је неодређено да би могло да буде тестирано.
У идеалном случају, треба спровести исцрпно тестирање рада програма за све могуће улазне вредности и проверити да ли излазне вредности задовољавају спецификацију. Међутим, овакав исцрпан приступ тестирању скоро никада није практично применљив. На пример, исцрпно тестирање коректности програма који сабира два 32-битна броја, захтевало би укупно \(2^{32}\cdot 2^{32}=2^{64}\) различитих тестова. Под претпоставком да сваки тест траје једну наносекунду, исцрпно тестирање би захтевало приближно \(1{,}8\cdot 10^{10}\) секунди што је око 570 година. Дакле, тестирањем није практично могуће доказати исправност чак ни прилично тривијалних програма. С друге стране, тестирањем је могуће доказати да програм није исправан тј. пронаћи грешке у програмима.
С обзиром на то да исцрпно тестирање није практично применљиво, обично се користи техника тестирања типичних улаза програма као и специјалних, карактеристичних улазних вредности за које постоји већа вероватноћа да доведу до неке грешке. У случају поменутог програма за сабирање, типични случај би се односио на тестирање коректности сабирања неколико случајно одабраних парова бројева, док би за специјалне случајеве могли бити проглашени случајеви када је неки од сабирака 0, 1, -1, најмањи негативан број, највећи позитиван број и слично.
Постоје различите методе тестирања, а неке од њих су:
Тестирање засебних јединица (енгл. unit testing) У овој методи тестирања, независно се тестовима проверава исправност засебних јединица кода. “Јединица” је обично најмањи део програма који се може тестирати. У процедуралним језицима, “јединица” је обично једна функција. Сваки јединични тест треба да буде независан од осталих, али пуно јединичних тестова може да буде груписано у батерије тестова, у једној или више функција са овом наменом. Јединични тестови треба да проверавају понашање функције, за типичне, граничне и специјалне случајеве. Ова метода веома је важна у обезбеђивању веће поузданости када се многе функције у програму често мењају и зависе једна од других. Кад год се промени жељено понашање неке функције, потребно је ажурирати одговарајуће јединичне тестове. Ова метода веома је корисна због тога што често открива тривијалне грешке, али и због тога што јединични тестови представљају својеврсну спецификацију.
Постоје специјализовани софтверски алати и библиотеке које омогућавају једноставно креирање и одржавање оваквих тестова. Јединичне тестове обично пишу и користе, у току развоја софтвера, сами аутори програма или тестери који имају приступ коду.
Регресионо тестирање (енгл. regression testing) У овом приступу, проверавају се измене програма како би се утврдило да се нова верзија понаша исто као стара (на пример, генерише се исти излаз). За сваки део програма имплементирају се тестови који проверавају његово понашање. Пре него што се направи нова верзија програма, она мора да успешно прође све старе тестове како би се осигурало да оно што је раније радило ради и даље, тј. да није нарушена ранија функционалност програма.
Регресионо тестирање примењује се у оквиру самог имплементирања софтвера и обично га спроводе тестери.
Интеграционо тестирање (енгл. integration testing) Овај вид тестирања примењује се када се више програмских модула обједињује у једну целину и када је потребно проверити како функционише та целина и комуникација између њених модула. Интеграционо тестирање обично се спроводи након што су појединачни модули прошли кроз друге видове тестирања. Када нова програмска целина, састављена од више модула успешно прође кроз интеграционо тестирање, онда она може да буде једна од компоненти целине на вишем нивоу која такође треба да прође интеграционо тестирање.
Тестирање ваљаности (енгл. validation testing) Тестирање ваљаности треба да утврди да систем испуњава задате захтеве и извршава функције за које је намењен. Тестирање ваљаности врши се на крају развојног процеса, након што су успешно завршене друге процедуре тестирања и утврђивања исправности. Тестови ваљаности који се спроводе су тестови високог нивоа који треба да покажу да се у обрадама користе одговарајући подаци и у складу са одговарајућим процедурама, описаним у спецификацији програма.
Тестирање, као један од кључних видова за осигурање квалитета софтвера (енг. quality assurance), се данас развило се у добро утемељену и широко подржану област рачунарства. Један од праваца унапређивања процеса тестирања је његова аутоматизација. Уместо да тестирање спроводи особа (тестер), аутоматским тестирањем тај поступак преузима рачунар и спроводи га аутоматски и много брже, док тестер може да се посвети дизајну аутоматских тестова и анализи резултата аутоматског тестирања.
У савременим методологијама за развој софтвера, тестирање се у процес развоја уводи рано и захтева сарадњу програмера и тестера. Аутор аутоматских тестова реализује их коришћењем наменских библиотека и алата (који могу, на пример, да симулирају и комуникацију корисника путем графичког корисничког интерфејса). Програмер тако аутоматизоване тестове може да користи у оквиру неких интегрисаних развојних окружења. Постоји мноштво алата за аутоматизовано спровођење тестирања. Неки од њих део су интегрисаних развојних окружења а неки се користе као самостални системи. Они се разликују и по величини, захтеваном умећу и по врсти подршке за тимски рад. На пример, наредни тестови у библиотеци Google test (googletest) се могу употребити за аутоматско тестирање функције која израчунава степен.
double stepen(double x, int n);
TEST(StepenTest, PozitivanEksponent) {
EXPECT_DOUBLE_EQ(stepen(2.0, 3), 8.0);
}
TEST(StepenTest, NulaEksponent) {
EXPECT_DOUBLE_EQ(stepen(2.0, 0), 1.0);
}
TEST(StepenTest, NegativanEksponent) {
EXPECT_DOUBLE_EQ(stepen(2.0, -1), 0.5);
}Тестови се покрећу аутоматски и након покретања пријављује се следећи извештај, који указује на то да функција није коректно имплементирана за негативне изложиоце.
[==========] Running 3 tests from 1 test suite. [ RUN ] StepenTest.PozitivanEksponent [ OK ] StepenTest.PozitivanEksponent [ RUN ] StepenTest.NulaEksponent [ OK ] StepenTest.NulaEksponent [ RUN ] StepenTest.NegativanEksponent stepen_test.cpp:25: Failure Expected equality of these values: stepen(2.0, -1) Which is: 1 0.5 [ FAILED ] StepenTest.NegativanEksponent [==========] 4 tests ran. [ PASSED ] 3 tests. [ FAILED ] 1 test.
И поред аутоматизације, обично остаје и важан простор за ручно тестирање, посебно за аспекте коришћења програма које није лако аутоматизовати (попут субјективног осећаја корисника).
Тестирање је процес провере да ли програм ради исправно, односно систематичан покушај да се пронађу грешке. Дебаговање се користи онда када знамо (или сумњамо) да грешка постоји и желимо да је пронађемо и отклонимо.
Дебагер је алат који омогућава праћење извршавања програма корак по корак. Уместо да се програм изврши “одједном”, дебагер омогућава програмеру да заустави извршавање на одређеним местима, прати ток програма и испитује стање података (вредности променљивих, стање меморије, стање на позивном, програмском стеку, итд).
Основни појмови у раду са дебагером су:
Посматрањем ових информација програмер може да уочи где долази до неочекиваног понашања и лакше пронађе узрок грешке.
Да би се програм дебаговао, потребно је компајлирати га у дебаг режиму (нпр. у C++-у помоћу опције -g). Након тога се програм покреће у дебагеру (на пример, gdb или његов графички интерфејс kdbg).
Савремена развојна окружења, као што су Visual Studio и Visual Studio Code (Слика 1), имају уграђене дебагере који омогућавају једноставно постављање тачака прекида, праћење променљивих и контролу извршавања програма, што дебаговање чини знатно једноставнијим.
Статичко испитивање исправности програма, (тј. статичка верификација) подразумева анализу изворног кода програма (без његовог извршавања). Такве анализе могу да спроводе и људи самостално (“на папиру”), али их обично спроводе људи уз помоћ наменских алата или наменски програми, потпуно аутоматски.
Процес верификације може бити неформалан и формалан. Неформалну верификацију спроводе програмери, анализом кода, посебно неких критичних делова. Формална верификација заснива се на прецизно дефинисаној семантици програмског језика и строгом логичком оквиру у којем се докази коректности изводе. Формално доказана исправност води до највишег могућег нивоа поузданости програма. Формално доказивање исправности је обично веома захтевно, те се оно ретко примењује, обично само за безбедносно критичне програме (као што је, на пример, програм за управљање метроом).
Не постоји алгоритам који за произвољан алгоритам може да докаже да задовољава своју спецификацију (баш као што не постоји ни алгоритам који може да испита да ли се произвољни програм зауставља). Највећи проблеми у томе су заустављање и анализа петљи. Оно што јесте могуће је постојање алгоритама који у неким случајевима и са неким поједностављивањима могу да докажу исправност задатог програма.
Потпуно прецизна, формална верификација програма захтева познавање свих детаља семантике програмских језика. Један од изазова у томе представља чињеница да се семантика уобичајених типова података и операција у програмима разликује од уобичајене семантике математичких операција над целим и реалним бројевима (иако велике сличности постоје). На пример, иако тип int подсећа на скуп целих бројева, а операција сабирања два податка типа int на сабирање два цела броја, разлике су евидентне — домен типа int је коначан (фиксне “ширине”), а операција се врши “по модулу” тј. у неким случајевима долази до прекорачења. Многа правила која важе за целе бројеве не важе за податке типа int. На пример, \(x \ge 0 \wedge y \ge 0 \Rightarrow x + y \ge 0\) важи ако су \(x\) и \(y\) цели бројеви, али не важи ако су подаци типа int. У неким случајевима, приликом верификације овакве разлике се апстрахују и занемарују. Тиме се, наравно, губи потпуно прецизна карактеризација понашања програма и “докази” коректности престају да буду докази коректности у општем случају. Ипак, овим се значајно олакшава процес верификације и у већини случајева овакве апроксимације ипак могу значајно да подигну степен поузданости програма.
У наставку текста, овакве апроксимације ће бити често вршене. Дакле, у наредном тексту ће фокус бити стављен на испитивање коректности алгоритама, а не њихове конкретне имплементације која зависи од техничких детаља програмског језика у ком су они имплементирани (на пример, питања репрезентације података и прекорачења).
Кључна идеја у конструкцији алгоритама је то да је конструкција алгоритама веома тесно повезана са доказивањем теорема математичком индукцијом. Циљ овог поглавља (али и остатка ове књиге) је да покажемо да је математичка индукција основни алат за анализу свих врста програма (и итеративних и рекурзивни), али и више од тога – она је основни алат за конструкцију алгоритама. У том светлу се прецизна анализа коректности неког алгоритма не врши након што је алгоритам конструисан, већ је она присутна све време током саме конструкције алгоритма. Доказ теореме кокрекности алгоритма и сам алгоритам су нераскидиво повезани.
Математичка индукција, у свом основном облику, је следећи начин доказивања особина природних бројева. Нека је \(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\).
Основни приступ конструкције алгоритама је тзв. индуктивни тј. рекурзивни приступ. У овом приступу циљ је од решења проблема задатог облика али мање димензије добити решење тог проблема веће димензије (у напреднијим облицима је могуће и да се решава већи број проблема мање димензије). Притом, за почетне димензије проблема (које зовемо базни случајеви) решење мора да се израчуна непосредно, без даљег свођења на проблеме мање димензије. Ако се приликом свођења димензија проблема увек смањује, конструисани алгоритми ће се увек заустављати (јер димензија мора да буде ненегативна).
Имплементација алгоритма може бити таква да променљиве унутар петље итеративно ажурирају своје вредности кренувши од вредности за базне случајеве, па до крајњих вредности које представљају решења задатог проблема. Пошто је ово прилично слично принципу математичке индукције, кажемо да је алгоритам дефинисан индуктивно.
Имплементација може бити таква да функција која решава полазни проблем саму себе позива да би решила проблем истог облика, али мање димензије (осим у базним случајевима, који се непосредно решавају) и тада кажемо да је алгоритам дефинисан рекурзивно.
Индуктивна конструкција лежи у основни практично свих итеративних алгоритама које смо до сада разматрали. На пример, приказани алгоритам степеновања почива на томе да знамо да израчунамо нулти степен броја (то је 1) и да ако знамо да израчунамо \(x^k\), тада умемо да израчунамо и \(x^{k+1}\) (то радимо тако што тај познати степен \(x^k\) помножимо са \(x\)).
double stepen(double x, int n) {
double s = 1.0;
for (int i = 0; i < n; i++)
s = s * x;
return s;
}Дакле, и у овом алгоритму имамо индуктивну базу (која одговара иницијализацији променљиве пре уласка у петљу) и индуктивни корак (који одговара телу петље, у ком се ажурира вредност резултујуће променљиве, у овом случају степена). База може одговарати и случају првог (а не обавезно нултог) степена, али тада не можемо да гарантујемо да ће алгоритам исправно израчунавати нулти степен.
Рекурзивна имплементација израчунавања степена може бити следећа (у њој се приликом решавања проблема димензије \(n > 0\) експлицитно захтева решавање проблема димензије \(n-1\)).
double stepen(double x, int n) {
if (n == 0)
return 1.0;
else
return stepen(x, n-1) * x;
}Дефинисање алгоритама индуктивно-рекурзивом конструкцијом је у веома тесној вези са доказивањем њихове коректности. Иако постоје формални оквири за доказивање коректности императивних програма (пре свега Хорова логика), у овом поглављу ћемо се бавити искључиво неформалним доказима и веза између логике у којој вршимо доказивање и (императивног) програмског језика у којем се програм изражава биће прилично неформална.
Као што смо већ наговестили, приликом доказивања коректности програма обично ћемо игнорисати ограничења записа бројева у рачунару и подразумеваћемо да је опсег бројева неограничен и да се реални бројеви записују са максималном прецизношћу. Дакле, обично ћемо игнорисати грешке које могу настати услед прекорачења или поткорачења вредности током извођења аритметичких операција. Ипак, прекорачења или поткорачења могу бити узрок битних грешака у неким програмима и тада у испитивању исправности користимо богатије моделовање записа бројева.
У принципу, доказивање коректности најједноставније је за програме који су сачињени од рекурзивно дефинисаних функција које не користе елементе императивног програмирања (као што су доделе вредности променљивама, петље и слично). Такве програме зовемо функционални програми. Главни разлог за једноставније доказивање исправности оваквих програма је то што се њихове функције могу једноставно моделовати математичким функцијама (које за исте аргументе увек дају исте вредности). Наиме, у функционалним програмима функције за исте улазне аргументе такође увек враћају исту вредност. То је тако због претпоставке да нема експлицитне доделе вредности променљивама, као и да контекст позива и глобалне променљиве не утичу на извршавање функција. Доказивање коректности рекурзивних функција тече неким обликом математичке индукције.
Проблем: Дефинисати функцију која за дати природан број \(n \geq 0\) и дат реалан број \(x\) (различит од \(0\) ако је \(n=0\)) израчунава \(x^n\).
Као што смо видели, алгоритам се веома једноставно конструише индуктивно-рекурзивном конструкцијом. Димензија проблема у овом примеру је изложилац \(n\).
Рекурзивна имплементација, као што смо видели је следећа.
double stepen(double x, int n) {
if (n == 0)
return 1.0;
else
return stepen(x, n-1) * x;
}Коректност се може формулисати у облику следеће теореме (коју доказујемо занемарујући питања репрезентације бројева у рачунару).
Теорема 1.4.1. За сваки природан број \(n\geq 0\) и реалан број \(x\) (различит од 0, ако је \(n=0\)), рекурзивна функција stepen враћа вредност \(x^n\) тј. важи \(\mathit{stepen}(x, n) = x^n\).
Доказ. Теорему можемо доказати индукцијом.
Базу индукције представља случај \(n=0\), тј. позив stepen(x, 0). На основу дефиниције функције stepen резултат је \(1\), што је уједно и вредност \(x^0\) (јер је по спецификацији тада \(x \neq 0\)).
Индуктивна хипотеза је тврђење: позив stepen(x, n-1) враћа вредност \(x^{n-1}\). Из те претпоставке потребно је да докажемо да позив stepen(x, n) враћа вредност \(x^n\). На основу дефиниције функције stepen, позив stepen(x, n) ће вратити производ stepen(x, n-1) * x. На основу индуктивне хипотезе знамо да позив stepen(x, n-1) враћа \(x^{n-1}\), па је стога резултат \(x^{n-1} \cdot x\), што је управо \(x^n\). \(\Box\)
Примећујемо огромну сличност између рекурзивне конструкције алгоритма и индуктивног доказа његове коректности. Стога слободно можемо да кажемо да су рекурзија и индукција “две стране исте медаље” (индукцију користимо као технику доказивања, а рекурзију као технику дефинисања функција тј. конструкције алгоритама).
Приметимо и да овај облик коришћења математичке индукције није онај уобичејени, јер се не користи индукција непосредно по природним бројевима, већ се користи индукција по структури рекурзивне функције у којој се, из претпоставке да сваки рекурзивни позив враћа коректан резултат, доказује да функција враћа коректан резултат. Таква форма математичке индукције се може доказати на основу уобичајене индукције по броју рекурзивних позива, под претпоставком да се докаже да се рекурзивна функција увек зауставља.
Исти проблем степеновања се може решити и на следећи начин, ефикасније. Овај алгоритам познат је под називом брзо степеновање. На пример, уместо да \(2^{10}\) израчунавамо као \(2^9 \cdot 2\), брже га можемо израчунати као \((2^2)^5\). Рекурзивна дефиниција тада изгледа овако.
\[ x^n = \begin{cases} 1 & \text{ako } n = 0, \\ (x^2)^{n/2} & \text{ako je } n \text{ paran,} \\ x \cdot x^{n-1} & \text{ako je } n \text{ neparan.} \end{cases} \]
float stepen_brzo(float x, unsigned n)
{
if (n == 0)
return 1.0f;
else if (n % 2 == 0)
return stepen_brzo(x * x, n / 2);
else
return x * stepen_brzo(x, n - 1);
}Вредност \(2^{10}\) се овом функцијом израчунава на следећи начин (означимо, краткоће ради, функцију stepen_brzo sa \(s\)):
\[\begin{eqnarray*} s(2, 10) &=& s(4, 5) = 4 \cdot s(4, 4) = 4 \cdot s(16, 2) = 4 \cdot s(256, 1) =\\ &=& 4 \cdot 256 \cdot s(256, 0) = 4 \cdot 256 \cdot 1 = 1024. \end{eqnarray*}\]
Теорема 1.4.2. За сваки природан број \(n\geq 0\) и реалан број \(x\) (различит од 0, ако је \(n=0\)), рекурзивна функција stepen_brzo враћа вредност \(x^n\) тј. важи \(\mathit{stepen\_brzo}(x, n) = x^n\).
Доказ. Докажимо исправност наведене функције. Како је у овом случају функција дефинисана општом рекурзијом, доказ ће пратити следећу схему: “Да би се показало да вредност \(\mathit{stepen\_brzo}(x, n)\) задовољава неко својство, може се претпоставити да за \(n > 0\) и \(n\) парно вредност \(\mathit{stepen\_brzo}(x \cdot x, n / 2)\) задовољава то својство, као и да за \(n > 0\) и \(n\) непарно вредност \(\mathit{stepen\_brzo}(x, n-1)\) задовољава то својство, и онда тврђење треба доказати под тим претпоставкама”. Сличне схеме индукције се могу доказати и за друге функције дефинисане општом рекурзијом и, у принципу, оне дозвољавају да се приликом доказивања коректности додатно претпостави да сваки рекурзивни позив враћа коректан резултат.1
Пређимо на сâм доказ чињенице да је \(\mathit{stepen\_brzo}(x, n) = x^n\) (за ненегативну вредност \(n\)).
Случај \(n = 0\): Тада је \(\mathit{stepen\_brzo}(x, n) = \mathit{stepen\_brzo}(x, 0) = 1 = x^0\).
Случај \(n > 0\): Тада је \(n\) или паран или непаран.
Случај \(n\) је паран: Тада је \(\mathit{stepen\_brzo}(x, n) = \mathit{stepen\_brzo}(x\cdot x, n/2)\). На основу првог дела индуктивне претпоставке, \(\mathit{stepen\_brzo}(x\cdot x, n/2)\) \(= (x\cdot x)^{n/2}\). Даље, елементарним аритметичким трансформацијама следи да је \(\mathit{stepen\_brzo}(x, n) = (x\cdot x)^{n/2} = (x^2)^{n/2} = x^n\).
Случај \(n\) је непаран: Тада је \(\mathit{stepen\_brzo}(x, n) = x \cdot \mathit{stepen\_brzo}(x,n-1)\). На основу другог дела индуктивне претпоставке, \(\mathit{stepen\_brzo}(x,n-1)\) \(= x^{n-1}\). Даље, елементарним аритметичким трансформацијама следи да је \(\mathit{stepen\_brzo}(x, n) = x\cdot x^{n-1} = x^n\). \(\Box\)
У случају императивних програма (програма који садрже наредбу доделе и петље), апарат који се користи за доказивање коректности мора бити знатно сложенији. Семантику императивних конструката знатно је теже описати у односу на (једноставну једнакосну) семантику чисто функционалних програма. Све време доказивања мора се имати у виду текући контекст тј. стање програма које обухвата текуће вредности свих променљивих које се јављају у програму. Програм имплицитно представља релацију преласка између стања и доказивање коректности захтева доказивање да ће програм на крају стићи у неко стање у којем су задовољени услови задати спецификацијом. Додатну отежавајућу околност чине пропратни ефекти додела, као и чињеница да позиви функција могу да врате различите вредности за исте прослеђене улазне параметре (у зависности од глобалног контекста тј. стања у којем се позив извршио). Због тога је доказ коректности сложеног програма теже разложити на елементарне доказе коректности појединих функција.
Као најкомплекснији програмски конструкт, петље представљају један од највећих изазова у верификацији. Уместо појединачног разматрања сваког стања кроз које се пролази приликом извршавања петље, обично се формулишу услови (инваријанте петљи) који прецизно карактеришу тај скуп стања. Инваријанта петље је логичка формула која укључује вредности променљивих које се јављају у некој петљи и која важи при сваком испитивању услова петље (тј. непосредно пре, након сваког извршавања тела петље, као и непосредно након извршавања петље). Инваријанте суштински описују значење свих променљивих унутар петље. Илуструјмо појам инваријанте на примеру итеративне функције за израчунавање степена.
double stepen(double x, int n) {
double s = 1.0;
for (int i = 0; i < n; i++)
s = s * x;
return s;
}
int main() {
cout << stepen(2.0, 10) << endl;
}Суштина доказа коректности лежи у следећем разматрању. Након иницијализације променљива \(s\) садржи вредност \(1 = x^0 = x^i\). У сваком кораку петље променљива \(s\) се множи са \(x\), а вредност \(i\) увећава за 1, па и даље важи \(s=x^i\). Дакле, услов \(s=x^i\) важи и пре, и током и након извршавања петље. Пошто је након извршавања петље \(i=n\), на крају променљива \(s\) садржи вредност \(x^n\), па, пошто је та вредност повратна вредност функције, функција исправно израчунава \(x^n\).
Ову скицу доказа можемо додатно прецизирати и доказати је математичком индукцијом.
Теорема 1.4.3. У сваком кораку петље (и на њеном почетку, непосредно након провере услова, али и на њеном крају, непосредно након извршавања тела), као и након извршавања целе петље важи да је \(0 \leq i \leq n\) и да је \(s = x^i\) (где је \(i\) текућа вредност променљиве i, а \(s\) текућа вредност променљиве s).
Доказ. Ово тврђење можемо доказати индукцијом и то по броју извршавања тела петље (обележимо тај број са \(k\)). Напоменимо само да ћемо петљу for сматрати само скраћеницом за петљу while, тако да ћемо иницијализацију петље сматрати за кôд који се извршава пре петље, док ћемо корак петље сматрати као последњу наредбу тела петље.
double s = 1.0;
int i = 0;
while (i < n) {
s = s * x;
i++;
}Обележимо са \(s_0, s_1, \ldots, s_k, \ldots\) вредности променљиве s, а са \(i_0, i_1, \ldots, i_k, \ldots\) вредност променљиве i након \(0, 1, \ldots, k, \ldots\) извршавања тела петље. Пошто променљива n не мења своју вредност, њену вредност ћемо означити са \(n\).
Базу индукције чини случај \(k=0\) тј. случај када се тело петље није још извршило. Пре уласка у петљу променљива i се иницијализује на \(0\) (важи \(i_0 = 0\)). Пошто је \(n \geq 0\), важи \(0 \leq i = i_0 = 0 \leq n\). Променљива s се иницијализује на вредност \(1\) (важи \(s_0 = 1\)), па је заиста \(s_0=x^{i_0}\). Дакле, услови теореме су задовољени пре првог извршавања тела петље.
Претпоставимо сада као индуктивну хипотезу да тврђење важи након \(k\) извршавања тела петље. Дакле, претпостављамо да услови важе за вредности \(s_k\) и \(i_k\) (са \(s_k\) и \(i_k\) обележавамо вредности променљивих након \(k\) извршавања тела петље) тј. да је \(0 \leq i_k \leq n\) и да је \(s_k = x^{i_k}\). Ако је услов петље испуњен, то ће уједно бити и вредности променљивих на почетку тела петље, пре њеног \(k+1\)-вог извршавања.
Из индуктивне хипотезе и претпоставке да је услов петље i < n испуњен (тј. да је \(i_k < n\)) докажимо да након \(k+1\) извршавања тела петље услови теореме важе и за вредности \(s_{k+1}\) и \(s_{k+1}\) (са \(s_{k+1}\) и \(i_{k+1}\) обележавамо вредности променљивих након \(k+1\) извршавања тела петље). Вредности \(s_{k+1}\) и \(i_{k+1}\) се могу лако одредити на основу вредности \(s_k\) и \(i_k\), анализом једног извршавања тела петље. На основу дефиниције функције важи да је \(s_{k+1} = s_k \cdot x\) и \(i_{k+1} = i_k + 1\). Зато, пошто је \(0 \leq i_k < n\), важи и да је \(0 \leq i_{k+1} \leq n\), па је услов који се односи на распон вредности променљиве i очуван. На основу индуктивне хипотезе знамо да је \(s_k = x^{i_k}\). Зато је \(s_{k+1} =x^{i_k} \cdot x = x^{i_k+1} = x^{i_{k+1}}\).
Нека су \(i\) и \(s\) вредности променљивих i и s након извршавања петље. На основу доказаног тврђења знамо да услови наведени у њему важе и након завршетка петље. Када се петља заврши, важи да је \(i = n\) (јер на основу првог услова знамо да је \(0 \leq i \leq n\), а услов петље i < n није испуњен). На основу другог услова знамо да је \(s=x^i=x^n\).
Заустављање се доказује једноставно тако што се докаже да се у сваком кораку петље ненегативна вредност \(n-i\) смањује за по 1, док не постане 0. \(\Box\)
Ако размотримо структуру претходног разматрања, можемо установити да смо идентификовали логичке услове који су испуњени непосредно пре и непосредно након сваког извршавања тела петље. Такви услови се називају инваријанте петље. Да бисмо доказали да је неки услов инваријанта петље, довољно је да докажемо:
да тај услов важи пре првог уласка у петљу и
да из претпоставке да тај услов важи пре неког извршавања тела петље и да је услов петље испуњен докажемо да тај услов важи и након извршавања тела петље.
Те две чињенице нам, на основу индуктивног аргумента, гарантују да ће услов бити испуњен пре и после сваке итерације петље, као и након извршавања целе петље (ако се она икада заустави), тј. да ће тај услов бити инваријанта петље (тај доказ се може спровести класичном математичком индукцијом на основу броја извршавања тела петље). Приметимо да први корак одговара доказивању базе индукције, а други доказивању индуктивног корака.
Свака петља има пуно инваријанти, при чему су неки услови “преслаби” а неки “прејаки” тј. не објашњавају понашање програма. На пример, било која ваљана формула (на пример, \(x \cdot 0 = 0\) или \((x \geq y) \vee (y \geq x)\)) је увек инваријанта петље. Од интереса су нам само оне инваријанте које у комбинацији са условом прекида петље (под претпоставком да петља није прекинута наредбом break) имплицирају услов који нам је потребан након петље. Ако је петља једина у неком алгоритму, обично је то онда услов коректности самог алгоритма. Дакле, након доказа леме која чини основу доказа да је неки услов инваријанта петље, потребно је да докажемо и
Дакле, општа структура анализе програма коришћењем инваријанти се може описати на следећи начин.
<incijalizacija>
// ovde vazi <invarijanta>
while (<uslov>)
// ovde vaze i <uslov> i <invarijanta>
<telo>
// ovde vazi <invarijanta>
// ovde ne vazi <uslov>, a vazi <invarijanta>Прикажимо сада краћу верзију претходног доказа коректности функције степеновања, у ком ћемо користити појам инваријанте и нећемо се директно позивати на математичку индукцију.
Лема 1.4.1. За сваки природни број \(n \geq 0\) и реални број \(x\) (различит од \(0\) када је \(n=0\)), у сваком кораку петље важи да је \(0 \leq i \leq n\) и \(s = x^i\) (ово је једна инваријанта петље).
Доказ. Докажимо да је услов инваријанта.
Покажимо да инваријанта важи пре уласка у петљу. Пре уласка у петљу променљиве имају вредности \(s = 1\) и \(i = 0\), те инваријанта, тривијално, важи.
Покажимо да инваријанта остаје одржана након сваког извршавања тела петље. Обележимо са \(s'\) и \(s''\) и са \(i'\) и \(i''\) вредности променљивих s и i пре и после извршавања тела и корака петље. Пошто се променљиве x и n не мењају, њихове вредности обележимо са \(x\) и \(n\).
Претпоставимо да инваријанта важи при уласку у петљу тј. да важи \(s' = x^{i'}\) и \(0 \leq i' \leq n\). Пошто је услов петље испуњен, важи и \(i' < n\).
Након извршавања тела петље, променљиве имају вредности \(s'' = s' \cdot x\) и \(i'' = i' + 1\). Потребно је показати да ове нове вредности задовољавају инваријанту, тј. да важи \(s'' = x^{i''}\) и \(0 \leq i'' \leq n\). Заиста, \(s' \cdot x = x^{i'+1}\) што је тачно на основу претпоставке. Takoђе, пошто важи да је \(0 \leq i' < n\), важи и да је \(0 \leq i'' \leq n\).
Дакле, ако су \(s\), \(i\), \(n\) и \(x\) текуће вредности променљивих, тада су \(s = x^i\) и \(0 \leq i \leq n\) инваријанте петље.
\(\Box\)
Покажимо да доказана инваријанта обезбеђује коректност.
Теорема 1.4.4. На крају извршавања алгоритма важи да је \(s = x^n\).
Доказ. Када се изађе из петље, важи \(i=n\). Заиста, на основу леме знамо да важи инваријанта \(0 \leq i \leq n\), па пошто не важи услов петље \(i < n\), по изласку из петље мора да важи да је \(i = n\). Комбиновањем са инваријантом \(x = s^i\), добија се да тада важи \(s = x^n\), што је и требало доказати. \(\Box\)
Докажимо сада коректност наредне итеративне имплементације алгоритма брзог степеновања. Овакву имплементацију добијамо пратећи промену променљивих током извршавања рекурзивних позива. Новоуведена променљива \(s\) акумулира коначну вредност степена.
double stepen_brzo(double x, int n) {
double s = 1.0;
while (n > 0) {
if (n % 2 == 1) {
s *= x;
n--;
} else {
x = x * x;
n /= 2;
}
}
return s;
}Размотримо како се мењају вредности променљивих док се израчунава степен \(2^{10}\).
| \(x\) | \(n\) | \(s\) |
|---|---|---|
| 2 | 10 | 1 |
| 4 | 5 | 1 |
| 4 | 4 | 4 |
| 16 | 2 | 4 |
| 256 | 1 | 4 |
| 256 | 0 | 1024 |
Или мало општије, ако је иницијална вредност променљиве \(x\) једнака некој вредности \(c\).
| \(x\) | \(n\) | \(s\) |
|---|---|---|
| \(c\) | 10 | \(1\) |
| \(c^2\) | 5 | \(1\) |
| \(c^2\) | 4 | \(c^2\) |
| \(c^4\) | 2 | \(c^2\) |
| \(c^8\) | 1 | \(c^2\) |
| \(c^8\) | 0 | \(c^{10}\) |
Лема 1.4.2. Нека је \(n \geq 0\) и \(x \neq 0\) ако је \(n = 0\). Нека је \(n_0\) почетна вредност променљиве \(n\), а \(x_0\) променљиве \(x\). Током извршавања петље важи инваријанта да је \(n \geq 0\) и \(s \cdot x^n = x_0^{n_0}\).
Доказ. Размотримо иницијализацију и одржање инваријанте.
Након иницијализације важи да је \(x=x_0\), \(n=n_0\) и \(s=1\), па инваријанта тривијално важи.
Претпоставимо да инваријанта важи при уласку у тело петље тј. да је \(s \cdot x^n = x_0^{n_0}\). Тада важи и услов петље \(n > 0\).
Ако је \(n\) непаран број, тада је \(n' = n-1\), \(s' = s \cdot x\) и \(x'=x\) па је \(s' \cdot {x'}^{n'} = s \cdot x \cdot x^{n-1} = s \cdot x^n = x_0^{n_0}\). Пошто је \(n > 0\), važi da je \(n' \geq 0\).
Ако је \(n\) паран број, тада је \(n' = n / 2\), \(x' = x^2\) и \(s' = s\). Тада је \(s' \cdot {x'}^{n'} = s \cdot (x^2)^{n/2} = s\cdot x^n = x_0^{n_0}\). Пошто је \(n > 0\), važi da je \(n' \geq 0\).
\(\Box\)
Из ове инваријанте следи коректност.
Теорема 1.4.5. Нека је \(n \geq 0\) и \(x \neq 0\) ако је \(n = 0\). Тада је \(\mathit{stepen\_brzo}(x, n) = x^n\).
Доказ. Када се петља заврши важи инваријанта \(n \geq 0\), \(s \cdot x^n = x_0^{n_0}\), а услов петље \(n > 0\) није испуњен. Зато је \(n = 0\), па важи \(s \cdot x^0 = x_0^{n_0}\) тј. \(s = x_0^{n_0}\). Дакле, повратна вредност функције садржана у променљивој \(s\) је управо једнака степену \(x^n\), за задате почетне вредности променљивих \(x\) и \(n\). \(\Box\)
За вежбу покажите и да је наредна, мало једноставнија имплементација такође коректна.
double stepen_brzo(double x, int n) {
double s = 1.0;
while (n > 0) {
if (n % 2 == 1)
s *= x;
x *= x;
n /= 2;
}
return s;
}Још неколико примера овако прецизних доказа коректности дато је у додатку @sec:primeri_dokaza. У наставку овог поглавља видећемо још неколико примера примене технике инваријанте петље. Мора се признати да када се техника користи потпуно формално, да би се доказала коректност већ написаног програмског кода, то не делује нарочито инспиришуће (поготово, ако су програми једноставни и ако је једноставно интуитивно разумети разлоге њихове коректности). Ретко када се у практичном програмирању коректност заиста доказује потпуно формално (осим у случају софтвера који може да угрози велики број живота, попут, на пример, софтвера који управља метро-системом у Паризу, који јесте у потпуности формално верификован). Међутим, аргументе и инваријанте на којима коректност почива програмер често “проврти по глави”. Видећемо и да се техника инваријанти може употребити и пре него што је програм написан у циљу извођења програмског кода из спецификације. Јасне инваријанте често једнозначно указују на то како програмски кôд треба да изгледа и на тај начин помажу у процесу програмирања.
Написати програм који учитава низ целих бројева а затим га трансформише тако да елементи буду подељени у три дела у зависности од задатих вредности \(A\) и \(B\). У првом делу су елементи мањи од задате вредности \(A\) (вредности из интервала \([-\infty, A)\)), у другом елементи већи или једнаки задатој вредности \(A\) и мањи или једнаки задатој вредности \(B\) (вредности из интервала \([A, B]\)), а у трећем елементи већи од задате вредности \(B\) (вредности из интервала \((B, +\infty)\)). Није битно у ком се редоследу налазе елементи унутар делова. Учитати елементе у низ, а затим реорганизовати редослед елемената у том низу (не користити помоћне низове).
У једној линији стандардног улаза налази се број елемената низа, \(N\), а затим се, у наредној линији налазе елементи низа раздвојени размацима. У последње две линије се налазе цели бројеви \(A\) и \(B\) одвојени празнином, и при томе је \(A < B\).
Исписати елементе резултујућег низа на стандардни излаз (могуће је исписати елементе сваке од три групе у посебном реду, раздвојене размацима, а могуће је исписати и цео низ у једном реду или у више редова).
10 1 3 5 4 8 5 7 2 3 6 3 5
1 2 5 4 3 5 3 7 6 8
Један приступ је да се до решења дође у две фазе. У првој фази би се на почетак низа довели сви елементи који су мањи од броја \(A\), а иза њих би се поставили сви елементи који су већи или једнаки броју \(A\). Након тога, у другој фази обрађује се само део низа, и он се поново истим поступком дели на елементе који су мањи или једнаки од броја \(B\) (то ће бити тачно елементи из интервала \([A, B]\)) и елементе који су већи од \(B\). Поделу можемо реализовати засебном функцијом, која прима део низа који се реорганизује и границу на основу које се врши подела, а која враћа позицију на којој почиње други део реорганизованог низа.
Задатак можемо решити помоћу само једног пролаза кроз низ и то “у месту” тј. без коришћења помоћног низа. Алгоритам у наставку познат је под називом “Холандска застава тробојка” (енгл. Dutch national flag, слика 2) и приписује се чувеном информатичару Дајкстри (енгл. Edsger W. Dijkstra).
Одржаваћемо три променљиве l, d и i и током петље наметнућемо следеће услове који ће бити инваријанте петље. Претпостававићемо да текуће вредности \(l\), \(d\) и \(i\) ових променљивих задовољавају \(0 \leq l \leq i \leq d \leq n\) и да важи:
Дакле, одржавамо распоред <<<<===???>>>, где су са < обележени елементи прве групе, са = елементи друге, са ? елементи треће групе, а са > елементи четврте групе.
Да би инваријанта важила пре уласка у петљу, јасно је да мора да важи да је \(i = 0\) и \(d=n\) (јер су сви елементи из интервала \([i, d) = [0, n)\) неиспитани). Такође, да бисмо били сигурни да су у интервалу \([0, l)\) сви елементи мањи од \(A\), тај интервал мора бити празан и мора да важи да је \(l=0\). Након овакве иницијализације и интервал \([l, i) = [0, 0)\) и интервал \([d, n) = [n, n)\) је празан, па задовољава наметнути услов.
Петља ће се извршавати док год има неиспитаних елемената, а то је док је \(i < d\). Размотримо како треба да изгледа тело петље, да би услови били одржани.
На крају петље важи да је \(i=d\). Уз остале наметнуте услове тврђење одатле следи (елементи из интервала позиција \([0, l)\) су мањи од \(A\), елементи из интервала позиција \([l, i) = [l, d)\) су између \(A\) и \(B\), интервал непрегледаних елемената \([i, d)\) је празан, док су елементи из интервала \([d, n)\) већи од \(B\)). Дакле, низ је разбијен на надовезане сегменте \([0, l)\), \([l, d)\) и \([d, n)\) и у сваком сегменту се налазе одговарајући елементи.
// funkcija organizuje elemente vektora u tri dela:
// prvo elementi iz intervala (-Inf, A), zatim
// elementi iz intervala [A, B] i na kraju
// elementi iz intervala (B, Inf)
void podelaNiza(vector<int>& niz, int A, int B) {
// - na pozicijama [0, l) su elementi iz intervala (-Inf, A)
// - na pozicijama [l, i) su elementi iz intervala [A, B]
// - na pozicijama [i, d) su jos neispitani elementi
// - na pozicijama [d, n) su elementi iz intervala (B, Inf)
int l = 0, i = 0, d = niz.size();
// dok god postoje neispitani elementi
while (i < d) {
if (niz[i] < A)
// menjamo tekuci element sa prvim elementom iz [A, B]
swap (niz[i++], niz[l++]);
else if (niz[i] <= B)
// tekuci element ostaje na svom mestu
i++;
else
// menjamo tekuci element sa poslednjim neispitanim
swap(niz[i], niz[--d]);
}
}#include <iostream>
#include <vector>
#include <algorithm>
using namespace std;
// funkcija ucitava elemente u vektor
vector<int> unosNiza() {
int n;
cin >> n;
vector<int> a(n);
for (int i = 0; i < n; i++)
cin >> a[i];
return a;
}
// funkcija organizuje elemente vektora u tri dela:
// prvo elementi iz intervala (-Inf, A), zatim
// elementi iz intervala [A, B] i na kraju
// elementi iz intervala (B, Inf)
void podelaNiza(vector<int>& niz, int A, int B) {
// - na pozicijama [0, l) su elementi iz intervala (-Inf, A)
// - na pozicijama [l, i) su elementi iz intervala [A, B]
// - na pozicijama [i, d) su jos neispitani elementi
// - na pozicijama [d, n) su elementi iz intervala (B, Inf)
int l = 0, i = 0, d = niz.size();
// dok god postoje neispitani elementi
while (i < d) {
if (niz[i] < A)
// menjamo tekuci element sa prvim elementom iz [A, B]
swap (niz[i++], niz[l++]);
else if (niz[i] <= B)
// tekuci element ostaje na svom mestu
i++;
else
// menjamo tekuci element sa poslednjim neispitanim
swap(niz[i], niz[--d]);
}
}
// ispis elemenata vektora na standardni izlaz
void ispisNiza(const vector<int>& a, int A, int B) {
int i = 0;
// ispisujemo elemente iz intervala (-Inf, A)
while (i < a.size() && a[i] < A)
cout << a[i++] << " ";
cout << endl;
// ispisujemo elemente iz intervala [A, B]
while (i < a.size() && a[i] <= B)
cout << a[i++] << " ";
cout << endl;
// ispisujemo elemente iz intervala (B, +Inf)
while (i < a.size())
cout << a[i++] << " ";
cout << endl;
}
int main() {
// ucitavamo elemente niza
vector<int> a = unosNiza();
// ucitavamo interval [A, B]
int A, B;
cin >> A >> B;
// reorganizujemo elemente po intervalima (-inf, A), [A, B] i [B, inf)
podelaNiza(a, A, B);
// ispisujemo elemente niza
ispisNiza(a, A, B);
return 0;
}Пример 1.4.1. Размотримо рад алгоритма на једном примеру. Нека је \(A=4\), \(B=7\) и нека низ има садржај 5 1 8 6 3 9 4 2. У наставку ћемо приказати стање низа током извођења алгоритма.
Након иницијализације променљивих стање је следеће.
| l | d | |||||||
| 5 | 1 | 8 | 6 | 3 | 9 | 4 | 2 | |
| i |
Елемент \(5\) на позицији \(i\) припада интервалу \([A, B]\), па се само увећава показивач \(i\).
| l | d | |||||||
| 5 | 1 | 8 | 6 | 3 | 9 | 4 | 2 | |
| i |
Елемент \(1\) на позицији \(i\) припада интервалу \((-\infty, A)\), па се размењује са елементом \(5\) на позицији \(l\) и оба показивача \(i\) и \(l\) се увећавју.
| l | d | |||||||
| 1 | 5 | 8 | 6 | 3 | 9 | 4 | 2 | |
| i |
Елемент \(8\) на позицији \(i\) припада интервалу \((B, +\infty)\), па се мења са првим елементом испред позиције \(d\) (што је елемент \(2\)) и показивач \(d\) се умањује.
| l | d | ||||||
| 1 | 5 | 2 | 6 | 3 | 9 | 4 | 8 |
| i |
Елемент \(2\) на позицији \(i\) припада интервалу \((-\infty, A)\), па се размењује са елементом \(5\) на позицији \(l\) и оба показивача \(i\) и \(l\) се увећавју.
| l | d | ||||||
| 1 | 2 | 5 | 6 | 3 | 9 | 4 | 8 |
| i |
Елемент \(6\) на позицији \(i\) припада интервалу \([A, B]\), па се само увећава показивач \(i\).
| l | d | ||||||
| 1 | 2 | 5 | 6 | 3 | 9 | 4 | 8 |
| i |
Елемент \(3\) на позицији \(i\) припада интервалу \((-\infty, A)\), па се размењује са елементом \(5\) на позицији \(l\) и оба показивача \(i\) и \(l\) се увећавју.
| l | d | ||||||
| 1 | 2 | 3 | 6 | 5 | 9 | 4 | 8 |
| i |
Елемент \(9\) на позицији \(i\) припада интервалу \((B, +\infty)\), па се мења са првим елементом испред позиције \(d\) (што је елемент \(4\)) и показивач \(d\) се умањује.
| l | d | ||||||
| 1 | 2 | 3 | 6 | 5 | 4 | 9 | 8 |
| i |
Елемент \(4\) на позицији \(i\) припада интервалу \([A, B]\), па се само увећава показивач \(i\).
| l | d | ||||||
| 1 | 2 | 3 | 6 | 5 | 4 | 9 | 8 |
| i |
Пошто \(i\) достиже вредност \(d\), алгоритам се завршава. Елементи на позицијама \([l, d)\) су из интервала \([A, B]\), лево од њих су мањи елементи, а десно већи.
U narednom apletu možete proveriti svoje razumevanje ovog algoritma.
✖
Уз теразије стоји скуп тегова целобројних маса. Одредити која је најмања целобројна маса која се не може измерити помоћу тих тегова (сваки тег се може употребити само једном).
Напомена: маса тела се уз помоћ теразија мери тако што се на један тас стави то тело, а на други тегови које имамо на располагању, тако да теразије буду у равнотежи.
Са стандардног улаза се учитава број \(n\) (\(1 \leq n \leq 10^3\)), а затим у наредном реду сортиран низ од \(n\) природних бројева мањих од \(10^4\), који представљају скуп маса тегова.
На стандардни излаз исписати тражени најмањи природан број који није збир неких елемената тог скупа.
8 1 2 4 7 15 32 35 48
30
Помоћу тегова масе \(m_0, \ldots, m_i\) сигурно не можемо да измеримо масе веће од \(Z_i = m_0 + \ldots + m_i\). Питање је да ли можемо измерити све масе из интервала \([0, Z_i]\).
Чињеница да су елементи сортирани олакшава решење задатка. Обрађиваћемо елемент по елемент и приликом додавања сваког новог тега масе \(m_i\) провераваћемо да ли у интервалу \([0, Z_i]\) постоји нека маса која се не може измерити или на снази остаје инваријанта да је могуће измерити све масе из \([0, Z_i]\).
Претпоставимо да се теговима \(m_0, \ldots, m_{i}\) могла измерити свака маса из интервала \([0, Z_{i}]\). Тада се додавањем тега \(m_{i+1}\) може измерити свака маса из интервала \([0 + m_{i+1}, Z_{i} + m_{i+1}] = [m_{i+1}, Z_{i+1}]\) (додавањем тега \(m_{i+1}\) на претходно одабране тегове). Ако је нови учитани елемент \(m_{i+1} > Z_i + 1\), онда се \(Z_i + 1\) не може измерити (јер је низ сортиран, па су масе свих преосталих тегова веће или једнаке \(m_{i+1}\)), и то је тражена вредност. У супротном, унија интервала \([0, Z_i] \cup [m_{i+1}, Z_{i+1}]\) покрива интервал \([0, Z_{i+1}]\), па се све масе из тог интервала могу измерити и инваријанта остаје на снази.
Пример 1.4.2. На пример, нека је дат низ \(1, 2, 3, 5, 14, 20, 27\).
int n;
cin >> n;
// invarijanta: sabiranjem elemenata trenutnog obradjenog
// skupa tegova mogu se dobiti sve mase iz intervala [0, zbir]
int zbir = 0;
for (int i = 0; i < n; i++) {
int m; cin >> m;
if (m > zbir + 1)
break;
zbir += m;
}
cout << zbir + 1 << endl;#include <iostream>
using namespace std;
int main() {
int n;
cin >> n;
// invarijanta: sabiranjem elemenata trenutnog obradjenog
// skupa tegova mogu se dobiti sve mase iz intervala [0, zbir]
int zbir = 0;
for (int i = 0; i < n; i++) {
int m; cin >> m;
if (m > zbir + 1)
break;
zbir += m;
}
cout << zbir + 1 << endl;
return 0;
}Докажимо коректност овог алгоритма.
Лема 1.4.3. Нека је \(Z\) текућа вредност променљиве zbir. Инваријанта петље је да је \(0 \leq i \leq n\), да је \(Z\) збир првих \(i\) елемената низа и да се сваки број из интервала \([0, Z]\) може добити као збир неког подскупа првих \(i\) елемената низа.
Доказ. Пре уласка у петљу је \(i=0\) и \(Z=0\). Збир првих \(i=0\) елемената низа је по дефиницији нула (тј. \(Z\)). Број \(0\) је једини елемент интервала \([0, Z] = [0, 0]\) и он се може добити као збир празног подскупа (тј. 0 елемената полазног низа).
Обележимо са \(Z\) и \(i\) вредности променљивих zbir и i пре уласка у петљу, а са \(Z'\) и \(i'\) вредности након извршавања тела и корака петље. Претпоставимо да инваријанта важи пре уласка у петљу.
Ако је \(m_i > Z+1\), тврдимо да је \(Z+1\) тражени најмањи број. На основу инваријанте знамо да су сви бројеви из интервала \([0, Z]\) покривени, тако да мањи број од \(Z+1\) не може бити решење. Докажимо да број \(Z+1\) не може бити збир неког подскупа тегова. Пошто је низ сортиран, важи \(Z+1 < m_i \leq m_{i+1} \leq \ldots \leq m_{n-1}\). Дакле, ни један од тих елемената не сме бити укључен у подскуп јер би њиховим укључивањем збир већ премашио \(Z+1\). Подскуп се мора састојати само од елемената \(m_0\) до \(m_{i-1}\), међутим, пошто је \(Z\) њихов збир, збир сваког њиховог подскупа је мањи или једнак \(Z\). Дакле, \(Z+1\) се не може измерити и он је тражено решење.
Ако је \(m_i \leq Z+1\), тада је \(Z' = Z + m_i\), \(i' = i + 1\) и тврдимо да је \(Z'\) збир свих елемената \(m_0\), …, \(m_i\) и да се сваки број из интервала \([0, Z']\) може представити као збир неког подскупа првих \(i'\) елемената низа. Прва тврдња је прилично очигледна, јер је по претпоставци \(Z\) збир свих елемената \(m_0\), …, \(m_{i-1}\), а \(Z' = Z+m_i\). На основу претпоставке знамо да сви бројеви из \([0, Z]\) могу бити збирови подскупова првих \(i\) елемената низа. Слично и сви бројеви из интервала \([m_i + 0, m_i + Z]\) се могу добити као збир неког подскупа првих \(i' = i+1\) елемента низа. Наиме, тај подскуп ће бити унија елемента \(m_i\) и оног подскупа првих \(i\) елемената низа чији је збир једнак разлици између тог броја и броја \(m_i\) — он је из интервала \([0, Z]\), па на основу претпоставке такав подскуп постоји. Пошто је \(m_i \leq Z + 1\) унија интервала \([0, Z]\) и \([m_i, m_i+Z]\) је \([0, m_i+Z] = [0, Z']\). Зато је сваки елемент из \([0, Z']\) једнак збиру неког подскупа првих \(i'\) елемената низа, па инваријанта остаје очувана. \(\Box\)
Теорема 1.4.6. Када се програм заврши, вредност \(Z+1\) је најмањи природни број који се не може представити као збир унетих бројева.
Доказ. Случај када се петља заврши прекидом, јер је \(m_i > Z+1\) је већ размотрен. Када се петља заврши, важи да је \(i = n\). На основу инваријанте \(Z\) је збир свих елемената низа, и сваки број из \([0, Z]\) јесте збир неког подскупа првих \(i=n\) елемената низа, тј. целог низа. Зато је \(Z+1\) најмањи елемент који није могуће добити (јер се укључивањем свих елемената добија највише \(Z\)) и приказано решење је исправно. \(\Box\)
У наредном аплету можете видети како овај алгоритам функционише.
✖
Не постоји општи поступак којим се за произвољни задати програм може утврдити да ли се он зауставља за задате вредности аргумената2. Ипак, за многе конкретне програме, може се утврдити да ли се заустављају или не. Како не постоји општи поступак који би се применио на све програме, заустављање сваког програма мора се испитивати засебно и користећи специфичности тог програма.
У програмима у којима су петље једине наредбе које могу довести до незаустављања потребно је доказати заустављање сваке појединачне петље. Ово се обично ради тако што се дефинише добро заснована релација3 таква да су суседна стања кроз које се пролази током извршавања петље међусобно у релацији. Код елементарних алгоритама ово се обично ради тако што се изврши неко пресликавање скупа стања у скуп природних бројева и покаже да се свако суседно стање пресликава у мањи природан број.4 Пошто је релација \(>\) на скупу природних бројева добро заснована, и овако дефинисана релација на скупу стања биће добро заснована. Величина која се мења (смањује) током извршавања петље назива се варијанта петље.
Размотримо неколико примера.
Итеративни алгоритам који врши степеновање узастопним множењем се зауставља. Заиста, у сваком кораку петље вредност \(n-i\) је природан број (јер инваријанта каже да је \(0 \leq i \leq n\)). Ова вредност опада кроз сваки корак петље (јер се \(n\) не мења, а \(i\) расте), па у једном тренутку мора да достигне вредност \(0\).
Рекурзивна функција која врши брзо степеновање се зауставља. Заиста, у свакон наредном рекурзивном позиву вредност \(n\) је строго мања од тренутне. Заиста, рекурзивни позиви се врше само када је \(n > 0\). Ако је \(n\) парно, вредност \(n/2\) је строго мања од \(n\) (јер је тада \(n \geq 2\)), а ако је непарна, вредност \(n-1\) је строго мања од \(n\). Пошто је \(n\) природан број он мора у неком тренутку достићи вредност \(0\), када се излази из рекурзије.
Није познато да ли се наредна функција зауставља за произвољну улазну вредност \(n\).5
void f(unsigned n)
{
while (n > 1) {
if (n % 2)
n = 3*n+1;
else
n = n/2;
}
}Опште уверење је да се функција зауставља за сваку улазну вредност \(n\) (то тврди још увек непотврђена Колацова (Collatz) хипотеза из 1937). Наведени пример показује како питање заустављања чак и за неке веома једноставне програме може да буде екстремно компликовано.
Сва досадашња разматрања о коректности програма вршена су заправо полуформално, тј. није постојао прецизно описан формални систем у којем се врши доказивање коректности императивних програма. Један од најзначајнијих формалних система овог типа описао је Тони Хор (енгл. Tony Hoare).
Семантика одређеног програмског кода може се записати тројком облика
\[\{\varphi\} {\texttt P} \{\psi\}\]
где је P низ наредби, а \(\{\varphi\}\) и \(\{\psi\}\) су логичке формуле које описују везе између променљивих које се јављају у тим наредбама. Тројку \((\varphi, {\texttt P}, \psi)\) називамо Хорова тројка. Интерпретација тројке је следећа: “Ако извршење низа наредби P почиње са вредностима улазних променљивих (у стању) које задовољавају услов \(\{ \varphi \}\) и ако P заврши рад у коначном броју корака, тада вредности програмских променљивих (стање) задовољавају услов \(\{ \psi \}\)”. Услов \(\{ \varphi \}\) назива се предуслов, а услов \(\{ \psi \}\) назива се постуслов (послеуслов).
На пример, тројка \(\{x=1\}\)y:=x\(\{y=1\}\)6, описује дејство наредбе доделе и каже да, ако је вредност променљиве \(x\) била једнака \(1\) пре извршавања наредбе доделе, и ако се наредба доделе изврши, тада ће вредност променљиве \(y\) бити једнака \(1\). Ова тројка је тачна. С друге стране, тројка \(\{x=1\}\)y:=x\(\{y=2\}\) говори да ће након доделе вредност променљиве \(y\) бити једнака \(2\) и она није тачна. Спецификација програма се може задати у облику Хорове тројке. На пример, спецификација функције степеновања се може задати у следећем облику:
\[\{n \geq 0 \wedge (n = 0 \Rightarrow x \neq 0)\}\texttt{s := stepen(x, n)}\{s = x^n\}\]
Хоровом логиком се дефинишу правила којима се од једноставнијих Хорових тројки изводе сложеније. Опис ових правила и пример њихове примене на доказ коректности функције степеновања дати су у поглављу @sec:hoare.
Формални докази (у јасно прецизираном логичком оквиру) су важни јер могу да се генеришу аутоматски уз помоћ рачунара или барем интерактивно у сарадњи човека са рачунаром. У оба случаја, формални доказ може да се провери аутоматски (док аутоматска провера неформалног доказа није могућа). Софтвер чија је исправност доказана и проверена аутоматски од стране наменских програма је најпоузданији софтвер и захтеви за таквим нивоом поузданости постављају се за неке безбедносно критичне апликације (као што је, на пример, контролни софтвер за метро).
Када се програм и доказ његове коректности истовремено развијају, програмер боље разуме сам програм и његова својства. Методологија формалног испитивања исправности утиче и на прецизност, конзистентност и комплетност спецификације, на јасноћу имплементације и склад имплементације и спецификације. Захваљујући томе добија се поузданији софтвер, чак и онда када се формални доказ не изведе експлицитно.
Ова теорема се може доказати и принципом јаке индукције за природне бројеве, у ком се из индуктивне претпоставке да сви бројеви мањи или једнаки \(k\) имају неко својство доказује да и број \(k+1\) има то својство. Међутим, принцип индукције који прати дефиницију рекурзивне функције је општији, јер се може применити и на функције чији аргументи нису природни бројеви или јесу природни бројеви, али се не смањују монотоно током рекурзивних позива. Стога ћемо у свим доказима користити овај општији принцип, који важи за све рекурзивне функције које се заустављају за све вредности својих аргумената.↩︎
Ово је чувени халтинг-проблем чију је неодлучивост први доказао Алан Тјуринг.↩︎
За релацију \(\succ\) се каже да је добро заснована (енгл. well founded) ако не постоји бесконачан опадајући ланац елемената \(a_1 \succ a_2 \succ \ldots\).↩︎
Сматрамо да и нула припада скупу природних бројева.↩︎
Пошто је опсег типа unsigned ограничен, у овом конкретном примеру се могу тестирати све могуће вредности за \(n\), међутим, у општем случају, ако размотримо било који могући природан број \(n\), тада је заустављање непознато.↩︎
Приликом описа Хорове логике, уместо C-овске, биће коришћена синтакса слична синтакси коришћеној у оригиналном Хоровом раду, где се додела уместо оператором = означава оператором :=.↩︎