## 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 := x + y;
    y := x - y;
    x := x - y
    { x = n ∧ y = m }


### Naloga 2

Dokažite parcialno in popolno pravilnost programa glede na dano specifikacijo.

    { }
    if y < x then
      z := x;
      x := y;
      y := z
    else
      skip
    end
    { x ≤ y }


### Naloga 3

Sestavite program `c`, ki zadošča specifikaciji

    [ n ≥ 0 ]
    c
    [ s = 1 + 2 + ... + n ]

in dokažite njegovo pravilnost.


### 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 ]