„Odpowiedniość między programami i logiką nasuwa sugestię, że programy są odpowiednikami twierdzeń, zaś podprogramy – lematów.”



Pobieranie 303,28 Kb.
Strona1/2
Data10.01.2018
Rozmiar303,28 Kb.
  1   2

Wykład 5

Logika programów Hoare’a

„Odpowiedniość między programami i logiką nasuwa sugestię, że programy są odpowiednikami twierdzeń, zaś podprogramy – lematów.”

Logika Hoare’a jako język specyfikacji i logiki programów umożliwia udowodnienie poprawności programów.


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

X  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

    1. Wykonanie operacji II zawsze kończy się i nie ma wpływu na program P

(II; P) = P = (P; II)

    1. Niezależnie od położenia operator  zawsze przerywa program P

(; P) =  = (P;)

    1. Sekwencja programów P, Q, R jest łączna, czyli

P: (Q;R) = (P; Q); R

Niedeterministyczny wybór w sekwencji


    1. 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 częściowego uporządkowania


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



    1. 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)


    1. Relacja uporządkowania  ma operator  jako dolny element i operator  jako największą dolną granicę . Stąd

  P

    1. oraz

(R  P  R  Q)  R  (P  Q)

    1. 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ł”


„Ideał” T jest używany do realizacji dowolnych czynności - jest lepszy od programu, lecz nie można go implementować.

    1. Każdy program zawiera się w T

T  P

    1. Wykonanie programu P po T daje rezultat T

(T; P) = T

Warunek


    1. Jeśli w wyniku warunku wybrano program P, to są dwa możliwe przypadki:

(P < true > Q) = P = (Q < false > P)

    1. Sekwencja nakłada się na warunek

(P < b > Q) ; R = (P;R) < b > (Q; R)

    1. Warunek jest idempotentny

(P < b > P) = P

    1. Warunek jest łączny

(P < b > Q ) < c > R = P < b  c > (Q < c > R)

Asercja


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 > )


Przypisanie


2.15. Przypisanie wartości zmiennej x do siebie niczego nie zmienia

(x := x) = II



    1. Podobnie w wielokrotnym przypisaniu

(x,y := e,y) = (x := e)

    1. 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))


    1. 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)

    1. Puste przypisanie: jeśli x jest już równe e, to wyklucza się przypisanie e do x

(x = e); (x := e) = (x = e)

Rekursja i iteracje

Program rekursyjny X  F(X) jest zdefiniowany jako wyrażenie

X = F(X)




Rekursja

    1. X  F(X) = F(X  F(X))

    2. F(Y)  Y  X  F(X)  Y
Iteracje jako specjalny rodzaj rekursji

(b * P) = def X (( P; X) < b > II)

2.23. Po zakończeniu iteracje powodują zmianę warunku  b

(b * P) = (b* P); ( b)


    1. Dwie pętle o tym samym ciele można zastąpić jedną pętlą

(b  c) * P; (b * P) = (b*P)
Deklaracje zmiennych

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)

    1. 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

    1. Inna zmienna x w b przesłania zmienną x poza b, stąd deklaracja zmiennej x przenosi się przez warunek b

if x is not free in b

var x; (P < b > Q) = (var x; P) < b > (var x; Q)

    1. Kolejno występujące deklaracje var i end dla x nie wywołują żadnego efektu

(var x; end x) = II

    1. Inna zmienna x w b przesłania zmienną x poza b, stąd deklaracje end x;  var x nie mają wpływu na przypisanie do x,

if x is not free in b

(end x; var x; x := e) = (x := e)



    1. Przypisanie do zmiennej x przed końcem jej bloku nie ma znaczenia

(x := e; end x) = end x

3. Semantyka operacyjna


