Logika Hoare'a - Hoare logic

Logika Hoare'a (znana również jako logika Floyda-Hoare'a lub zasady Hoare'a ) to formalny system z zestawem logicznych reguł do rygorystycznego wnioskowania o poprawności programów komputerowych . Został zaproponowany w 1969 roku przez brytyjskiego informatyka i logika Tony'ego Hoare'a , a następnie udoskonalony przez Hoare'a i innych badaczy. Pierwotne pomysły zostały zasiane przez prace Roberta W. Floyda , który opublikował podobny system schematów blokowych .

Hoare potrójny

Centralną cechą logiki Hoare'a jest trójka Hoare'a . Trójka opisuje, w jaki sposób wykonanie fragmentu kodu zmienia stan obliczeń. Trójka Hoare'a ma formę

${\ Displaystyle \ {P \} C \ {Q \}}$

gdzie i są twierdzeniami i jest poleceniem . jest nazwany warunek i na postcondition : gdy warunek jest spełniony, wykonanie polecenia ustanawia postcondition. Asercje to formuły w logice predykatów . ${\displaystyle P}$${\displaystyle Q}$${\ Displaystyle C}$${\displaystyle P}$${\displaystyle Q}$

Logika Hoare zapewnia aksjomaty i reguły wnioskowania dla wszystkich konstrukcji prostego imperatywnego języka programowania . Oprócz reguł dla prostego języka w oryginalnym artykule Hoare'a, Hoare i wielu innych badaczy opracowało od tego czasu reguły dla innych konstrukcji językowych. Istnieją reguły dotyczące współbieżności , procedur , skoków i wskaźników .

Poprawność częściowa i całkowita

Używając standardowej logiki Hoare'a, można udowodnić tylko częściową poprawność , podczas gdy zakończenie należy udowodnić osobno. Tak więc intuicyjne odczytanie trójki Hoare'a brzmi: Ilekroć utrzymuje się stan przed wykonaniem , wtedy będzie obowiązywał później lub nie kończy się. W tym drugim przypadku nie ma „po”, więc może być w ogóle dowolna wypowiedź. Rzeczywiście, można wybrać fałsz, aby wyrazić, że nie kończy się. ${\displaystyle P}$${\ Displaystyle C}$${\displaystyle Q}$${\ Displaystyle C}$${\displaystyle Q}$${\displaystyle Q}$${\ Displaystyle C}$

Całkowitą poprawność można również wykazać za pomocą rozszerzonej wersji reguły While.

W swoim artykule z 1969 r. Hoare użył węższego pojęcia zakończenia, które pociągało za sobą również brak jakichkolwiek błędów w czasie wykonywania: „Niepowodzenie zakończenia może być spowodowane nieskończoną pętlą; na przykład zakres operandów numerycznych, wielkość pamięci masowej lub limit czasu systemu operacyjnego."

Zasady

Pusty schemat aksjomatu instrukcji

Pusty oświadczenie zasada stwierdza, że Skip stwierdzenie nie zmienia stanu programu, co jest prawdziwe, co przed pominąć również odnosi się później.

${\displaystyle {\dfrac {}{\{P\}{\texttt {pominąć}}\{P\}}}}$

Schemat aksjomatu przypisania

Aksjomat przypisania stwierdza, że ​​po przypisaniu każdy predykat, który wcześniej był prawdziwy dla prawej strony przypisania, jest teraz obowiązujący dla zmiennej. Formalnie niech P będzie stwierdzeniem, w którym zmienna x jest wolna . Następnie:

${\ Displaystyle {\ dfrac {}{\ {P [E / x] \} x: = E \ {P \}}}}$

gdzie oznacza twierdzenie P , w którym każdy wolny występowanie od x został zastąpiony przez wyrażenie E . ${\displaystyle P[E/x]}$

