Logic of Hoare: Różnice pomiędzy wersjami
(Utworzono nową stronę "Paper of R.W. Floyd brought some light on proving programs correct. Later C.A.R. Hoare proposed another formalization based on the ideas of Floyd. S. Cook addressed the...") |
|||
| Linia 4: | Linia 4: | ||
In the light of the paper [{{Odn|ref=nie|Goraj, Mirkowska, Paluszkiewicz}}] this theorem is unnecessary. Theorem 5 of this paper states that notions of feasible and of acceptable description of program coincide. In other words if a verification condition of a program is valid in all models of a theory then it is provable from the axioms of the theory. For the details see [{{Odn |ref=nie |AL4software }}] sections on Floyd's descriptions of programs and Hoare's logic of partial correctness. | In the light of the paper [{{Odn|ref=nie|Goraj, Mirkowska, Paluszkiewicz}}] this theorem is unnecessary. Theorem 5 of this paper states that notions of feasible and of acceptable description of program coincide. In other words if a verification condition of a program is valid in all models of a theory then it is provable from the axioms of the theory. For the details see [{{Odn |ref=nie |AL4software }}] sections on Floyd's descriptions of programs and Hoare's logic of partial correctness. | ||
| + | |||
| + | === ''Czy logika Hoare'a nie jest narzędziem lepszym od logiki algorytmicznej?'' === | ||
| + | :1. Po pierwsze, logika Hoare'a jest fragmentem logiki algorytmicznej. By się o tym przekonać wystarczy zaobserwować, że <br/> | ||
| + | ::a) "trójki" w rachunku Hoare'a czyli formuły postaci <math> \{\alpha\} K \{\beta\} </math> wyrażają to samo co formuły logiki algorytmicznej postaci <math> (\alpha \land K\,\mathbb{1}) \Rightarrow K \beta </math>, tj. własność semantycznej częściowej poprawności programu <math>K</math> względem warunku początkowego <math> \alpha </math> i warunku końcowego <math> \beta </math>, ponadto <br/> | ||
| + | ::b) każda reguła rachunku Hoare's jest wywodliwa (posiada dowód) w logice algorytmicznej zob [{{Odn|ref=nie|LogProg2}}] str. 250-260.<br/> | ||
| + | :2. Język logiki Hoare'a nie ma środków do wyrażania pozostałych ważnych praktycznie własności semantycznch programów np. stop, całkowita poprawność, równoważność, etc. <br /> | ||
| + | :3. Istnieją próby zmodyfikowania logiki Hoare'a w taki sposób by można było formułować własność całkowitej poprawności i dowodzić jej. Zob. książka Apt, de Boer i Olderog. Zauważmy jednak, że przyjęte w tym celu reguły wnioskowania mają sens tylko w dziedzinach arytmetycznych (tj. takich w których prawdziwa jest własność Archimedesa), w wielu istotnych dla informatyki strukturach danych np. stosy, kolejki, drzewa, kopce, etc. podejście takie jest nie do powtórzenia.<br /> | ||
| + | :4. Powyższe uwagi mozna wypowiedzieć nieco ogólniej, logika Hoare'a nie wydaje się dobrą podstawą do rozwijania teorii struktur danych i w związku z tym nie rokuje nadziei na zastosowanie w programowaniu obiektowym.<br /> | ||
| + | :5. Relatywna pełność logiki Hoare'a - czy to jest potrzebne? <br /> | ||
| + | System Hoare'a reguł wnioskowania o częściowej poprawności programów zbudowanych z instrukcji przypisania przy pomocy trzech konstrukcji programistycznych: składanie, instrukcja warunkowa oraz instrukcja while iteracji powstał wykorzystując wcześniejsza pracę R.W. Floyda (1967) i nie był wolny od błędów. Błędy te Hoare usuwał i co ważniejsze pokazywał, ze jego system może być wykorzystywany w dowodach częściowej poprawności programów np. quicksort. Nasuwało się kolejne pytanie: czy każda trójka wyrażająca prawdziwą własnośc częściowej poprawności posiada dowód w tym systemie. Na to pytanie S. Cook udzielił odpowiedzi w tzw. twierdzeniu o relatywnej pełności logiki Hoare'a: | ||
| + | |||
| + | Zauważmy, że parę lat wcześniej w pracy [[Media:GMP1970.pdf|Góraj,Mirkowska,Paluszkiewicz 1970]] udowodniono własność pełności systemu Floyda (zmodyfikowanego przez autorki)<br /> | ||
| + | |||
| + | '''Twierdzenie'''. Opis programu P jest akceptowalny w teorii T wtedy i tylko wtedy gdy opis ten jest dopuszczalny w każdym modelu tej teorii. | ||
| + | |||
| + | Tę sama treść zawiera twierdzenie udowodnione przez L. Banachowskiego [LB1] | ||
| + | Warunek weryfikacyjny VC programu P jest twierdzeniem teorii T wtedy i tylko wtedy gdy jest formułą prawdziwą w każdym modelu teorii T. | ||
| + | |||
| + | Jak porównać te dwa twierdzenia z twierdzeniem Cooka o relatywnej pełności. | ||
| + | Twierdzenie GMP mówi nam: jeśli znalazłeś właściwe formuły jako kandydatów na niezmienniki pętli to dowód częściowej poprawności sprowadza się do udowodnienia długiej koniunkcji formuł pierwsego rzędu. | ||
| + | |||
| + | Twierdzenie o relatywnej pełności ma nieco inną postać. Jeśli udowodnisz pewną liczbę formuł pierwszego rzędu to formuła wyrazająca własnośc częściowej poprawności posiada dowód. | ||
| + | |||
| + | Pozostają wątpliwości: rozpatrzmy algorytm Euklidesa. Jak wygląda dowód poprawności? | ||
| + | (ROZWIŃ) | ||
Aktualna wersja na dzień 19:30, 8 sie 2017
Paper of R.W. Floyd brought some light on proving programs correct. Later C.A.R. Hoare proposed another formalization based on the ideas of Floyd. S. Cook addressed the problem of completeness of Floyd-Hoare calculus and formulated the so called relative completeness theorem.
In the light of the paper [Goraj, Mirkowska, Paluszkiewicz ↓] this theorem is unnecessary. Theorem 5 of this paper states that notions of feasible and of acceptable description of program coincide. In other words if a verification condition of a program is valid in all models of a theory then it is provable from the axioms of the theory. For the details see [AL4software ↓] sections on Floyd's descriptions of programs and Hoare's logic of partial correctness.
Czy logika Hoare'a nie jest narzędziem lepszym od logiki algorytmicznej?
- 1. Po pierwsze, logika Hoare'a jest fragmentem logiki algorytmicznej. By się o tym przekonać wystarczy zaobserwować, że
- a) "trójki" w rachunku Hoare'a czyli formuły postaci [math] \{\alpha\} K \{\beta\} [/math] wyrażają to samo co formuły logiki algorytmicznej postaci [math] (\alpha \land K\,\mathbb{1}) \Rightarrow K \beta [/math], tj. własność semantycznej częściowej poprawności programu [math]K[/math] względem warunku początkowego [math] \alpha [/math] i warunku końcowego [math] \beta [/math], ponadto
- b) każda reguła rachunku Hoare's jest wywodliwa (posiada dowód) w logice algorytmicznej zob [LogProg2 ↓] str. 250-260.
- a) "trójki" w rachunku Hoare'a czyli formuły postaci [math] \{\alpha\} K \{\beta\} [/math] wyrażają to samo co formuły logiki algorytmicznej postaci [math] (\alpha \land K\,\mathbb{1}) \Rightarrow K \beta [/math], tj. własność semantycznej częściowej poprawności programu [math]K[/math] względem warunku początkowego [math] \alpha [/math] i warunku końcowego [math] \beta [/math], ponadto
- 2. Język logiki Hoare'a nie ma środków do wyrażania pozostałych ważnych praktycznie własności semantycznch programów np. stop, całkowita poprawność, równoważność, etc.
- 3. Istnieją próby zmodyfikowania logiki Hoare'a w taki sposób by można było formułować własność całkowitej poprawności i dowodzić jej. Zob. książka Apt, de Boer i Olderog. Zauważmy jednak, że przyjęte w tym celu reguły wnioskowania mają sens tylko w dziedzinach arytmetycznych (tj. takich w których prawdziwa jest własność Archimedesa), w wielu istotnych dla informatyki strukturach danych np. stosy, kolejki, drzewa, kopce, etc. podejście takie jest nie do powtórzenia.
- 4. Powyższe uwagi mozna wypowiedzieć nieco ogólniej, logika Hoare'a nie wydaje się dobrą podstawą do rozwijania teorii struktur danych i w związku z tym nie rokuje nadziei na zastosowanie w programowaniu obiektowym.
- 5. Relatywna pełność logiki Hoare'a - czy to jest potrzebne?
System Hoare'a reguł wnioskowania o częściowej poprawności programów zbudowanych z instrukcji przypisania przy pomocy trzech konstrukcji programistycznych: składanie, instrukcja warunkowa oraz instrukcja while iteracji powstał wykorzystując wcześniejsza pracę R.W. Floyda (1967) i nie był wolny od błędów. Błędy te Hoare usuwał i co ważniejsze pokazywał, ze jego system może być wykorzystywany w dowodach częściowej poprawności programów np. quicksort. Nasuwało się kolejne pytanie: czy każda trójka wyrażająca prawdziwą własnośc częściowej poprawności posiada dowód w tym systemie. Na to pytanie S. Cook udzielił odpowiedzi w tzw. twierdzeniu o relatywnej pełności logiki Hoare'a:
Zauważmy, że parę lat wcześniej w pracy Góraj,Mirkowska,Paluszkiewicz 1970 udowodniono własność pełności systemu Floyda (zmodyfikowanego przez autorki)
Twierdzenie. Opis programu P jest akceptowalny w teorii T wtedy i tylko wtedy gdy opis ten jest dopuszczalny w każdym modelu tej teorii.
Tę sama treść zawiera twierdzenie udowodnione przez L. Banachowskiego [LB1] Warunek weryfikacyjny VC programu P jest twierdzeniem teorii T wtedy i tylko wtedy gdy jest formułą prawdziwą w każdym modelu teorii T.
Jak porównać te dwa twierdzenia z twierdzeniem Cooka o relatywnej pełności. Twierdzenie GMP mówi nam: jeśli znalazłeś właściwe formuły jako kandydatów na niezmienniki pętli to dowód częściowej poprawności sprowadza się do udowodnienia długiej koniunkcji formuł pierwsego rzędu.
Twierdzenie o relatywnej pełności ma nieco inną postać. Jeśli udowodnisz pewną liczbę formuł pierwszego rzędu to formuła wyrazająca własnośc częściowej poprawności posiada dowód.
Pozostają wątpliwości: rozpatrzmy algorytm Euklidesa. Jak wygląda dowód poprawności? (ROZWIŃ)
