# Pravilnost programov

### Program, ki zamenja `x` in `y`

Program, ki zamenja vrednosti `x` in `y`:

```
{ x = m ∧ y = n }
t := x ;
x := y ;
y := t
{ x = n ∧ y = m }
```

Tudi ta zadošča specifikaciji:

```
{ x = m ∧ y = n }
while true do skip done
{ x = n ∧ y = m }
```

Tudi ta zadošča:
```
{ x = m ∧ y = n }
x := n ;
y := m
{ x = n ∧ y = m }
```

Še enkrat (`c` ne omenja `m` in `n`):
pravimo, da sta `m` in `n` **duhova** (ghost variable)
```
{ x = m ∧ y = n }
c
{ x = n ∧ y = m }
```

### Primer: uredi spremnljivki `x` in `y`

Poskus:
```
{ true }
c
{ x ≤ y }
```

```
{ true }
x := 1 ; y := 7
{ x ≤ y }
```

```
{ x = m ∧ y = n }
c
{ x = min(m, n) ∧ y = max(m, n) }
```
Opomba: `m` in `n` sta duhova.

Rešitev:
```
{ x = m ∧ y = n }
if x > y then 
  t := x ;
  x := y ;
  y := t
else
  skip
end
{ x = min(m, n) ∧ y = max(m, n) }
```

Kaj pa to?

```
{ x = m ∧ y = n }
             -- x = m, y = n
x := x + y ; -- x = m + n, y = n
y := x - y ; -- y = m + n - n = m, x = m + n
x := x - y   -- x = m + n - m = n, y = m
{ x = n ∧ y = m }
```
Opomba: `c` lahko omeni samo `x` in `y`

Bolje:
```
{ x = m ∧ y = n }
x := x + y ;
{ x = m + n ∧ y = n }
y := x - y ;
{ y = m + n - n  ∧ x = m + n }
x := x - y
{ x = m + n - m ∧ y = m } ⇒
{ x = n ∧ y = m }
```

### Naloga

```
{ x ≤ 7 }    ⇒ (prištejemo 3)
{ x + 3 ≤ 10 }
x := x + 3
{ x ≤ 10 }
```

### Naloga:

Zapiši: `c` se ne ustavi (odgovor: `{true} c {false}`)
Zapiši: `c` se ustavi (odgovor: `[ true  ] c [ true ]`)

```
{ true  } c { true  }
-- vedno res, ker ϕ ⇒ true velja


{ true  } c { false }
"true ∧ (c se ustavi) ⇒ false" ⇔
"(c se ustavi) ⇒ false"        ⇔ opomba: ϕ ⇒ false
                                          je ekvivalentno
                                          ¬ ϕ 
"ne (c se ustavi)"
"c se ne ustavi"

{ false } c { true  }  -- vedno res
"false ∧ (c se ustavi) ⇒ true"
"false ⇒ true"
"true"


{ false } c { false }  -- vedno res
"false ∧ (c se ustavi) ⇒ false"
"false ⇒ false"
"true"

[ true  ] c [ true ]
"true ⇒ c se ustavi ∧ true"
"true ⇒ c se ustavi"
"c se ustavi"


[ true  ] c [ false ]  -- nikoli ne velja
"true ⇒ c se ustavi ∧ false"
"true ⇒ false"
"false"

[ false ] c [ true  ]  -- vedno velja
"false ⇒ c se ustavi ∧ true"
"true"

[ false ] c [ false ]  -- vedno velja
"false ⇒ c se ustavi ∧ true"
```

### Naloga

```
{ x ≤ y }                                 ⇒
{ x + x ≤ x + y ≤ y + y }                 ⇒
{ (x + x) / 2 ≤ (x + y) / 2 ≤ (y + y)/2 } ⇒
{ x ≤ (x + y)/2 ≤ y }
s := (x + y)/2
{ x ≤ s ≤ y }
```


### Naloga

```
[ b ≥ 0 ]
i := 0 ;
p := 1 ;
while i < b do
   p := p * a ;
   i := i + 1
done
[ p = a ^ b ]
```

Najprej dokažemo delno pravilnost:

```
{ b ≥ 0 }
i := 0 ;
{ b ≥ 0, i = 0 }
p := 1 ;
{ b ≥ 0, i = 0, p = 1 }
?

{ p = a^i, i ≤ b }
while i < b do
   { p = a^i, i ≤ b, i < b }  ⇒ (malo manj očitno)
   { p · a = a^(i+1), i+1 ≤ b }
   p := p * a ;
   { p = a^(i+1), i+1 ≤ b }
   i := i + 1
   { p = a^i, i ≤ b }
done
{ p = a^i, i ≤ b, i ≥ b }  ⇒
{ p = a^i, i = b }         ⇒
{ p = a^b }
```

Preverimo, da se `b - i` zmanjšuje (`b - i ≥ 0` že vemo)
Telo zanke:

```
  [ b - i = z ]        ⇒
  [ b - i - 1 < z ]    ⇒
  [ b - (i + 1) < z ]
  p := p * a ;
  [ b - (i + 1) < z ]
  i := i + 1
  [ b - i < z ]

```

### Naloga

```
[ x = m ∧ y = n ]
if y < x then
   [ x = m ∧ y = n, y < x ]           => (easy)
   [ y = min(m, n) ∧ x = max(m, n) ]
   [ y = min(m, n) ∧ (x + y) - y = max(m, n) ]
   x := x + y ;
   [ y = min(m, n) ∧ x - y = max(m, n) ]
   [ x - (x - y) = min(m, n) ∧ x - y = max(m, n) ]
   y := x - y ;
   [ x - y = min(m, n) ∧ y = max(m, n) ]
   x := x - y
   [ x = min(m, n) ∧ y = max(m, n) ]
else
   [ x = m ∧ y = n, ¬ (y < x) ]  ⇒
   [ x = m ∧ y = n, x ≤ y ]
   skip
   [ x = m ∧ y = n, x ≤ y ]           ⇒ (easy)
   [ x = min(m, n) ∧ y = max(m, n) ]
end
[ x = min(m, n) ∧ y = max(m, n) ]
```