Jest to zapisane we wpisie wiki dotyczącym Symbolic Execution , ale nie mogę znaleźć żadnego odniesienia do niego. Czy ktoś może mi pokazać wskaźnik? Dziękuję Ci.
Jest to zapisane we wpisie wiki dotyczącym Symbolic Execution , ale nie mogę znaleźć żadnego odniesienia do niego. Czy ktoś może mi pokazać wskaźnik? Dziękuję Ci.
Odpowiedzi:
Nie znam artykułu poświęconego porównaniu symbolicznej realizacji z abstrakcyjną interpretacją. Nie uważam też, że taki jest potrzebny. Wystarczy przeczytać oryginalne opisy tych dwóch technik.
(I odwrotnie, jeśli byłoby jakieś nieoczekiwane połączenie, to byłoby to warte opisania. Ale bardzo wątpię, aby tak było.)
Główną ideą wykonania symbolicznego jest to, że w dowolnym punkcie wykonania można wyrażać wartości wszystkich zmiennych jako funkcje wartości początkowych. Główną ideą interpretacji abstrakcyjnej jest to, że można systematycznie badać wszystkie wykonania programu za pomocą serii nadmiernych przybliżeń. (Słyszę, jak kilku entuzjastów AI jęczy przy poprzednim przybliżeniu.)
Zatem przynajmniej w pierwotnym sformułowaniu symboliczne wykonanie nie dotyczyło zbadania wszystkich możliwych wykonań. Widać to nawet w tytule: zawiera słowo „testowanie”. Ale oto więcej z Sekcji 8: „W przypadku programów z nieskończonymi drzewami wykonania testowanie symboliczne nie może być wyczerpujące i nie można ustalić absolutnego dowodu poprawności”.
Natomiast abstrakcyjna interpretacja ma na celu zbadanie wszystkich egzekucji. W tym celu wykorzystuje kilka składników, z których jeden jest bardzo podobny do głównej idei symbolicznej realizacji. Składnikami tymi są (1) stany abstrakcyjne, (2) łączenie i poszerzanie (stąd „tytuł” w tytule).
Stany abstrakcyjne.Konkretny stan programu w danym momencie jest w zasadzie migawką zawartości pamięci (w tym samego kodu programu i licznika programu). Ma wiele szczegółów, które są trudne do wyśledzenia. Podczas analizowania określonej właściwości możesz zignorować duże części konkretnego stanu. Lub możesz chcieć dbać tylko o to, czy dana zmienna jest ujemna, zero lub dodatnia, ale nie przejmuj się jej dokładną wartością. Ogólnie rzecz biorąc, chcesz rozważyć abstrakcyjną wersję konkretnego stanu. Aby to zadziałało, musisz mieć właściwość komutatywności: Jeśli przyjmiesz konkretny stan, wykonasz instrukcję, a następnie wyodrębnisz stan wynikowy, powinieneś uzyskać taki sam wynik, jak gdyby wyodrębnić stan początkowy, a następnie wykonać to samo oświadczenie, ale w stanie abstrakcyjnym. Ten schemat przemienności pojawia się w obu artykułach. To jest wspólny pomysł. Ponownie, abstrakcyjna interpretacja jest bardziej ogólna, ponieważ nie narzuca ona abstrakcji państwa - po prostu mówi, że powinien istnieć sposób, aby to zrobić. Natomiast wykonanie symboliczne mówi, że używasz wyrażeń (symbolicznych), które wspominają wartości początkowe.
Łączenie i poszerzanie. Jeśli wykonanie programu osiągnie określoną instrukcję na dwa różne sposoby, wykonanie symboliczne nie próbuje połączyć dwóch analiz. Dlatego powyższy cytat mówi o drzewach egzekucji, a nie o dagach. Pamiętaj jednak, że abstrakcyjna interpretacja chce objąć wszystkie egzekucje. Dlatego prosi o sposób połączenia analiz dwóch wykonań w punkcie, w którym mają ten sam licznik programu. (Przyłączenie mogłobybądź bardzo głupi ({a} join {b} = {a, b}) tak, że sprowadza się to do tego, co robi symboliczne wykonanie.) Ogólnie, samo połączenie nie jest wystarczające, aby zagwarantować, że w końcu skończysz analizować wszystkie wykonania. (W szczególności wspomniane wcześniej głupie sprzężenie nie będzie działać.) Rozważmy program z pętlami: „n = input (); dla i w zakresie (n): dostuff ()”. Ile razy powinieneś ominąć pętlę i ciągle dołączać? Żadna stała odpowiedź nie działa. Potrzebne jest zatem coś innego, a to się poszerza , co można postrzegać jako heurystykę. Załóżmy, że obejrzałeś pętlę 3 razy i nauczyłeś się, że „i = 0 lub i = 1 lub i = 2”. Następnie powiesz: hmmm, ... poszerzmy się, a otrzymasz „i> = 0”. Ponownie abstrakcyjna interpretacja nie mówi, jak poszerzać - mówi tylko, jakie poszerzanie właściwości powinno się sprawdzić.
(Przepraszam za tę długą odpowiedź: naprawdę nie miałem czasu, aby ją skrócić).
Myślę, że ma to bardzo płytkie znaczenie. Pierwszym krokiem abstrakcyjnej interpretacji jest zidentyfikowanie konkretnej semantyki kolekcjonowania. Zamiast opisywać ewolucję pojedynczego stanu, zbieranie semantyki opisuje ewolucję zbiorów stanów. Ponieważ symboliczne wykonanie powoduje o reprezentacjach zbiorów stanów, można argumentować, że reprezentuje ono konkretną semantykę programu. Nie wiem, czy opracowywana jest dokładniejsza korespondencja.
Zobacz Patrick Cousot. Metody opracowywania i aproksymacji punktów fixes d'opérateurs monotones sur un treillis, analizowanie sémantique des programów (Iteracyjne metody konstruowania i aproksymacji punktów stałych operatorów monotonicznych na sieciach, analiza statyczna programu). Thèse ès Sciences Mathématiques, Université Joseph Fourier, Grenoble, Francja, 21 marca 1978 r. Https://cs.nyu.edu/~pcousot/publications.www/CousotTheseEsSciences1978.pdf (niestety w języku francuskim), strona (3) -27 do (3) -29