Schemat aksjomatu przypisania oznacza, że ​​prawdziwość P jest równoważna prawdziwości P . Tak więc były prawdziwe przed przypisaniem, przez aksjomat przypisania, wtedy P byłoby prawdziwe po którym. Odwrotnie, były fałszywe (tj. prawdziwe) przed oświadczeniem przypisania, P musi następnie być fałszywe. ${\displaystyle P[E/x]}$${\displaystyle P[E/x]}$${\displaystyle P[E/x]}$${\ Displaystyle \ neg P [E / x]}$

Przykłady prawidłowych trójek obejmują:

• ${\ Displaystyle \ {x + 1 = 43 \} y: = x + 1 \ {y = 43 \}}$
• ${\ Displaystyle \ {x + 1 \ równoważnik N \} x: = x + 1 \ {x \ równoważnik N \}}$

Wszystkie warunki wstępne, które nie są modyfikowane przez wyrażenie, mogą zostać przeniesione do warunku końcowego. W pierwszym przykładzie przypisanie nie zmienia faktu, że , więc obie instrukcje mogą pojawić się w warunku końcowym. Formalnie wynik ten uzyskuje się przez zastosowanie schematu aksjomatu z P będącym ( i ), który daje byt ( i ), który z kolei można uprościć do danego warunku wstępnego . ${\displaystyle y:=x+1}$${\displaystyle x+1=43}$${\displaystyle y=43}$${\displaystyle x+1=43}$${\displaystyle P[(x+1)/y]}$${\displaystyle x+1=43}$${\displaystyle x+1=43}$${\displaystyle x+1=43}$

Schemat aksjomatu przypisania jest równoważny powiedzeniu, że aby znaleźć warunek wstępny, najpierw weź warunek końcowy i zastąp wszystkie wystąpienia lewej strony przypisania prawą stroną przypisania. Uważaj, aby nie robić tego wstecz, kierując się tym niepoprawnym sposobem myślenia: ; ta zasada prowadzi do bezsensownych przykładów, takich jak: ${\ Displaystyle \ {P \} x: = E \ {P [E / x] \}}$

${\ Displaystyle \ {x = 5 \} x: = 3 \ {3 = 5 \}}$

Inną błędną zasadą, która na pierwszy rzut oka wydaje się kusząca, jest ; prowadzi do bezsensownych przykładów, takich jak: ${\ Displaystyle \ {P \} x: = E \ {P \ klin x = E \}}$

${\ Displaystyle \ {x = 5 \} x: = x + 1 \ {x = 5 \ klin x = x + 1 \}}$

Podczas gdy dany warunek końcowy P jednoznacznie określa warunek wstępny , odwrotność nie jest prawdziwa. Na przykład: ${\displaystyle P[E/x]}$

• ${\ Displaystyle \ {0 \ równoważnik r \ cdot r \ klin r \ cdot r \ równoważnik 9 \} x: = r \ cdot r \ {0 \ równoważnik x \ klin x \ równoważnik 9 \}}$,
• ${\ Displaystyle \ {0 \ leq r \ cdot r \ klin r \ cdot r \ równ 9 \} x: = r \ cdot r \ {0 \ równ x \ klin r \ cdot r \ równ 9 \}}$,
• ${\ Displaystyle \ {0 \ leq r \ cdot r \ klin r \ cdot r \ równ 9 \} x: = r \ cdot r \ {0 \ równ r \ cdot r \ klin x \ równ 9 \}}$, oraz
• ${\ Displaystyle \ {0 \ równoważnik r \ cdot r \ klin r \ cdot r \ równoważny r 9 \} x: = r \ cdot r \ {0 \ równoważny r \ cdot r \ klin r \ cdot r \ równy 9 \} }$

są prawidłowymi instancjami schematu aksjomatu przypisania.

Aksjomat przypisania zaproponowany przez Hoare'a nie ma zastosowania, gdy więcej niż jedna nazwa może odnosić się do tej samej przechowywanej wartości. Na przykład,

${\ Displaystyle \ {y = 3 \} x: = 2 \ {y = 3 \}}$

