Správnosť algoritmov^Korektnosť ^ ^ Správnost: algoritmov Korektnost: Fo IB110 Podzim 2010 l Správnosť algoritmov^Korektnost ^ ^ Prečo? ■ 1962, Marinerl - start rakety ■ 1981, Kanada - informácia o volebných preferenciách ■ 1985-87, Therac-25 - nespravne davky rontgenoveho žiarenia ■ probiem Y2K ■ http://www.devtopics.com/20-famous-software-disasters/ IB110 Podzim 2010 2 Správnosť algoritmov^Korektnosť ^ ^ Typy chýb ■ syntaktické chyby ■ until / untli m for (k=0;k<101){ sum = sum + k } versus for (k=0;k<101;k=k+1){ sum = sum + k } ■ sémantické chyby ■ výsledná hodnota premennej cyklu m for (k=0;k=k+1;k<101){ sum = sum + k } versus for (k=0;k<101;k=k+1){ sum = sum + k } ■ logické chyby pre daný text zisti, kol'ko viet obsahuje slovo kniha ■ koniec vety indikuje výskyt symbolov ,,. " (bodka, medzera) ■ koniec vety indikuje výskyt symbolu „. " (bodka) poatace nerobia chyby IB110 Podzim 2010 3 Správnosť algoritmov^Korektnosť ^ ^ Testovanie a ladenie syntaktické chyby, run-time chyby testovanie, testovacie sady ladenie nezarucujú bezchybnost; algoritmu IB110 Podzim 2010 4 Správnosť algoritmov^Korektnosť ^ ^ Čiastočná a úplná korektnost: 2pecifikácia algoritmického problému 1. urCenie množiny vstupných inštancií 2. urcenie vžtahu medži vstupnými inštanciami a požadovaným výstupom. ■ ciastocna korektnost!: pre každu vstupnu inštanciu X platí, že ak výpocet algoritmu na X skoncí, tak výstup ma požadovanu vlastnost! ■ konecnost: výpocet skoncí pre každu vstupnu instanciu ■ uplna koreknost: ciastocna korektnost! + konecnost IB110 Podzim 2010 5 Správnosť algoritmov^Korektnosť ^ ^ Dokaz korektnosti invarianty ■ kontrolne body programu invariant = tvrdenie, ktore platí pri kaZdom priechode kontrolnúym bodom ■ ciastocnú korektnost; konvergencia ■ s kontrolnymi bodmi asociujeme kvantitatívnu vlastnost; ■ pri kaZdom priechode kontrolním bodom sa hodnota kvantitatívnej vlastnostni zniZuje ■ hodnota kvantitatívnej vlastnosi nesmie prekroát dolnú hranicu ■ konecnost vypoctu IB110 Podzim 2010 6 Správnosť algoritmov^Korektnosť ^ Príklady ^ Zrkadlový obraz Zrkadlový obraz : reťazec S i: symboly reťazca S v obráťenom poradí Noťacia ■ reverse(„fakulťa") = '„aťlukaf" ■ head(„fakulťa") = „f" ■ tail(„fakulťa") = „akulťa" symbol A oznaCuje prazdny reťazec (reťazec neobsahuje Žiaden symbol) ■ symbol • oznacuje zreťazenie (spojenie) dvoch reťazcov IB110 Podzim 2010 7 Správnosť algoritmov^Korektnosť ^ Príklady ^ Zrkadlový obraz Algoritmus X <- S: Y<- A 1 ' V X<-tail(Z) IB110 Podzim 2010 8 Správnosť algoritmov^Korektnosť ^ Príklady ^ Zrkadlový obraz Kontrolné body a invarianty Invariant 1 vstupná podmienka Invariant 2 S = révérsé( Y) • X charakterizuje výpočet Invariant 3 Y = révérsé(S) poZadovaný vztah medzi vstupom S a váýstupom Y IB110 Podzim 2010 9 Správnosť algoritmov^Korektnosť ^ Príklady ^ Zrkadlový obraz Platnost: invariantov dokazujeme, že pre každý platný vstup: ak výpočet dosiahne kontrolný bod, tak tvrdenie je pravdive v akom poradí sa prechýdzajý kontrolne bodý? 1 —> 2 —> 2 —► ..-2 —> 3 IB110 Podzim 2010 10 Správnosť algoritmov^Korektnosť ^ Príklady ^ Zrkadlový obraz Platnosť invariantov 2 pre každý reťazec S po vykonaní príkazov X — S, Y — A platí rovnosť! S = reverse( Y) • X 2 —► 3 ak S = reverse( Y) • X a X = A, ťak Y = reverse(S) ak S = reverse(Y) • X a X = A, tak po vykonaní príkazov Y — head(X) • Y; X — tail(X) plať í znovu ta ista rovnosť! pre nove hodnoty premenných X aY dokazali sme CiastoCnU korektnost! IB110 Podzim 2010 11 Správnosť algoritmov^Korektnosť ^ Príklady ^ Zrkadlový obraz Konečnost: ■ výpočet algoritmu je nekonečný prave ak prechádza kontrolným bodom 2 nekonečne vel'a krat ■ s kontrolným bodom 2 asociujeme kvantitatívnu vlastnost! (tzv. konvergent) a ukáZeme, Ze jej hodnota klesá a pritom je zdola ohraničena ■ konvergentom pre kontrolný bod 2 je dlZka retazca X ■ pri kazdom priechode kontrolným bodom 2 dlzka retazca X klesne o 1 ■ ak dlzka X klesne na 0 (X je prazdný retazec), tak výpocet neprechádza cýklom a nenavstívi kontrolný bod 2 dokazali sme konecnost IB110 Podzim 2010 12 Správnost: algoritmov^Korektnosť ^ Príklady ^ Zrkadlový obraz Korektnost: korektnosť = ciastocna korektnosť + konecnost IB110 Podzim 2010 13 Správnosť algoritmov^Korektnosť ^ Príklady ^ Euklidov algoritmus Euklidov algoritmus Vstup dve kladné celé čísla X a Y Výstup najvaCSí spoločný deliteľ Z čísel X a Y spoločný deliteľ Z Z delí X a Z delí Y (celočíselne) najvacsí deliteľ pre kazde číslo U > Z, bud' U nedelí X alebo U nedelí Y IB110 Podzim 2010 14 Správnosť algoritmov^Korektnosť ^ Príklady ^ Euklidov algoritmus Implementácia function Euclid (X, Y) V — X W — Y while V = W do if V > W then V — V - W fi if V < W then V — W - V fi od return (V) Invariant 1 V a W sú násobkom Z Invariant 2 V > Z a W > Z Invariant 3 neexistuje väčší spoločný deliteľ čísel V a W nez číslo Z vSetky invariatný platia v každom bode výpočtu IB110 Podzim 2010 15 Správnosť algoritmov^Korektnosť ^ Príklady ^ Euklidov algoritmus Ciastocna korektnost Invariant 1 V a W sU nasobkom Z Invariant 2 V > Z a W > Z Invariant 3 neexistuje väčSí spoločný deliteľ čísel V a W neZ číslo Z Inicializacia V ^ X, W ^ Y ■ invarianty 1, 2, 3 sa priradením neporusia IF príkaz if V > W thén V <- V - W i ■ Fakt Ak V > W, tak dvojice čísel V, W a V - W, W maju rovnakých spoločných delitel'ov ak Z delí V, W a V > W, tak V - W > 0a V - W > Z ■ invariantý 1, 2, 3 zostavaju zachovane IF príkaz if W > V thén W <- W - V i ■ sýmetrický IB110 Podzim 2010 16 Spravnost algoritmov^Korektnosť ^ Príklady ^ Euklidov algoritmus Ciastocna korektnost Invariant 1 V a W sU nasobkom Z Invariant 2 V > Z a W > Z Invariant 3 neexistuje väCs í spoloCný deliteľ C ísel V a W nez C íslo Z while príkaz ■ vsetky invarianty zostavajU v platnosti po preveden í jednotlivyCh pr íkazov Cyklu ■ Cyklus konC í ked' V = W V je najvaCsím spoloCnym delitel'om V, W ■ V = Z CiastoCna korektnost! IB110 Podzim 2010 17 Správnost: algoritmov^Korektnosť ^ Príklady ^ Euklidov algoritmus Konečnosť ■ vypocet je nekonecny prave ak while príkaz sa vykona nekonecne vel;a krat ■ konvergentom while cyklu je sucet V + W ■ pri kazdom vstupe do tela cyklu je V > Z > 0, W > Z > 0 a V=W i pri vykonaní tela cyklu sa odcíta cele kladne císlo bud' od V alebo od W ■ suma V + W sa pri kazdom priechode cyklom znízi aspoň o 1 na zaciatku je V + W = X + Y a preto sa cyklus vykona nanajvýš X + Y kra't konecnost IB110 Podzim 2010 18 Správnosť algoritmov^Korektnosť ^ Príklady ^ Insertsort Triedenie vkladaním Insertion — Sort (A) for j — 2 to length[A] do key — A[j] i — j — 1 while i > 0 A A[i] > key do A[i + 1] — A[i] i — i — 1 od A[i + 1] — key od Invariant na začiatku iteracie for cyklu obsahuje A[1... j — 1] tie isté prvky, ako obsahovalo na tychto pozíciach pole A na začiatku vypočtu, ale utriedene od najmenšieho po najvacsí IB110 Podzim 2010 19 Spravnost algoritmov^Korektnosť ^ Príklady ^ Insertsort Čiastočná korektnost: a konečnost: Invariant na žaáatku iteracie for cýklu obsahuje A[1... j — 1] tie iste prvký, ako obsahovalo na týchto pož íciach pole A na žaciatku výpoctu, ale utriedene od najmensieho po najvacsí Inicialižacia tvrdenie platí na žaciatku výpoctu (j = 2, postupnost! A[1] obsahuje jediný prvok a je utriedena) FOR cýklus v tele cýklu sa hodnotý A[j — 1], A[j — 2], A[j — 3],... posuvaju o jednu pož íciu doprava až kým sa nenajde vhodna pož ícia pre A[j ] Ukoncenie for cýklus sa ukonc í keď j = n + 1. Substituciou n + 1 ža j dostavame, že pole A[+... n obsahuje tie iste prvký, ako na žaciatku výpoctu, ale utriedene. Konecnost for cýklus nemen í hodnotu riadiacej premennej cýklu IB110 Podzim 2010 20 Správnosť algoritmov;>Formálna verifikácia !3> ^ Správnost: algoritmov K Formálna verifikácia IB110 Podzim 2010 21 Správnosť algoritmov;>Formálna verifikácia !3> ^ Formálna verifikácia ■ interaktívne dokazovanie ■ dokazovanie formálnym odvodením (theorem proving) m overovanie modelu (model checking) IB110 Podzim 2010 22