Jak trudno jest zredukować terminację do częściowej poprawności?

Jeśli jesteś zaznajomiony z weryfikacją programu, prawdopodobnie wolisz przeczytać pytanie przed tłem . Jeśli nie jesteś zaznajomiony z weryfikacją programu, być może nadal będziesz w stanie odpowiedzieć na to pytanie, ale prawdopodobnie wolisz najpierw przeczytać tło .

tło

Często mówi się, że sprawdzenie częściowej poprawności jest nierozstrzygalne. Dla celów dyskusji wybierzmy jeden bardzo konkretny sposób, aby to stwierdzenie było precyzyjne, w stylu Floyda - Hoare. Flowgraph jest digrafu z wybitnym początkowego węzła , z których wszystkie węzły są osiągalne. Program jest flowgraph którego węzły są polecenia. Istnieją trzy typy założeń komend (1), które zakładają q , (2) twierdzenia potwierdzają q i (3) przypisania v: = e. Tutaj q jest formułą fol (logika pierwszego rzędu), e jest terminem fol, a v jest zmienną.

Mówimy, że program jest częściowo poprawny, gdy istnieje sposób na adnotację każdego węzła x warunkiem wstępnym a (x) i warunkiem dodatkowym b (x), tak że (1) warunek początkowy węzła jest prawidłowy, (2) { a (x) } x { b (x) } obowiązuje dla wszystkich poleceń x , a (3) ( b (x) oznacza, że (y) ) jest ważne dla wszystkich krawędzi od x do y . Tutaj tróje Hoare są zdefiniowane następująco:

• { p } assert q { r } oznacza, że ​​( p oznacza ( q i r )) jest prawidłowe
• { p } zakładamy, że q { r } oznacza, że ​​(( p i q ) oznacza, że r ) jest poprawny
• { S } v: = E { R } oznacza, że (( P z E zastąpiono v ) wynika, R ) jest ważna

Oto falisty argument, dlaczego sprawdzenie tej częściowej poprawności jest nierozstrzygalne: Po wypełnieniu niektórych a (x) i niektórych b (x) należy sprawdzić, czy niektóre formuły fol są poprawne, a to jest nierozstrzygalne.

Typowym sposobem zakodowania zakończenia w częściowej poprawności jest dodanie pewnych specjalnych stwierdzeń, które zasadniczo mówią „od ostatniego wykonania mnie postęp był postępujący w kierunku zakończenia”. Te asercje postępu muszą być umieszczone w taki sposób, aby wszystkie nieskończone spacery po schemacie blokowym (rozpoczynające się w węźle początkowym) zawierały nieskończenie wiele asercji postępu. Mówiąc ściślej, powiedzmy, że asercje postępu mają zawsze formę aser u < v , gdzie u i v są dodatnimi liczbami całkowitymi, są poprzedzone przypisaniem u : = f , a po nich następuje przypisanie v : = u . Tutaj f jest afunkcja wariantu , u to jej bieżąca wartość, a v to jej poprzednia wartość. Teraz, gdy mówimy o „dodatnich liczbach całkowitych” i porównujemy je, musimy upewnić się, że dostępna jest nieco więcej niż folia: powiedzmy, że arytmetyka Peano jest dostępna. (Nie podoba mi się ten wybór. Możesz zignorować, jeśli jest to wygodne.) Oczywiście, f może korzystać z innych funkcji i stałych wymienionych w programie. (Zauważ, że dodanie założeń na początku programu jest równoważne z wprowadzeniem nielogicznych aksjomatów.)

Teraz, jeśli program z zapewnieniami postępu jest nadal częściowo poprawny, to wiemy, że oryginalny program się kończy.

Pytanie

Biorąc pod uwagę program kończący, wydaje się, że wymyślenie różnych funkcji dla asercji postępu jest trudne. Ale jak ciężko? (Wiem, że nawet przy powyższym ogromnym tle nadal pozostawiłem to pytanie trochę otwarte lub źle zdefiniowane, w zależności od tego, jak chcesz na nie spojrzeć.)