jest błędne, jeśli x i y odnoszą się do tej samej zmiennej ( aliasing ), chociaż jest to właściwe wystąpienie schematu aksjomatu przypisania (z obiema i bytem ). ${\ Displaystyle \ {P \}}$${\ Displaystyle \ {P [2/x] \}}$${\ Displaystyle \ {y = 3 \}}$

Zasada kompozycji

Weryfikacja kodu wymiany bez zmiennych pomocniczych

Trzy poniższe stwierdzenia (wiersz 2, 4, 6) wymieniają wartości zmiennych a i b , bez potrzeby stosowania zmiennej pomocniczej. W dowodzie weryfikacyjnym początkowa wartość a i b jest oznaczona odpowiednio przez stałe A i B . Dowód najlepiej czytać wstecz, zaczynając od wiersza 7; Na przykład, linia 5 uzyskuje się z linii 7, zastępując w (ekspresję docelowej linii 6), (źródło ekspresji w linii 6). Niektóre uproszczenia arytmetyczne są stosowane milcząco, a mianowicie. (wiersz 5→3) i (wiersz 3→1). ${\displaystyle ab}$${\displaystyle a-(ab)=b}$${\displaystyle a+bb=a}$ Nr Kod Asercje 1:       ${\ Displaystyle \ {a = A \ klin b = B \}}$ 2: ${\displaystyle a:=a+b;}$       3: ${\ Displaystyle \ {ab = A \ klin b = B \}}$ 4: ${\displaystyle b:=ab;}$ 5: ${\ Displaystyle \ {b = A \ klin ab = B \}}$ 6: ${\displaystyle a:=ab}$ 7: ${\ Displaystyle \ {b = A \ klin a = B \}}$

Reguła kompozycji Hoare'a dotyczy sekwencyjnie wykonywanych programów S i T , gdzie S wykonuje się przed T i jest zapisywane ( Q jest nazywane stanem pośrednim ): ${\displaystyle S;T}$

${\displaystyle {\dfrac {\{P\}S\{Q\}\quad,\quad \{Q\}T\{R\}}{\{P\}S;T\{R\}} }}$

Rozważmy na przykład następujące dwa przypadki aksjomatu przypisania:

${\ Displaystyle \ {x + 1 = 43 \} y: = x + 1 \ {y = 43 \}}$

oraz

${\ Displaystyle \ {y = 43 \} z: = y \ {z = 43 \}}$

Z reguły sekwencjonowania wnioskuje się:

${\ Displaystyle \ {x + 1 = 43 \} y: = x + 1; z: = y \ {z = 43 \}}$

Kolejny przykład pokazano w prawym polu.

Reguła warunkowa

${\ Displaystyle {\ dfrac {\ {B \ klin P \} S \ {Q \} \ quad, \ quad \ {\ neg B \ klin P \} T \ {Q \}} {\ {P \} \texttt {if}}\ B\ {\texttt {wtedy}}\ S\ {\texttt {else}}\ T\ {\texttt {endif}}\{Q\}}}}$

Reguła warunkowa mówi, że warunek końcowy Q wspólny dla części then i else jest również warunkiem końcowym całości instrukcji if...endif . W części then i else , nienegowany i zanegowany warunek B można dodać do warunku wstępnego P , odpowiednio. Warunek B nie może mieć skutków ubocznych. Przykład podano w następnej sekcji .

Ta zasada nie była zawarta w oryginalnej publikacji Hoare'a. Jednak skoro oświadczenie

${\displaystyle {\texttt {jeżeli}}\ B\ {\texttt {wtedy}}\ S\ {\texttt {inny}}\ T\ {\texttt {endif}}}$

ma taki sam efekt jak konstrukcja z jednorazową pętlą

