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 vsex
-e v predpogoju izrazimo ze
, nato pae
-je zamenjamo zx
. - 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 ]
마지막 수정됨: 일요일, 12 3월 2023, 6:11 AM