Ich versuche mir verschiedene Ansätze zur Softwareüberprüfung beizubringen. Ich habe einige Artikel gelesen. Soweit ich gelernt habe, verwendet die Aussagenlogik mit Zeit im Allgemeinen die Modellprüfung mit SAT-Lösern (in laufenden - reaktiven Systemen), aber was ist mit der Logik erster Ordnung mit Zeit? Verwendet es Theorembeweiser? Oder kann es auch SAT verwenden?
Hinweise auf Bücher oder Artikel für Anfänger in dieser Angelegenheit werden sehr geschätzt.
Antworten:
Die Logik erster Ordnung ist unentscheidbar, daher hilft die SAT-Lösung nicht wirklich. Es gibt jedoch Techniken zur begrenzten Modellprüfung von Formeln erster Ordnung. Dies bedeutet, dass nur eine feste Anzahl von Objekten berücksichtigt werden kann, wenn versucht wird, festzustellen, ob die Formel wahr oder falsch ist. Dies ist natürlich nicht vollständig, aber wenn ein Gegenbeispiel gefunden wird, ist es wirklich ein Gegenbeispiel.
Das Tool Alloy ist ein Tool, mit dem Modelle in Logik erster Ordnung beschrieben werden können (obwohl die Oberflächensyntax auf relational beschriebenen Modellen basiert) und die begrenzte Modellprüfung verwendet, um Lösungen zu finden. Unter der Haube wird ein SAT-Löser verwendet. Eine Legierungserweiterung ermöglicht Modelle mit zeitlichem Charakter, obwohl sie technisch keine zeitliche Logik unterstützt.
Wenn Sie beispielsweise die Programmkorrektheit weiter untersuchen möchten, können Sie sich die Tools zur Programmüberprüfung ansehen. Diese basieren im Allgemeinen auf der Hoare-Logik (zum Nachdenken über Vor- und Nachbedingungen), möglicherweise erweitert um die Trennungslogik (zum Nachdenken über Haufen). Diese Logiken sind im Allgemeinen unentscheidbar, daher ist ein gewisses Maß an Interaktion zwischen dem Menschen und dem Verifizierungswerkzeug erforderlich. Einige Beispielwerkzeuge sind:
quelle
Nachdem ich Ihre Frage gelesen hatte, konnte ich nur sehen und hatte genug Wissen, um die Themen miteinander zu verknüpfen, indem ich eine Reihe von Artikeln auf hoher Ebene gab, die einen Drilldown von der Softwareüberprüfung durchführten und schließlich versuchten, Modellprüfung und Theoremprüfung zu vereinen. Hoffentlich hat mein Kommentar das getan:
Schauen Sie sich Software-Verifikation, dann Formale Verifikation, dann Modellprüfung und Formale Software-Verifikation an: Modellprüfung und Theoremprüfung
Dave hat eine gute Antwort gegeben, für die ich dem ersten Teil der Frage nicht viel mehr gerecht werden kann als Dave, da ich auch neu darin bin.
Da dies Ihre erste Frage auf einer SE- Site ist, habe ich keine Antwort, sondern einen Kommentar gegeben, weil eine Antwort hier nicht nur eine Reihe von Links sein kann, sondern eine schriftliche Antwort geben und Links zur Unterstützung der Antwort verwenden muss. also ein Kommentar statt einer Antwort.
In Bezug auf:
Bücher, die ich vorschlagen und verwenden würde, sind:
Logik in der Informatik - Modellierung und Argumentation über Systeme 2nd Ed. von Huth und Ryan Dies führt die Logik ein und geht zur Modellprüfung über, geht aber nicht auf die Theoremprüfung ein. Dies sollte also alle Ihre grundlegenden Fragen im Zusammenhang mit Logik und Modellprüfung abdecken.
Prinzipien der Modellprüfung von Baier und Katoen Ich habe gerade angefangen, diese zu lesen, und es ist viel besser, als viele Papiere zu lesen und zu versuchen, herauszufinden, wie sie alle zusammenpassen. Dies ist eines der am meisten, wenn nicht sogar am meisten empfohlenen Bücher zum Thema Modellprüfung. Es sollte Ihre erweiterten Fragen zur Modellprüfung beantworten.
Zeitliche Logik und Zustandssysteme von Kroger und Merz Ich habe oft Bücher von verschiedenen Autoren, wenn ich ein Thema selbst lerne. Dieser soll die "Prinzipien der Modellprüfung" ergänzen / abrunden.
Handbuch der praktischen Logik und des automatisierten Denkens von Harrison Als Programmierer kann ich dieses Buch nicht genug empfehlen. Das Buch beginnt mit der Einführung der Logik und geht den ganzen Weg durch die Erstellung des Kernels für einen Theorembeweiser, der auf der Arbeit von HOL Light basiert . Nur um hervorzuheben, dass das Buch funktionierenden OCaml-Code verwendet, die Theoreme in Begriffen erklärt, die ich für freundlich halte, und Ihnen das gibt, was Sie wissen müssen, aber nicht so viel, dass Sie keine Verbindung herstellen können oder das Gefühl haben, auf Nebengleisen zu laufen. If ist ein sehr fokussiertes Buch über den Übergang von der Logik zu einer bestimmten Art von Theorembeweis.
Wie man es beweist: Ein strukturierter Ansatz von Velleman Um in die Beweisassistenten für Theoreme einzusteigen, müssen Sie Theoreme leben und schlafen.
Eine Einführung in Beweise und die mathematische Umgangssprache bei Tag Dies ist ein kostenloses Buch, das nicht nur "Wie man es beweist" ergänzt, sondern darüber hinaus geht. Ich wäre nicht überrascht zu sehen, wie dieser populär wird.
Gegenwärtig kann ich nicht mehr auf Theorembeweise eingehen, weil ich immer noch die Vor- und Nachteile und Unterschiede jedes einzelnen lerne, aber diejenigen, auf die ich mich konzentriere, sind
Isabelle, weil es auf der Vereinigung höherer Ordnung basiert.
Diese Proof-Assistenten verfügen normalerweise auch über Bücher, sind aktuell, beliebt, Open Source, werden gepflegt und haben aktive Support-Communities.
Hinweis: Ich habe worldcat.org verwendet, um auf die Bücher zu verweisen, aber Sie können sie mithilfe der Look-Inside-Funktion von Amazon überprüfen.
quelle