Hoare Logikschleife Invariant

Wenn wir von Hoares Logik sprechen, um die (teilweise) Korrektheit von Programmen zu beweisen, dann benutzen Sie die Vor- und Nachbedingung, zerlegen das Programm und benutzen die Regeln von Hoares Logik-Inferenzsystem, um eine induktive Formel zu erstellen und zu beweisen >

In Ihrem Beispiel möchten Sie das Programm mit der Regel

In Ihrem Fall

• p: i ≥ 0
• b: i & gt; 0
• S: i: = i-1.

Also im nächsten Schritt schließen wir {i ≥ 0 ^ i > 0} i := i−1 {i ≥ 0} ab. Dies kann weiter leicht abgeleitet und bewiesen werden. Ich hoffe, das hilft.

Um nützlich zu sein (für Ihre Argumentation) ist der Hauptpunkt der Invariante. Sehen Sie sich also die Nachbedingung an, die Sie beweisen möchten, und versuchen Sie, eine Invariante zu erstellen, die Ihnen hilft, Schritt für Schritt zur Nachbedingung zu gelangen, die aus dem Code der Schleife abgeleitet werden kann.

Ich bin mir nicht sicher, ob das deine Frage beantworten wird, aber nur für den Fall, dass es das tut:

• Eine "loop-invariant" informell ist eine Tatsache, die vor und nach einer Iteration einer Schleife wahr bleibt. Es definiert im Wesentlichen die Konsistenzbeschränkung des Programms in Bezug auf diese Schleife.
• Ich weiß nicht genug über Hoare Logic, um Ihnen genau zu sagen, wie eine Schleifeninvariante "berechnet" werden würde, aber ich vermute, dass so etwas von der Sprache des zu analysierenden Codes mehr abhängt als von der formalen Beweissprache selbst . Haben Sie eine formale algorithmische Beschreibung, mit der Sie arbeiten? Ich könnte vielleicht mit etwas mehr Hintergrund weitermachen.
• Eine nützliche Schleifeninvariante würde etwas Spezifisches über den Zustand einer Anwendung beschreiben. Wenn Sie zum Beispiel Insertion Sort schreiben, würde eine nützliche Schleifeninvariante für die Bewegungsschleife des Hauptelements im Wesentlichen angeben, dass die (Unter) -Liste die gleiche Sammlung von Objekten vor und nach der Ausführung der Schleife enthält, und vielleicht die Elemente, die vorher waren in sortierter Reihenfolge in sortierter Reihenfolge.