Na zakończenie pokażemy jak można wykorzystać logikę do precyzyjnego zdefiniowania semantyki programów. Jako
przykładowy język rozważymy pewien fragment Pascala. Następnie wykorzystamy ją do opisu formalnych metod weryfikacji tych programów.
Będziemy rozważać język, który dysponuje:
1 zmiennymi całkowitoliczbowymi (dokładniej, naturalnymi);
2 instrukcjami:
1 przypisania:
2 złożoną:
3 warunkową: if warunek then akcja1 else akcja2;
4 pętli while warunek do akcja;
Definicja
Jeśli w programie występuje n zmiennych (x1,...,xn), stan obliczenia programu jest ciągiem (x1, . . . , xn) liczb, gdzie xi
odpowiada wartości zmiennej xi.
Stąd będziemy rozważać zbiory takich ciągów, czyli relacje i predykaty n-argumentowe. Będą nas interesować relacje wyznaczone przez formuły.
Definicja
Niech U = An, dla pewnego modelu A języka I-go rzędu o nośniku A, a ϕ będzie dowolną formułą tego języka, której zmienne wolne są podzbiorem (x1,...,xn). Zdefiniujmy:
W ϕ = {(x1, . . . , xn); (A, (x1, . . . , xn)) |= ϕ}
jako zbiór wszystkich warościowań, przy których formuła jest spełniona w modelu.
Przykład 1Rozważmy instrukcję S x:=2*y+1, której wykonanie zmienia stan (x, y ) w (2y + 1, y ). Jeśli dany jest zbiór stanów początkowych opisany formułą y 6 3, to zbiór wszystkich stanów końcowych opisany jest formuła x 6 7 ∧ y 6 3. Mówimy, że S przekształca stan y 6 3 w x 6 7 ∧ y 6 3.
Sematykę języka programowania definiujemy przez sposób transformacji stanu początkowego w końcowy.
Definicja
Asercją nazywamy trójkę pSq, gdzie S jest programem, a p,q formułami opisującymi warunek początkowy i końcowy. asercja jest prawdziwa: |= pSq, gdy program S rozpoczynając się w stanie p, znajdzie się w stanie q po zakończeniu obliczeń, o ile to nastąpi.
Wtedy mówimy, że program jest częściowo poprawny wzgłedem p,q. Asercje są zwane trójkami Hoare’a.
Nietrudno zauważyć, że podany w przykładzie warunek wstępny jest najsłabszym, który pociąga warunek końcowy, czyli, w szczególności x 6 7.
Definicja
Formuła A jest słabsza od formuły B, jeśli B ⇒ A.
Zauważmy, że wtedy zbiór WA zawiera zbiór WB! I stąd nazwa.
Definicja
Dla programu S i formuły q najsłabszym warunkiem wstępnym nazywamy najsłabszą formułę p, dla której pSq. Wtedy p oznaczamy symbolem nww(S,q) .
Bezpośrednio z definicji wynika:
Lemat
|= pSq wtedy i tylko wtedy, gdy |= p ⇒ nww(S,q).
Teraz można precyzyjnie opisać semantykę każdej instrukcji. W tym celu wystarczy wyznaczyć najsłabszy warnek wstępny dla każdej instrukcji i formuły opisującej zbiór stanów po jej wykonaniu.
1 nww (x:=t,p(x))=p(x⇐t);
2 nww (S1;S2,q)= nww (S1, nww (S2,q))
3 nww (if B then S1 else S2,q)= (B ⇒ nww (S1,q)) ∧(¬B ⇒ nww (S2,q))
4 nww ( while B do S,q)=(¬ B ⇒q) ∧ (B ⇒ nww (S;while B do S,q))
Nietrudno wykazać,że zachodzi:
Lemat
1 nww(if B then S1 else S2,q)= (B ∧ nww(S1,q)) ∨(¬B ∧ nww(S2,q)),
2 nww( while B do S,q)=(¬ B ∧q) ∨ (B ∧ nww(S;while B do S,q)).
Przykład 2
nww (x:=x+a; y:= y-1, x = (b − y ) ∗ a) z def. nww dla złożenia
nww (x:=x+a;, nww ( y:= y-1, x = (b − y ) ∗ a) z def. nww dla podstawienia
nww (x:=x+a;, x = (b − y + 1) ∗ a) z def. nww dla podstawienia
x + a = (b − y + 1) ∗ a upraszczając równanie x = (b − y ) ∗ a
Przykład 3
nww (q:=0; r:= x, x = q ∗ y + r ) = df. nww dla złożenia nww (q:=0;, nww (r:= x, x = q ∗ y + r ))∗ = df. nww dla podst.
nww (q:=0, x = q ∗ y + x) = df. nww dla podst.
x = x = 0 ∗ y + x = upraszczając r-nie
x = x
Wtedy ponieważ x > 0 ∧ y > 0 ⇒ x = x z lematu 1.6 mamy {x > 0 ∧ y > 0}q:=0; r:= x{x = q ∗ y + r}
Przykład 4Podobnie korzystając najpierw z definicji nww mamy nww (if y=0 then x:=0 else x:=y+1, x = y ) = (y = 0 ⇒ nww (x:= 0, x = y )) ∧ (y 6= 0 ⇒ nww (x:= y+1, x = y )) = (y = 0 ⇒ 0 = y ) ∧ (y 6= 0 ⇒ y + 1 = y ) równ.
(y 6= 0 ⇒ false równ.
y = 0
Przykład 5
nww (if x>= y then x:=x-y else y:=y-x, nwd (x, y ) = nwd (a, b)) (x > y ⇒ nww (x:= x-y, nwd (x, y ) = nwd (a, b)))∧
(y > x ⇒ nww (y:= y-x, nwd (x , y ) = nwd (a, b))) = (x > y ⇒ nwd (x − y , y ) = nwd (a, b))∧
(y > x ⇒ nwd (x , y − x ) = nwd (a, b))
W ostatnim (w tym podrozdziale) twierdzeniu zebraliśmy najważniejsze własność warunków wstępnych.
Twierdzenie
1 |= nww (S, p) ∧ nww (S, q) ⇔ nww (S, p ∧ q)
2 |= nww (S, p) ∧ nww (S, ¬p) ⇔ nww (S, false)
3 |= ¬nww (S, ¬p) ⇒ nww (S, p)
4 p ⇒ q pociąga |= nww (S, p) ⇒ nww (S, q)
System dowodzenia, w którym formułami są asercje jest używany do dowodzenia własności programów, np. ich poprawności. System ten nie pozwala na dowodzenie własności dziedziny, w której są prowadzone obliczenia, u nas jest zbiór liczb całowitych. Tego typu formuły są w tym systemie aksjomatami.
System Hoare’a Aksjomaty dziedziny
Każda formuła prawdziwa w dziedzinie obliczenia jest aksjomatem.
Aksjomat przypisania
` {p(x\t)}x := t{p(x)}
Reguła złożenia
` {p}S1{q} i ` {q}S2{r } pociągają ` {p}S1; S2{r } Reguła instrukcji warunkowej
` {p ∧ B}S1{q} i ` {p ∧ ¬B}S2{q} pociągają
` {p}if B then S1 else S2 {q}
Reguła pętli
` {p ∧ B}S{p} pociąga ` {p} while B do S {p ∧ ¬B}
Definicja
Formułę p występującą w powyższej regule nazywamy niezmiennikiem pętli.
Reguła konsekwencji
` p1 ⇒ p, ` {p}S{q}, ` q ⇒ q1 pociągają ` {p1}S{q1}
Wyznaczanie niezmiennika pętli jest zwykle bardzo
skomplikowanym zadaniem. Dlatego w zadaniach podaje się potencjalny niezmiennik p i należy wykazać, że faktycznie p nim jest. Wtedy dowód asercji {s} while B do S {q} przebiega w trzech etapach: należy wyskazać , że p jest niezmiennikiem, a nastepnie udowodnić, że s ⇒ p i p ∧ ¬B ⇒ q.
Częściowa poprawność mnożenia
{true}
x := 0;
{x = 0}
y := b;
{x = 0 ∧ y = b}
while y<>0 do {x = (b − y )a}
begin x:=x+a; y:=y-1 end;
{x = ab}
Twierdzenie
` {true}P{x = ab}.
DowódZ aksjomatu przypisania mamy {0 = 0} x := 0 {x = 0}, stosując regułę konsekwencji o przesłance true ⇒ 0 = 0 mamy {true}x:=0{x = 0}. Rozumowanie dla
{x = 0}y:=b{x = 0 ∧ y = b} jest podobne.
Niech x = (b − y )a będzie formułą p. W przykładzie 2.
pokazaliśmy,że to jest niezmiennik x:=x+a; y:=y-1. Podobnie możemy wzmocnić warunek wstępny:
{p ∧ y 6= 0}x:=x+a; y:=y-1{p}
Mamy wtedy przesłankę reguły pętli,a zatem {p}
while y<> 0 do
begin x:=x+a; y:=y-1 end {p ∧ ¬(y 6= 0)}
Częściowa poprawność algorytmu Euklidesa
Korzystajac z aksjomatów dziedziny i reguły konsekwencji otrzymujemy, że x = ab jest w-kiem końcowym programu.
Zajmijmy się jeszcze algorytmem Euklidesa.
{true}
x=a; y:=b;
while x<>y do
if x>y then x:=x-y else y:=y-x;
{x = nwd (a, b)}
Bezpośrednio z opisu najsłabszego w-ku wstępnego mamy, {true}P{x = nwd (a, b)}.