${\displaystyle {\texttt {bool}}\ b:={\texttt {prawda}};{\texttt {podczas}}\ b\klin b\ {\texttt {do}}\ S;b:={\ texttt {false}}\ {\texttt {wykonane}};b:={\texttt {prawda}};{\texttt {gdy}}\ \neg B\wedge b\ {\texttt {wykonaj}}\ T; b:={\texttt {fałsz}}\ {\texttt {gotowe}}}$

reguła warunkowa może być wyprowadzona z innych reguł Hoare. W podobny sposób reguły dla innych konstrukcji programów pochodnych, takich jak for loop, do...until loop, switch , break , continue mogą zostać zredukowane przez transformację programu do reguł z oryginalnego artykułu Hoare'a.

Reguła konsekwencji

${\displaystyle {\dfrac {P_{1}\rightarrow P_{2}\quad,\quad \{P_{2}\}S\{Q_{2}\}\quad,\quad Q_{2}\rightarrow Q_{1}}{\{P_{1}\}S\{Q_{1}\}}}}$

Ta zasada pozwala wzmocnić warunek wstępny i/lub osłabić warunek końcowy . Służy np. do osiągnięcia dosłownie identycznych warunków końcowych dla części „ teraz” i „ inna” . ${\displaystyle P_{2}}$${\displaystyle Q_{2}}$

Na przykład dowód

${\displaystyle \{0\leq x\leq 15\}{\texttt {jeśli}}\ x<15\ {\texttt {wtedy}}\ x:=x+1\ {\texttt {inaczej}}\ x :=0\ {\texttt {endif}}\{0\leq x\leq 15\}}$

musi zastosować regułę warunkową, co z kolei wymaga udowodnienia

${\ Displaystyle \ {0 \ równoważnik x \ równoważnik 15 \ klin x <15 \} x: = x + 1 \ {0 \ równoważnik x \ równoważnik 15 \}}$lub uproszczony

${\ Displaystyle \ {0 \ równoważnik x <15 \} x: = x + 1 \ {0 \ równoważnik x \ równoważnik 15 \}}$

dla ówczesnej części i

${\ Displaystyle \ {0 \ równoważnik x \ równoważnik 15 \ klin x \ geq 15 \} x: = 0 \ {0 \ równoważnik x \ równoważnik 15 \}}$lub uproszczony

${\ Displaystyle \ {x = 15 \} x: = 0 \ {0 \ równoważnik x \ równoważnik 15 \}}$

do innego części.

Jednak reguła przypisania dla części then wymaga wybrania P jako ; zastosowanie reguły daje zatem plony ${\displaystyle 0\leq x\leq 15}$

${\ Displaystyle \ {0 \ równoważnik x + 1 \ równoważnik 15 \} x: = x + 1 \ {0 \ równoważnik x \ równoważnik 15 \}}$, co jest logicznie równoważne

${\ Displaystyle \ {-1 \ równoważnik x <15 \} x: = x + 1 \ {0 \ równoważnik x \ równoważnik 15 \}}$.

Reguła konsekwencji jest potrzebna do wzmocnienia warunku wstępnego uzyskanego z reguły przypisania do wymaganego dla reguły warunkowej. ${\displaystyle \{-1\leq x<15\}}$${\displaystyle \{0\leq x<15\}}$

Podobnie, w przypadku innego części, wydajność zasada przyporządkowanie

${\ Displaystyle \ {0 \ równoważnik 0 \ równoważnik 15 \} x: = 0 \ {0 \ równoważnik x \ równoważnik 15 \}}$lub równoważnie

${\ Displaystyle \ {{\ texttt {prawda}} \} x: = 0 \ {0 \ równoważnik x \ równoważnik 15 \}}$,

stąd reguła konsekwencji musi być zastosowana odpowiednio z i byciem i , aby ponownie wzmocnić warunek wstępny. Nieformalnie, efektem reguły konsekwencji jest „zapomnienie”, że jest to znane przy wejściu do części else , ponieważ reguła przypisania używana dla części else nie potrzebuje tych informacji. ${\displaystyle P_{1}}$${\displaystyle P_{2}}$${\ Displaystyle \ {x = 15 \}}$${\displaystyle \{{\texttt {prawda}}\}}$${\ Displaystyle \ {x = 15 \}}$