Rozróżnia się stany początkowe danych oznaczone jako s, stany końcowe danych oznaczone jako t. Poszczególne tranzycje, które mogą zachodzić w programie, są sformułowane na podstawie aksjomatów 2.1-2.30.
Zmiana stanu w programie z początkowego na końcowy jest zdefiniowana jako

(s, P)  (t, Q) =def (s; P)  (t; Q)



Podstawowe tranzycje w programie:

  1. Można zastąpić przepisanie zmiennej v wartością e sekwencją wartości początkowych s poprzedzających wartość e oraz wartości e

(s,v := e)  (v := (s; e), II)

Na podstawie praw 2.1 oraz 2.18




  1. II nie ma wpływu na przebieg programu

(s, (II; Q))  (s,Q)

Na podstawie prawa 2.1




  1. Program P przechodzi w Q, natomiast R jest zachowany

(s, (P;R)  (t, (Q; R)), gdy (s, P)  (t, Q)

Na podstawie: Kompozycja sekwencji jest monotoniczna




  1. Ponieważ nie wiadomo, czy P czy Q, stąd dwie możliwe tranzycje

(s, P  Q)  (s, P)

(s, P  Q)  (s, Q)

Na podstawie prawa 2.7


  1. Zakłada się, że b zawiera jedynie zmienne wolne, stąd nie zmienił się stan początkowy s danych

(s, P < b > Q)  (s, P), gdy s; b

(s, P < b > Q)  (s,Q), gdy s; b

Na podstawie praw 2.19 i 2.11


  1. Każde wywołanie rekurencyjne z ciała procedury jest wymieniane na całą procedurę rekurencyjną,

(s,  X  F(X))  (s, F(  X  F(X)))

Na podstawie prawa 2.21




  1. Zły program wykonuje nieskończoną liczbę kroków

(s, )  (s, )

Na podstawie :  jest zwrotne



4. Technika asercji indukcyjnych dla dowodzenia poprawności programów
System dowodzenia opiera się na systemie asercji, które mogą pełnić rolę profesjonalnych komentarzy w programach. Asercje formalizują aspekty intuicyjnego zrozumienia programu. Powinny być zawsze prawdziwe, gdy sterowanie przechodzi wzdłuż linii, do której są one dołączone. Prawdziwość asercji można udowodnić, gdy zastosuje się modele instrukcji programu.
Podstawowe reguły logiki Hoare:
Podstawową konstrukcją językową jest {S}. Oznacza ona, że stan przed wykonaniem instrukcji S ma własność  i wykonanie instrukcji S zmienia własność stanu na .
Aksjomaty (reguły) systemu dowodzenia poprawności programów [6]:
A1. {x := e} – aksjomat przypisania

A2. Jeżeli {S};     {S}

A3. Jeżeli {S};     {S}

A4. Jeżeli {S1) 1; 1{S2} {S1,S2}

A5. Jeżeli   b{S1} i    b     {if b then S1}

A6. Jeżeli   b{S1} i   b{S2}   {if b then S1 else S2}

Niech S = S1; if  b then repeat S1 until b

A7. Jeżeli {S1} i    b    {repeat S1 until B}   b

Niech while b do S1

A8. Jeżeli   b {S1}  {while b do S1}   b


Uwaga: w programach := oznacza = oraz = oznacza ==
Zastosowanie praw, tranzycji i reguł dowodzenia


  • W systemach dowodzenia prawa 2.1-2.30 odnoszą się do syntaktyki programów - służą do sprawdzenia przepływu danych między instrukcjami, do analizy strukturalnej własności tekstów programów wraz z różnymi transformacjami strukturalnymi oraz ustanawiania warunków zakończenia pętli

  • Tranzycje (1)-(8) i reguły A.1-A8 służą do analizy efektów wykonania programu, dotyczą więc jego semantyki


Problem poprawności programów
Problem dowodzenia poprawności programu jest ściśle związany z problemem zatrzymania się programu. Oparty jest on na fakcie, że modelowanie zachowania programu jest oparte:

  • na specyfikacji semantycznej obejmującej instrukcje i deklaracje podstawowe jako aksjomaty dowodu

  • i regułach wnioskowania opartych na instrukcjach i deklaracjach strukturalnych, które wiążą strukturę dowodu ze strukturą programu.

Program S jest częściowo poprawny względem specyfikacji, gdy dla wejścia spełniającego asercję wejściową  przy dowolnym wartościowaniu początkowym zmiennych programu, że jeśli S kończy się, to wartość zmiennych spełnia asercję wyjściową .


Program S jest poprawny względem specyfikacji, gdy dla wejścia spełniającego asercję wejściową  przy dowolnym wartościowaniu początkowym zmiennych programu, to S kończy się i wartość zmiennych spełnia asercję wyjściową .
Problem stopu programu [8]
Przykład programu, który zatrzymuje się (podano tekst w pseudojęzyku) dla liczb naturalnych nieparzystych, natomiast nie zatrzymuje się dla liczb parzystych.

  1. dopóki X1 dopóty wykonuj X  X-2

  2. zatrzymaj się

Przykład programu, który się zawsze zatrzymuje dla dowolnych liczb naturalnych, ale nie można tego formalnie udowodnić.



  1. dopóki X  1, dopóty wykonuj:

    1. jeśli X jest parzyste, wykonuj X X/2

    2. w przeciwnym przypadku (X nieparzyste) wykonaj X3*X +1

  1. zatrzymaj się

Dowód nieroztrzygalności problemu stopu



Nie istnieje program Q w języku L, który po zaakceptowaniu dowolnej pary (S, X), składającej się z tekstu poprawnego programu S w języku L i napisu X, zatrzyma się po pewnym skończonym czasie wypisując „tak”, jeśli program S(X) zatrzymuje się dla danych X, lub nie, jeśli program S(X) nie zatrzymuje się dla danych X.

Dowód „nie wprost”



Z
akłada się, że program Q istnieje i z tego założenia wyprowadza się sprzeczność.

N
iech program S w języku L ma jako dane – poprawny program W w języku L. Po przeczytaniu danych program S wykonuje kopię W, otrzymując parę . Następnie program S uaktywnia program Q na danych . Program S czeka na zakończenie Q. Zgodnie z założeniem Q powinien się zatrzymać, ponieważ jego dana W jest poprawnym programem w języku L, druga dana jako kopia W jest tylko napisem dla Q. Jeśli Q odpowie „tak”, to program S ma wejść w nieskończoną pętlę, a jeśli Q odpowie „nie”, S ma natychmiast zatrzymać się.

Istnieje jednak logiczna niemożliwość skonstruowania takiego programu S. Załóżmy bowiem, że programem W jest sam program S. Aby zobaczyć, że program S jako dana dla siebie, stanowi sprzeczność, załóżmy że S zatrzymuje się wtedy, gdy daną będzie jego własny tekst, S(S). Jednak na początku powtórzono dwa egzemplarze tego programu. Następnie będą one przekazane programowi Q, który powinien po pewnym czasie zatrzymać się, dlatego dla danych , gdy S(S), musi dać odpowiedź „tak”. Rozpocznie wtedy nieskończoną pętlę, stąd S(S) S(S). Podobnie jest w przypadku „nie” dla danej S(S)S(S) . Oba przypadki prowadzą do sprzeczności, a jeden z nich musi zachodzić. Ponieważ z założenia wynika, że S jest poprawnym programem, dlatego przyczyną tych sprzeczności jest program Q. Stąd wniosek, że nie można rozstrzygnąć problemu stopu.

Przykład 5.1

[Na przykładzie Hoare] badanie poprawności programu, który oblicza resztę z dzielenia metodą kolejnego odejmowania, aż różnica będzie mniejsza od odjemnika.

Program S



  1   2


©operacji.org 2017
wyślij wiadomość

    Strona główna