## 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 ∧ x - y = n }
    x := x - y
    { y = m ∧ 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 }
        z := x;
        { y ≤ z }
        x := y;
        { x ≤ z }
        y := z
        { x ≤ y }
    else
        { true, !(y < x) } =>
        { x ≤ y }
        skip
        { x ≤ y }
    end
    { x ≤ y }


    { 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 } =>
    { 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 ]
    s := 0;
    [ n ≥ 0, s = 0 ]
    m := n;
    [ n ≥ 0, s = 0, m = n ] =>
    [ s = n + (n-1) + ... + (m+1), m >= 0 ]
    while m > 0 do
        [ s = n + (n-1) + ... + (m+1), m >= 0, m > 0, R = m, m >= 0 ] =>
        [ s+m = n + (n-1) + ... + m, m > 0, R > R-1 = m-1 ] =>
        [ s+m = n + (n-1) + ... + (m-1+1), m-1 >= 0, R > m-1 ]
        s := s + m;
        [ s = n + (n-1) + ... + (m-1+1), m-1 >= 0, R > m-1 ]
        m := m - 1
        [ s = n + (n-1) + ... + (m+1), m >= 0, R > m, m >= 0 ]
    done
    [ s = n + (n-1) + ... + (m+1), m >= 0, m <= 0 ] =>
    [ s = n + (n-1) + ... + (m+1), m = 0 ] =>
    [ 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.

    [ y > 0 ]
    x := 0 ;
    c := 0 ;
    while y > c do
      x := x + 1 ;
      c := x * x * x
    end
    if y < c then
      x := 0 ;
      y := 0
    else
      skip
    end
    [ x = ∛y ]