Wenn formale Aspekte zum Erstellen von Code verwendet werden, gibt es eine generische Methode zum Bestimmen einer Schleifeninvariante oder wird sie je nach Problem völlig anders aussehen?Was ist der beste Weg, eine Schleifeninvariante zu bestimmen?
Es wurde bereits darauf hingewiesen, dass ein und dieselbe Schleife mehrere Invarianten haben kann, und dass Berechenbarkeit gegen Sie ist. Es bedeutet nicht, dass du es nicht versuchen kannst.
Sie sind in der Tat, auf der Suche nach einem induktiven invariant: dem Wort invariant auch für eine Eigenschaft verwendet werden, die bei jeder Iteration wahr ist, aber für die es nicht genug, um zu wissen, dass es bei einer Iteration halten zu folgern, dass es beim nächsten hält. Wenn I eine induktive Invariante ist, dann ist jede Konsequenz von I eine Invariante, aber möglicherweise keine induktive Invariante.
Sie versuchen wahrscheinlich, eine induktive Invariante zu erhalten, um eine bestimmte Eigenschaft (Nachbedingung) der Schleife unter bestimmten Bedingungen (Vorbedingungen) zu beweisen.
Es gibt zwei Heuristiken, die sehr gut funktionieren:
Start mit dem, was Sie haben (Vorbedingungen) und schwächen, bis Sie eine induktive invariant haben. Um eine Intuition zu erhalten, wie man schwächt, wenden Sie eine oder mehrere Vorwärtsschleifeniterationen an und sehen Sie, was in der Formel, die Sie haben, nicht mehr wahr ist.
Beginnen Sie mit dem, was Sie wollen (Nachbedingungen) und stärken Sie, bis Sie eine induktive Invariante haben. Um die Intuition zu stärken, wenden Sie eine oder mehrere Schleifeniterationen rückwärts an und sehen Sie, was hinzugefügt werden muss, damit die Nachbedingung abgeleitet werden kann.
Wenn der Computer möchten Sie in Ihrer Praxis helfen, kann ich die Jessie deduktiven Überprüfung Plug-in für C-Programme von Frama-C empfehlen. Es gibt andere, vor allem für Java und JML Annotationen, aber ich bin weniger vertraut mit ihnen. Das Ausprobieren der Invarianten, an die du denkst, ist viel schneller, als wenn du auf Papier arbeitest. Ich sollte darauf hinweisen, dass die Überprüfung, dass eine Eigenschaft eine induktive Invariante ist, auch unentscheidbar ist, aber moderne automatische Prüfer machen viele einfache Beispiele gut. Wenn Sie sich für diese Route entscheiden, holen Sie so viele wie möglich aus der Liste: Alt-ergo, Simplify, Z3.
Mit der optionalen (und etwas schwierig zu installierenden) Bibliothek Apron kann Jessie auch infer some simple invariants automatically.
Ich glaube nicht, dass es einfach ist, dies zu automatisieren. Aus wiki:
Aufgrund der grundlegenden Ähnlichkeit von Schleifen und rekursiven Programmen ist der Nachweis der teilweisen Korrektheit von Schleifen mit Invarianten dem Nachweis der Korrektheit rekursiver Programme über Induktion sehr ähnlich. Tatsächlich ist die Schleifeninvarianz oft die induktive Eigenschaft, die man von einem rekursiven Programm nachweisen muss, das einer gegebenen Schleife entspricht.
Danke, ich möchte es nicht automatisieren, es ist nur für Stift und Papier Übungen, wo ich Schleifen Invarianten finden muss. Ich denke, es braucht nur Übung. – filinep
Es ist eigentlich trivial, Schleifen Invarianten zu generieren. true ist zum Beispiel ein guter. Es erfüllt alle drei Eigenschaften, die Sie wollen:
Aber was nach dem du bist es hält Iteration
"True" ist schwach. Ich denke du meinst "du bist hinter der * stärksten * Schleifeninvariante". Ihre Antwort hat einen guten Punkt, aber ich würde sagen, normalerweise braucht man "jede induktive Invariante, die stark genug ist, um die Eigenschaft zu beweisen, die man sich vorstellt". Die stärkste Schleifeninvariante existiert möglicherweise nicht (wenn es eine Unendlichkeit von Variablen gibt, wird durch Hinzufügen von "und x '= x" für ein frisches x zu einer Invariante eine stärkere Invariante gebildet) und kann unhandlich sein. –
In Bezug auf "schwächste" haben Sie natürlich Recht. Ich habe es durcheinander gebracht! (Ich habe es als "wahr ist schwach, da es nichts bedeutet"). Antwort aktualisiert Ihr zweiter Punkt erscheint mir allerdings etwas künstlich. Willst du damit sagen, dass es nicht existiert, weil es unendlich viel Platz benötigt, um es aufzuschreiben? – aioobe
Nun, in den meisten Logiken ist eine Formel eine endliche Ansammlung von Symbolen, und ich denke, ein paar Metasätze wären nicht wahr, wenn man unendliche Assemblagen zuließ und sich sogar auf regelmäßige Assemblagen beschränkte, die endlich beschrieben werden können. Du musst also vorsichtig sein. Lassen Sie diesen Nitpick beiseite (in ACSL können Sie zum Beispiel die Invarianz von unendlichen Variablen in einer endlichen Klausel angeben), mein Punkt war, dass die stärkste Invariante viel komplexer als nötig sein kann. –
Es gibt eine Reihe von Heuristiken zum Auffinden von Schleifeninvarianten. Ein gutes Buch dazu ist "Programmierung in den 1990ern" von Ed Cohen. Es geht darum, wie man eine gute Invariante findet, indem man die Nachbedingung von Hand manipuliert. Beispiele sind: Ersetze eine Konstante durch eine Variable, stärke invariant, ...
Ich habe über das Schreiben von Schleifeninvarianten in meinem Blog geschrieben, siehe Verifying Loops Part 2. Die Invarianten, die benötigt werden, um eine Schleifenkorrektheit zu beweisen, umfassen typischerweise 2 Teile:
(2) ist einfach. Um (1) abzuleiten, beginne mit einem Prädikat, das den gewünschten Zustand nach Beendigung ausdrückt. Es besteht die Möglichkeit, dass es über eine Reihe von Daten ein "Forall" oder "Existiert" enthält. Ändern Sie nun die Grenzen von "forall" oder "exists" so, dass (a) sie von Variablen abhängen, die von der Schleife modifiziert wurden (zB Schleifenzähler), und (b) damit die Invariante trivial wahr ist, wenn die Schleife zum ersten Mal eingegeben wird (in der Regel, indem die Reichweite von "forall" oder "exists" leer gemacht wird.
Nun, da ist es. Die perfekte Antwort. +1 :) Hast du jemals gesehen, Simplify eine Verpflichtung zu lösen, dass Alt-ergo oder Z3 fehlgeschlagen?:-) – aioobe
@aioobe In diesem Artikel funktioniert Simplify gut, und in Abb.1 gibt es eine Verpflichtung mit der Eigenschaft, die Sie fragen (beide Alt-ergo und Z3 scheitern daran). Alles hängt natürlich vom Zielprogramm ab :) http://www-lipn.univ-paris13.fr/~mayero/publis/Calculemus2010.pdf –
Aha, schön :-) Erste, die ich gesehen habe :) – aioobe