## Naloge za ogrevanje - Kako *deluje* logična implikacija $\implies$? - (Komentar) Dokazujemo, da iz izjave $A$ sledi izjava $D$. Pri tem si pomagamo z vmesnimi izjavami $B$ in $C$. Zapisali smo $A \implies B \implies C \implies D$. V tem zapisu ne mislimo na $A \implies (B \implies (C \implies D))$ ampak na $A \implies B \wedge B \implies C \wedge C \implies D$. - Dokaži, da velja: $\forall x,y\in \mathbb{Z}:\ x < y \implies x \leq y$. Poišči proti-primer, ko obrat ne velja ($x \leq y \implies x < y$). - Dokaži, da velja: $\forall x, y\in \mathbb{Z}:\ x < y \implies x + 1 \leq y$. ## Dokazovanje pravilnosti Pri dokazovanju pravilnosti si lahko pomagamo z naslednjimi splošnimi nasveti. * Po stavku `x := N` vedno velja `{ x = N }`. Formalno to dokažemo tako: `{ N = N } x := N { x = N }`. * Pravilo za prireditveni stavek je `{ P[x ↦ e] } x := e { P }`. Pri izpeljevanju najprej vse `x`-e v predpogoju izrazimo z `e`, nato pa `e`-je zamenjamo z `x`. * V zančni invarianti se zančni pogoj in lokalne spremenljivke ne pojavljajo, saj mora invarianta veljati tudi po izstopu iz zanke. Ko invarianto »peljemo« čez telo zanke, se nam v njej lahko pojavijo lokalne spremenljivke. Teh se želimo znebiti, ko dosežemo konec zanke. * Na koncu zanke se lahko izkaže, da je invarianta prešibka in iz nje ne moremo izpeljati končnega pogoja. V tem primeru lahko v invarianto dodamo še kak pogoj in ga ločeno peljemo čez zanko. To ne bo nikoli pokvarilo obstoječe izpeljave: če velja $A \implies C$, potem velja tudi $A \wedge B \implies C$. ### Naloga 1 Dokažite parcialno in popolno pravilnost programa glede na dano specifikacijo. { x = m ∧ y = n } => { x + y - (x + y - y) = n ∧ x + y - y = m } x := x + y; { x - (x - y) = n ∧ x - y = m } y := x - y; { x - y = n ∧ y = m } x := x - y { x = n ∧ y = m } { x = m ∧ y = n } => { x + y = m + y ∧ y = n } x := x + y; { x = m + y ∧ y = n } => { x - y = m ∧ 0 + x = n - y + x } y := x - y; { y = m ∧ 0 + x = n + y } => { y = m ∧ 0 + x - y = n } x := x - y { y = m ∧ 0 + x = n } => { x = n ∧ y = m } ### Naloga 2 Dokažite parcialno in popolno pravilnost programa glede na dano specifikacijo. { true } if y < x then { true, y < x } => { y < x, x = x } z := x; { y < x, z = x } { y < z } x := y; { y < z, x = y } { x < z } y := z { x < z, y = z } else { true, !(y < x) } => { y >= x } skip { y >= x } end { x < z, y = z ali y >= x } => { x ≤ y } { true } if y < x then { true, y < x } => { y ≤ x } z := x; { y ≤ z } x := y; { x ≤ z } y := z { x ≤ y } else { true, !(y < x) } => { x ≤ y } skip { x ≤ y } end { x ≤ y } ### Naloga 3 Sestavite program `c`, ki zadošča specifikaciji [ n ≥ 0 ] c [ s = 1 + 2 + ... + n ] in dokažite njegovo pravilnost. [ n ≥ 0 ] i := 1 ; [ n ≥ 0, i = 1 ] s := 0 ; [ n ≥ 0, i = 1, s = 0 ] => [ s = 1 + 2 + ... + (i-1), i <= n+1 ] while i <= n do [ s = 1 + 2 + ... + (i-1), i <= n+1, i <= n, n-i = R, n-i >= -1 ] => [ s = 1 + 2 + ... + (i-1), i <= n+1, i <= n, n-i-1 = R-1 < R, n-i >= -1 ] => [ s+i = 1 + 2 + ... + (i-1) + i, i <= n, n-i-1 < R, n-i >= 0 ] <=> [ s+i = 1 + 2 + ... + (i-1) + i, i <= n, n-i-1 < R, n-i-1 >= -1 ] <=> [ s+i = 1 + 2 + ... + (i+1-1), i+1 <= n+1, n-(i+1) < R, n-(i+1) >= -1 ] s := s + i; [ s = 1 + 2 + ... + (i+1-1), i+1 <= n+1, n-(i+1) < R, n-(i+1) >= -1 ] i := i + 1 [ s = 1 + 2 + ... + (i-1), i <= n+1, n-i < R, n-i >= -1 ] done [ s = 1 + 2 + ... + (i-1), i <= n+1, !(i <= n) ] => [ s = 1 + 2 + ... + (i-1), i <= n+1, i > n ] => [ s = 1 + 2 + ... + (i-1), i = n+1 ] => [ s = 1 + 2 + ... + n ] ### Naloga 4 Dokažite parcialno in popolno pravilnost programa glede na dano specifikacijo. { x ≥ 0 } y := 0; z := x; while 1 < z - y do s := (y + z)/2; if s * s < x then y := s else z := s end done { y² ≤ x ≤ (y+1)² } ### Naloga 5 Dokažite popolno pravilnost spodnjega programa. NEDOKONČANA RESITEV: [ y > 0 ] x := 0 ; c := 0 ; while y > c do x := x + 1 ; c := x * x * x end { x * x * x = c, y <= c } => if y < c then [ I, y <= c, y < c ] => [ 0 = ∛0 ] x := 0 ; [ x = ∛0 ] y := 0 [ x = ∛y ] else [ x * x * x = c, y <= c, y >= c ] => [ x = ∛y ] skip [ x = ∛y ] end [ x = ∛y ]