Podczas gdy reguła

${\displaystyle {\dfrac {\{P\klin B\}S\{P\}}{\{P\}{\texttt {podczas}}\ B\ {\texttt {do}}\ S\ {\ texttt {gotowe}}\{\neg B\klin P\}}}}$

Tutaj P jest niezmiennikiem pętli , który ma być zachowany przez ciało pętli S . Po zakończeniu pętli ten niezmiennik P nadal obowiązuje, a ponadto musiał spowodować zakończenie pętli. Podobnie jak w regule warunkowej, B nie może mieć skutków ubocznych. ${\ Displaystyle \ neg B}$

Na przykład dowód

${\ Displaystyle \ {x \ leq 10 \} {\ texttt {podczas}} \ x <10 \ {\ texttt {zrobić}} \ x: = x + 1 \ {\ texttt {gotowe}} \ {\ neg x <10\klin x\leq 10\}}$

reguła while wymaga udowodnienia

${\ Displaystyle \ {x \ równoważnik 10 \ klin x <10 \} x: = x + 1 \ {x \ równoważnik 10 \}}$lub uproszczony

${\ Displaystyle \ {x <10 \} x: = x + 1 \ {x \ równ 10 \}}$,

co można łatwo uzyskać dzięki regule przypisania. Na koniec warunek końcowy można uprościć do . ${\displaystyle \{\neg x<10\klin x\leq 10\}}$${\ Displaystyle \ {x = 10 \}}$

Na przykład reguła while może być użyta do formalnej weryfikacji następującego dziwnego programu w celu obliczenia dokładnego pierwiastka kwadratowego x dowolnej liczby a — nawet jeśli x jest zmienną całkowitą, a a nie jest liczbą kwadratową:

${\displaystyle \{{\texttt {prawda}}\}{\texttt {podczas}}\ x\cdot x\neq a\ {\texttt {do}}\ {\texttt {pomiń}}\ {\texttt { gotowe}}\{x\cdot x=a\klin {\texttt {prawda}}\}}$

Po zastosowaniu reguły while, w której P jest prawdziwe , pozostaje do udowodnienia

${\displaystyle \{{\texttt {prawda}}\klin x\cdot x\neq a\}{\texttt {pomiń}}\{{\texttt {prawda}}\}}$,

co wynika z reguły pomijania i reguły konsekwencji.

W rzeczywistości, dziwny program jest częściowo poprawna: jeśli to się stało, aby zakończyć, pewne jest, że x musi być zawarta (przez przypadek) wartość a „s pierwiastka kwadratowego. We wszystkich innych przypadkach nie wygaśnie; dlatego nie jest całkowicie poprawne.

Choć zasada całkowitej poprawności

W przypadku zastąpienia powyższej reguły zwykłego while następującą, rachunek Hoare'a może być również wykorzystany do wykazania poprawności całkowitej , tj. terminacji, jak również poprawności częściowej. Zwykle zamiast nawiasów klamrowych używa się nawiasów kwadratowych, aby wskazać inne pojęcie poprawności programu.

${\displaystyle {\dfrac {<\ {\text{jest dobrze ugruntowanym porządkowaniem na planie}}\ d\quad,\quad [P\klin B\t klina\w D\t klina = z]S[ P\klin t\in D\klin t<z]}{[P\klin t\in D]{\texttt {gdy}}\ B\ {\texttt {do}}\ S\ {\texttt {wykonane} }[\neg B\klin P\klin t\w D]}}}$