Innymi słowy: szukam odniesienia, które sformalizuje problem sprowadzenia terminacji do częściowej poprawności, a następnie powie coś o jego złożoności. Odpowiedź, która robi to wszystko, byłaby oczywiście mile widziana.

Jednym ze sposobów rozwiązania tego problemu jest rozważenie złożoności obliczeniowej problemów decyzyjnych dla klas zapytań o częściową poprawność i zakończenie, o których wiadomo, że są rozstrzygalne. Interpretacja abstrakcyjna przy użyciu domeny wielościennej może wnioskować o adnotacjach częściowej poprawności, o których wspominasz, w przypadkach, gdy wymagane adnotacje są połączeniami nierówności liniowych. Obliczenie abstrakcyjnego warunku końcowego jest wykładnicze pod względem liczby zmiennych. Potem jest narzut związany ze znalezieniem stałego punktu. Zobacz wczesne artykuły Cousota, aby uzyskać więcej informacji na ten temat oraz bibliotekę fartuchów, jeśli chcesz grać z nią bezpośrednio.

Znalezienie funkcji wariantowych jest rozstrzygalne, gdy funkcje wariantowe są liniowe. Nie mogłem znaleźć pełnej charakterystyki złożoności tego, ale „Zakończenie programów liniowych” autorstwa Tiwari ma sekcję, która omawia złożoność. Zobacz także „Kompletną metodę syntezy liniowych funkcji rankingowych” Podelskiego i Rybalchenko. Ponadto Byron Cook wykonał prace nad wykorzystaniem abstrakcyjnej interpretacji, aby pomóc w konstruowaniu argumentów dotyczących zakończenia. Zobacz na przykład „Ranking abstrakcje” i „Analizy wariancji z analiz niezmienniczości”. Mogą one dać lepszy wgląd w związek między częściową poprawnością a zakończeniem.

Spinki do mankietów:

• http://www.csl.sri.com/users/tiwari/html/cav04.html
• http://www7.in.tum.de/~rybal/papers/vmcai04-linear-ranking.pdf
• http://www.dcs.qmul.ac.uk/~hyang/paper/esop08.pdf
• http://research.microsoft.com/terminator/popl07a.pdf

Widoczna redukcja z niezbędnego braku rozwiązania do częściowej poprawności, a mianowicie:

P nigdy się nie kończy, gdy jest uruchamiany w stanie początkowym spełniającym φ iff { φ } P {false} jest poprawny.

Zdaję sobie sprawę, że to kolejna brak odpowiedzi. Jego zaletą jest to, że jest krótszy niż te powyżej.

Istnieje standardowa technologia - zwykle nierozstrzygalna, oczywiście - do zapełniania wykresu warunkami wstępnymi i końcowymi, a mianowicie najsłabsza semantyka liberalnego warunku wstępnego , która jest formą semantyki transformatora predykatowego, która daje najsłabsze warunki wstępne dla spełnienia specyfikacji lub nie -zakończenie. Zasadniczo jest to pełna teoria częściowej poprawności dla takich języków, a nawet pełna poprawność

To kreda i ser decydują, które zakończenie i częściowa poprawność leży u podstaw ciężkiej pracy, ponieważ oba są tak bardzo nierozstrzygalne. Jednak częściowa poprawność jest związana z problemami związanymi z projektowaniem języka, zarówno dla języków programowania, jak i specyfikacji, podczas gdy trudność zakończenia jest czysta: dla każdej teorii zastosowanej do udowodnienia zakończenia istnieją algorytmy, które kończą się, ale udowodniono, że terminacja jest względna do tej teorii. Na przykład obliczenia w czystym polimorficznym rachunku lambda muszą się kończyć, ale arytmetyka Peano nie może tego udowodnić.

Mam wrażenie, że praca nad abstrakcyjną interpretacją zapoczątkowana przez Patricka Cousota była najbardziej dynamiczna w tej dziedzinie, ale nie udaję, że jestem ekspertem.