Wykład 5
Logika programów Hoare’a
Logika ta polega na zdefiniowaniu:
· semantyki instrukcji i deklaracji podstawowych jako aksjomatów
· instrukcji i deklaracji strukturalnych jako reguł wnioskowania, które bezpośrednio kojarzą strukturę dowodu ze strukturą syntaktyki.
1. Specyfikacja podstawowych operacji w językach programowania (na podstawie C.A.R.Hoare, He Jifeng, A.Sampaio: Algebraic Derivation of an Operational Semantics):
^ przerwanie poprawnego programu
II nic nie rób
x,y,...z := e,f,...,g wielokrotne przypisanie
P;Q sekwencja
P Õ Q wybór niedeterministyczny P lub Q
P < b > Q if b then P else Q
mX · P rekursywny program X z ciałem P
T „ideał”
var v deklaracja wprowadzająca zmienną
end v koniec obowiązywania zmiennej
b^ asercja: if b then II else ^
2. Podstawowe prawa
Nic nie rób, przerwanie, sekwencja
2.1. Wykonanie operacji II zawsze kończy się i nie ma wpływu na program P
(II; P) = P = (P; II)
2.2. Niezależnie od położenia operator ^ zawsze przerywa program P
(^; P) = ^ = (P;^)
2.3. Sekwencja programów P, Q, R jest łączna, czyli
P: (Q;R) = (P; Q); R
2.4. Operator Õ jest łączny, zamienny, idempotentny i wobec niego operator ^ jest równy zero, stąd mamy dla sekwencji programów P,Q R, S
P; (Q Õ R); S = (P;Q;S) Õ (P; R; S)
Relacja Í jest częściowego porządku, czyli jest zwrotna, przechodnia, antysymetryczna. Stąd, jeśli program P zawiera się w programie Q, to program P spełnia ostrzejsze wymagania. Stąd mamy:
P Í Q =def (P Õ Q) = P
2.5. Jeśli program Pi zawiera się w Pi+1: Pi Í Pi+1 dla każdego i oraz suma programów Èi Pi jest zawarta w programie Q, stąd każdy program Pi jest zawarty w programie Q, czyli:
(Èi Pi ) Í Q « "i · (Pi Í Q)
2.6. Relacja uporządkowania Í ma operator ^ jako dolny element i operator Õ jako największą dolną granicę . Stąd
^ Í P
2.7. oraz
(R Í P Ù R Í Q) « R Í (P Õ Q)
2.8. Z zależności P Í Q wynika F(P) Í F(Q) dla wszystkich interpretacji F (od funkcji należących do programów do programów). Oznacza to, że F, i w konsekwencji wszystkie operatory języka, są monotoniczne względem Í. Stąd mamy:
if P Í Q then
(1) (P Õ R) Í (Q Õ R) (Õ monotoniczny)
(2) ( R; P; S) Í (R; Q; S) (; monotoniczny)
„Ideał” T jest używany do realizacji dowolnych czynności - jest lepszy od programu, lecz nie można go implementować.
2.9. Każdy program zawiera się w T
T Ê P
2.10. Wykonanie programu P po T daje rezultat T
(T; P) = T
2.11. Jeśli w wyniku warunku wybrano program P, to są dwa możliwe przypadki:
(P < true > Q) = P = (Q < false > P)
2.12. Sekwencja nakłada się na warunek
(P < b > Q) ; R = (P;R) < b > (Q; R)
2.13. Warunek jest idempotentny
(P < b > P) = P
2.14. Warunek jest łączny
(P < b > Q ) < c > R = P < b Ù c > (Q < c > R)
Notacja b^ oznacza asercję. Oznacza on II, gdy b jest równe true, w przeciwnym wypadku oznacza ono ^. Stąd mamy:
b^ = def (II < b > ^)
2.15. Przypisanie wartości zmiennej x do siebie niczego nie zmienia
(x := x) = II
2.16. Podobnie w wielokrotnym przypisaniu
(x,y := e,y) = (x := e)
2.17. Lista zmiennych i wyrażeń może wystąpić jako dowolna permutacja
(x, y, z := e, f, g) = (y, x, z := f, e, g)
2.18. Sekwencja przypisań do tej samej zmiennej może być zastąpiona pojedynczym przypisaniem
(x := e; x := f(x)) = (x := ((x := e); f(x))) = (x := f(e))
2.19. Przypisanie przenosi się prawostronnie przez warunek, zastępując wystąpienie przypisywanej zmiennej w warunku
x := e; (P < b > Q) = (x := e; P) < ((x := e); b) > (x := e; Q)
2.20. Puste przypisanie: jeśli x jest już równe e, to wyklucza się przypisanie e do x
(x = e)^; (x := e) = (x = e)^
Rekursja
2.21. mX · F(X) = F(mX · F(X))
2.22. F(Y) Í Y ® mX · F(X) Í Y
(b * P) = def mX · (( P; X) < b > II)
2.23. Po zakończeniu iteracje powodują zmianę warunku Ø b
(b * P) = (b* P); (Ø b) ^
2.24. Dwie pętle o tym samym ciele można zastąpić jedną pętlą
(b Ù c) * P; (b * P) = (b*P)
Deklaracja var x,y,...,z wprowadza zmienne x,y,...,z od miejsca wystąpienia deklaracji do wystąpienia deklaracji zakończenia bloku zmiennej end x,y,...,z.
Jeśli P jest programem i x jest zmienną, mówimy że wystąpienie x w P jest wolne, jeżeli jest poza blokiem deklaracji innej zmiennej x w P, natomiast w bloku zmienna
x nie jest wolna. W aksjomatach nie uwzględniono zagnieżdżeń deklaracji.
2.25. Obojętna jest kolejność deklaracji zmiennych oraz zakończenia
(1) (var x; var y ) = var x, y = (var y; var x)
(2) (end x; end y ) = end x, y = (end y; end x)
2.26. Inna zmienna x w P przesłania zmienną x poza P
if x is not free in P
(1) P; var x = var x; P
(2) end x; P = P; end x
2.27. Inna zmienna x w b przesłania zmienną x poza b, stąd deklaracja zmiennej x przenosi się przez warunek b
...
RezidentRnR