Wprowadzenie do weryfikacji logicznej pierwszego rzędu

9

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.

FELIPE N.
źródło
2
Przede wszystkim witamy w CS: SE. Chociaż nie jestem w tym ekspertem, wydajesz się chwytać kilka tematów naraz, pozostawiając wiele dziur. Nie martw się; Ciągle to robię. Spójrz na weryfikację oprogramowania, a następnie weryfikację formalną, a następnie kontrolę modelu i formalną weryfikację oprogramowania: sprawdzanie modelu i sprawdzanie twierdzeń
Guy Coder

Odpowiedzi:

9

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:

Dave Clarke
źródło
10

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:

Wszelkie wskazówki do książek lub artykułów dla początkujących w tej sprawie są bardzo mile widziane.

Książki, które polecam i których używam to:

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

  • HOL Light dzięki książce Johna Harrisona.
  • Coq, ponieważ opiera się na rachunku konstrukcji
  • 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.

Guy Coder
źródło
Aby uniknąć wielu zmian w odpowiedzi, dodam dodane informacje jako komentarze, a następnie w przyszłości będę je dodawać do odpowiedzi. Za próbę rozwiązania wielu podobieństw i różnic między asystentami dowodu. Google dla Freek Wiedijk; Uważam, że jego papiery są bardzo przydatne.
Guy Coder,
Bardzo dziękuję za szczegółową i dokładną odpowiedź. Za dodawanie komentarzy do książek i link do bezpłatnej książki. Znów nie mogę ci wystarczająco podziękować :-)
FELIPE N.