Vaje 3 (dokazovanje pravilnosti)

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 ]