Próbuję nauczyć się różnych podejść do weryfikacji oprogramowania. Przeczytałem kilka artykułów. O ile się dowiedziałem, logika zdaniowa z temporalnym na ogół wykorzystuje sprawdzanie modelu za pomocą solverów SAT (w systemach trwających - reaktywnych), ale co z logiką pierwszego rzędu z temporalną? Czy wykorzystuje dowody twierdzeń? Czy może również używać SAT?
Wszelkie wskazówki do książek lub artykułów dla początkujących w tej sprawie są bardzo mile widziane.
Odpowiedzi:
Logika pierwszego rzędu jest nierozstrzygalna, więc rozwiązywanie SAT naprawdę nie pomaga. To powiedziawszy, istnieją techniki sprawdzania modeli ograniczonych formuł pierwszego rzędu. Oznacza to, że przy ustalaniu, czy formuła jest prawdziwa czy fałszywa, można brać pod uwagę tylko określoną liczbę obiektów. Oczywiście nie jest to kompletne, ale jeśli zostanie znaleziony kontrprzykład, to naprawdę jest on kontrprzykładem.
Narzędzie Stop to jedno narzędzie, które pozwala opisywać modele w logice pierwszego rzędu (chociaż składnia powierzchni oparta jest na modelach relacyjnie opisanych) i wykorzystuje sprawdzanie modeli ograniczonych w celu znalezienia rozwiązań. Solver SAT jest używany pod maską. Jedno rozszerzenie stopu pozwala na modele o charakterze czasowym, choć technicznie nie obsługuje logiki czasowej.
Jeśli chcesz dalej badać, na przykład, aby zweryfikować poprawność programu, możesz spojrzeć na narzędzia do weryfikacji programu. Zasadniczo opierają się one na logice Hoare'a (do rozumowania warunków wstępnych i następczych), ewentualnie rozszerzonej o logikę separacji (do rozumowania o hałdach). Te logiki są na ogół nierozstrzygalne, dlatego wymagana jest pewna interakcja między człowiekiem a narzędziem weryfikacji. Niektóre przykładowe narzędzia to:
źródło
Po przeczytaniu twojego pytania jedynym sposobem, w jaki mogłem zobaczyć i mieć wystarczającą wiedzę, aby powiązać ze sobą tematy, było przekazanie zestawu artykułów na wysokim poziomie, które przechodzą od weryfikacji oprogramowania, kończąc na próbie połączenia sprawdzania modelu i dowodzenia twierdzeń. Mam nadzieję, że mój komentarz to zrobił:
Spójrz na weryfikację oprogramowania, następnie weryfikację formalną, a następnie kontrolę modelu i formalną weryfikację oprogramowania: kontrola modelu i sprawdzanie twierdzeń
Dave udzielił dobrej odpowiedzi, na którą nie mogę zrobić więcej sprawiedliwości w pierwszej części pytania niż Dave, ponieważ jestem w tym również nowy.
Ponieważ jest to twoje pierwsze pytanie na stronie SE , powodem, dla którego nie dałem odpowiedzi, ale komentarz, jest to, że tutaj odpowiedź nie może być tylko zbiorem linków, ale musi dać pisemną odpowiedź i użyć linków na poparcie odpowiedzi; stąd komentarz zamiast odpowiedzi.
Z pozdrowieniami dla:
Książki, które polecam i których używam to:
Logika w informatyce - modelowanie i rozumowanie dotyczące systemów 2nd Ed. autor: Huth i Ryan Wprowadza to logikę i przechodzi do sprawdzania modelu, ale nie przechodzi do dowodzenia twierdzeń. Powinno to obejmować wszystkie podstawowe pytania związane z logiką i sprawdzaniem modelu.
Zasady sprawdzania modeli przez Baiera i Katoena Właśnie zacząłem czytać ten i jest to o wiele lepsze niż czytanie wielu artykułów i próba sprawdzenia, jak wszystkie one do siebie pasują. Jest to jedna z najbardziej, jeśli nie najbardziej zalecana książka na temat sprawdzania modelu. Powinien odpowiedzieć na bardziej zaawansowane pytania dotyczące sprawdzania modelu.
Logika czasowa i systemy stanowe Krogera i Merza Często lubię mieć książki różnych autorów podczas samodzielnego uczenia się przedmiotu. Ten ma uzupełnić / uzupełnić „Zasady sprawdzania modelu”
Podręcznik praktycznej logiki i automatycznego rozumowania Harrison Będąc programistą Nie mogę wystarczająco polecić tej książki. Książka zaczyna się od wprowadzenia logiki i przechodzi przez etap tworzenia jądra dla dowcipnisia opartego na pracy HOL Light . Żeby podkreślić, że książka używa działającego kodu OCaml, wyjaśnia te twierdzenia w kategoriach, które uważam za przyjazne, i daje ci to, co musisz wiedzieć, ale nie tak bardzo, że nie możesz nawiązać połączenia ani poczuć, że biegniesz w dół. If jest bardzo skoncentrowaną książką na temat przejścia od logiki do określonego rodzaju twierdzenia twierdzącego.
Jak to udowodnić: ustrukturyzowane podejście Vellemana Aby dostać się do asystentów Proof dla twierdzenia dowodzącego, że będziesz musiał żyć i spać twierdzenia.
Wprowadzenie do dowodów i języka matematycznego według dnia Jest to bezpłatna książka, która nie tylko uzupełnia „Jak to udowodnić”, ale w sumie wykracza poza nią. Nie zdziwiłbym się, gdy ten stał się popularny.
W chwili obecnej nie mogę rozwinąć więcej o dowodzeniu twierdzeń, ponieważ wciąż uczę się zalet / wad i różnic każdego z nich, ale te, na których się skupiam, to
Isabelle, ponieważ opiera się na unifikacji wyższego rzędu.
Ci asystenci ds. Proofów zazwyczaj mają także książki, są aktualni, popularni, mają otwarte oprogramowanie, utrzymują i mają aktywne społeczności wsparcia.
Uwaga: Użyłem worldcat.org, aby odnieść się do książek, ale możesz je przejrzeć za pomocą funkcji Amazon zajrzyj do środka.
źródło