W tej regule, oprócz zachowania niezmiennika pętli, udowadnia się również zakończenie za pomocą wyrażenia t , zwanego wariantem pętli , którego wartość ściśle maleje ze względu na ugruntowaną relację < na pewnym zbiorze domen D podczas każdej iteracji. Ponieważ < jest dobrze ugruntowane, ściśle malejący łańcuch elementów D może mieć tylko skończoną długość, więc t nie może się zmniejszać w nieskończoność. (Na przykład, zwykły porządek < jest dobrze ufundowany na dodatnich liczbach całkowitych , ale ani na liczbach całkowitych, ani na dodatnich liczbach rzeczywistych ; wszystkie te zbiory są rozumiane w sensie matematycznym, a nie obliczeniowym, wszystkie są w szczególności nieskończone.) ${\ Displaystyle \ mathbb {N}}$${\ Displaystyle \ mathbb {Z}}$ ${\ Displaystyle \ mathbb {R} ^ {+}}$

Ze względu na niezmienny pętli P , warunek B musi oznaczać, że t nie jest minimalna elementu z D , inaczej ciało S nie może zmniejszyć ţ dalej, to założenie reguły byłoby błędne. (Jest to jeden z różnych zapisów zapewniających całkowitą poprawność.)

Wznowienie pierwszego przykładu z poprzedniej sekcji , dla dowodu całkowitej poprawności

${\displaystyle [x\leq 10]{\texttt {podczas}}\ x<10\ {\texttt {zrobić}}\ x:=x+1\ {\texttt {gotowe}}[\neg x<10\ klin x\leq 10]}$

regułę while dla całkowitej poprawności można zastosować, gdzie np. D jest nieujemnymi liczbami całkowitymi o zwykłej kolejności, a wyrażenie t jest , co z kolei wymaga udowodnienia ${\ Displaystyle 10-x}$

${\ Displaystyle [x \ leq 10 \ klin x <10 \ klin 10-x \ geq 0 \ klin 10-x = z] x: = x + 1 [x \ leq 10 \ klin 10-x \ geq 0 \ klin 10-x<z]}$

Mówiąc nieformalnie, musimy udowodnić, że odległość zmniejsza się w każdym cyklu pętli, podczas gdy zawsze pozostaje nieujemna; proces ten może trwać tylko przez skończoną liczbę cykli. ${\ Displaystyle 10-x}$

Poprzedni cel dowodowy można uprościć do:

${\displaystyle [x<10\klin 10-x=z]x:=x+1[x\leq 10\klin 10-x<z]}$,

co można udowodnić w następujący sposób:

${\displaystyle [x+1\leq 10\klin 10-x-1<z]x:=x+1[x\leq 10\klin 10-x<z]}$ jest uzyskiwany przez regułę przypisania, oraz

${\displaystyle [x+1\leq 10\klin 10-x-1<z]}$może być wzmocniony przez regułę konsekwencji.${\displaystyle [x<10\klin 10-x=z]}$

W przypadku drugiego przykładu z poprzedniej sekcji oczywiście nie można znaleźć wyrażenia t, które jest zmniejszane przez pustą treść pętli, dlatego nie można udowodnić zakończenia.

Zobacz też

• Asercja (informatyka)
• Komunikowanie procesów sekwencyjnych
• Projekt według umowy
• Semantyka denotacyjna
• Logika dynamiczna
• Edsger W. Dijkstra
• Niezmienność pętli
• Semantyka transformatora predykatów
• Weryfikacja programu
• Rachunek doprecyzowania
• Logika separacji
• Rachunek sekwencyjny
• Statyczna analiza kodu

Uwagi

Bibliografia

Dalsza lektura

• Roberta D. Tennenta. Specyfikowanie oprogramowania (podręcznik zawierający wprowadzenie do logiki Hoare'a, napisany w 2002 r.) ISBN  0-521-00401-2

Linki zewnętrzne

• KEY-Hoare jest półautomatyczny system weryfikacji zbudowany na szczycie klucz twierdzenie Prover. Zawiera rachunek Hoare'a dla prostego języka.
• j-Algo-modul Hoare calculus — Wizualizacja rachunku Hoare'a w programie do wizualizacji algorytmów j-Algo