Beweisbarkeit von while-Schleife vs for-Schleife

Ich habe diesen Lehrer, er ist ziemlich schlau (manchmal, haha), er sagte, gute Programmierer versuchen, whileLoops anstelle von forLoops zu verwenden. Der Grund, den er dafür angegeben hat, ist, dass whileSchleifen bewiesen werden können, wie in, man kann vollständig erklären, was in einer whileSchleife passiert , während man das für eine forSchleife nicht tun kann . Er sagte auch etwas über NASA-Programmierer, die nur whileSchleifen verwenden und foraus diesem Grund keine Schleifen machen dürfen .

Es fällt mir ziemlich schwer, das zu verstehen, denn für beide Schleifen kann man erklären, wie sie im Detail funktionieren, oder? für beide würden Sie immer wissen, was passieren wird?

kann mir jemand erklären, warum whileSchleifen bewiesen werden können (und deshalb könnte es forzumindest in einigen Fällen besser sein als Schleifen).

EDIT:
Vielleicht bezog er sich auf:
2: Alle Loops müssen eine feste Obergrenze haben. Es muss trivial möglich sein, dass ein Überprüfungswerkzeug statisch nachweist, dass eine voreingestellte Obergrenze für die Anzahl der Iterationen einer Schleife nicht überschritten werden kann. Wenn die Schleifenbindung nicht statisch nachgewiesen werden kann, gilt die Regel als verletzt.

Dies sagt jedoch immer noch nichts über den Unterschied zwischen while- und for-Schleifen aus.

Kurz gesagt : Was Ihr Lehrer wahrscheinlich gemeint hat, ist, dass die Semantik von whilein den meisten Sprachen ziemlich gleich ist, während sich die Semantik von forerheblich ändern kann (siehe Diskussion unten). Daher sind abstrakte sprachunabhängige Beweise mit a zuverlässiger while, aber man sollte darauf achten, dass ein Beweis mit einer Schleife in vielen Sprachen formöglicherweise nicht mit der Semantik der forSchleife übereinstimmt .

Ihre Frage ist nicht präzise genug (obwohl dies möglicherweise nicht Ihre Schuld ist).

Der Punkt ist, dass es afaik keine offizielle, ISO-unterstützte Norm oder anderweitig offiziell akzeptierte Referenzdefinition von forund whileSchleifen gibt. Die Definition hängt von der Programmiersprache ab.

Daher können Sie keine allgemeine Aussage über ihre Äquivalenz machen, bevor Sie nicht genau definiert haben, was jeder tun kann. Ich spreche das genauer an, da es eines der Hauptargumente ist, die in anderen Antworten verwendet werden (und die Diskussion wird im Folgenden nützlich sein).

Zur Intertranslatierbarkeit von forund whileSchleifen

Zusammenfassung : Dies hängt von der Programmiersprache ab, ist jedoch immer möglich, solange Sie eine Endlosschleife haben und einen Ausweg finden.

Sie können jedoch eine solche Aussage für eine bestimmte Programmiersprache treffen, und die Antwort hängt von den Merkmalen der Sprache ab.

Das bedeutet auch, dass es keinen allgemeinen Beweis gibt, sondern nur einen für jede Programmiersprache.

Eine Sache, die im Allgemeinen zutrifft, ist, dass eine whileSchleife im Allgemeinen eine forSchleife imitieren kann , da die while-Schleife die Prüfung der Ausgangsbedingungen der for-Schleife durchführen, die Initialisierung der Steuervariablen mit einer Zuweisung vor dem Eintritt in die Schleife durchführen und die Inkrementierung durchführen kann am Ende des Schleifenkörpers, so dass

for i from 1 by 2 to 10 do { xxx }

wird

i=1
while i≤11 do { xxx; i←i+2 }

Dies funktioniert mehr oder weniger für die meisten Sprachen, ist jedoch nicht so offensichtlich, wie es scheint, und es gibt möglicherweise viele "Details", über die Sie sich Sorgen machen müssen.

In vielen Sprachen forwertet die Schleife beispielsweise 3 Argumente (Anfangswert, Inkrement und Endwert) als strenge Argumente aus , die einmal vor dem Eintritt in die Schleife ausgewertet werden, während andere dann als Thunk-Argumente verwendet werden , die bei jeder Runde neu bewertet werden sollen, oder möglicherweise als faules Argument , das nur bei erstmaliger Verwendung ausgewertet wird.

Ein weiterer Punkt kann sein, dass die Inkrementvariable lokal für die forSchleife sein kann oder eine lokale Variable der Funktion sein muss, in der die Schleife erscheint.

Abhängig von solchen Problemen kann die Übersetzung von a forin a whilestark variieren, obwohl dies normalerweise möglich ist.

Gleiches gilt für die Umkehrung, bei der a whilein eine forSchleife übersetzt wird.

Das erste Problem ist, dass eine whileSchleife die Ausgangsbedingung bei jeder Runde immer neu bewertet. Einige forSchleifen sehen jedoch keine Bedingung vor, die bei jeder Runde neu bewertet wird, außer dem Vergleich der Steuervariablen mit einem festen Wert, der beim Eintritt in die Schleife berechnet wird. Dann ist die Übersetzung nur möglich, wenn es unter anderen Bedingungen ein anderes Mittel gibt, um aus der Schleife zu springen.

Dies ist mit verschiedenen Geräten möglich, wobei normalerweise mit einer bedingten Anweisung begonnen wird, die die Bedingung testet, gefolgt von einem Sprung, der, sofern verfügbar, durch eine Schleifen-Exit-Anweisung, eine return-Anweisung (nach Einkapselung der Schleife in eine Funktion) und eine goto-Anweisung implementiert wird oder eine Ausnahmeerhebung.

Mit anderen Worten, es ist wiederum sehr abhängig von Sprachen und möglicherweise von subtilen Merkmalen von Sprachen.

Wie von @milleniumbug beantwortet , ist die Intertranslation in der Sprache C einfach, da ein forLopp im Wesentlichen eine whileSchleife plus etwas Extra für eine inkrementierte Steuervariable ist .

Dies gilt jedoch nicht unbedingt für andere Sprachen und höchstwahrscheinlich nicht auf die gleiche Weise.

Abgesehen davon sollten Programmiersprachen normalerweise nur mit einer dieser Schleifen Turing-Leistung haben, da Sie dafür nur eine Endlosschleife benötigen. Solange Sie also eine Möglichkeit haben, für immer eine Schleife zu erstellen und möglicherweise zu stoppen, sind Sie sich ziemlich sicher, dass Sie jedes andere Konstrukt nachahmen können ... aber nicht unbedingt einfach.

In Bezug auf Beweise

Zusammenfassung : Es ist mir kein Grund bekannt zu behaupten, dass Beweise mit dem einen oder anderen erheblich schwieriger sein sollten (es sei denn, es handelt sich um ein seltsames Merkmal der Sprache).

Es liegt wahrscheinlich ein Missverständnis vor, oder Ihr Lehrer hatte etwas anderes im Sinn.

Die formale Semantik kann für die verschiedenen Arten von Schleifen definiert werden, die in Programmiersprachen definiert sind, und dann zum Nachweis von Eigenschaften verwendet werden.

Abhängig von der Sprache kann es in einigen Fällen komplexer sein, formale Beweise für Programme zu erstellen. Das hängt aber von der Sprache ab.

Ich kann mir keinen Grund vorstellen, warum Beweise bei einem Konstrukt wesentlich schwieriger sein sollten als bei dem anderen. Die forSchleife kann komplexer sein, da sie wie in C alles bieten kann, was mit einem whilePlus anderer Dinge gemacht wird. Aber wenn Sie es mit a machen würden while, müssten Sie die Extras in einer anderen Form hinzufügen.

Ich könnte das formale allgemeine Argument der Intertranslatierbarkeit verwenden, solange die Möglichkeit einer einzelnen Endlosschleife besteht. Ich werde dies jedoch unterlassen, da die Konstruktionen nichts sind, mit dem Sie sich in einem Beweis befassen möchten, und es wäre eindeutig eine unfaire Aussage, zumindest in der Praxis.

Nach der obigen Diskussion haben wir jedoch gesehen, dass die Schwierigkeiten für die Intertranslatierbarkeit von der großen Variabilität der forSchleife von Sprache zu Sprache herrühren. Daher die folgende Schlussfolgerung, die wahrscheinlich die richtige Antwort ist:

Eine Möglichkeit, die Aussage Ihres Lehrers zu verstehen, besteht darin, dass die Semantik der whileSchleife in allen Programmiersprachen ziemlich gleich ist, während die Syntax und Semantik der forSchleife von Sprache zu Sprache erheblich variieren kann. Daher ist es möglich, allgemeine "abstrakte" Beweise mit whileSchleifen zu erstellen, die weitgehend sprachunabhängige Semantik aufweisen, während dies für die forSchleife nicht möglich ist, deren Syntax und Semantik sich von Sprache zu Sprache zu stark ändern. Dies gilt jedoch nicht innerhalb einer bestimmten Sprache, wenn die Semantik beider genau definiert ist.

Mein bester Vorschlag ist, dass Sie Ihren Lehrer fragen, was er genau gemeint hat und ob er Ihnen ein Beispiel geben kann. Fehlphrasen oder Missverständnisse sind ein häufiges Ereignis.

In der Sprache C können Sie jede forSchleife in eine äquivalente whileSchleife umschreiben und umgekehrt.

while -> for Transformation:

Umschreiben

while(condition) { instructions; }

zu

for(; condition; ) { instructions; }

for -> while Transformation:

Dies ist etwas komplizierter, insbesondere wenn Sie eine continueAnweisung in Ihrer Schleife haben.

Umschreiben:

for(init; condition; next) { instructions; }

zu:

{
    init;
    while(condition)
    {
        instructions;
    next_label:
        next;
    }
}

aber ersetzen Sie jede continue;Aussage durch goto next_label;Aussage. Wenn conditiones sich um eine Nullanweisung handelt, ersetzen Sie sie durch true.

Wie Sie sehen können, ist in der C-Sprache keine "beweisbarer" (was auch immer das bedeutet) als die andere, denn selbst wenn eine der Schleifen vorhanden wäre, könnten Sie sie in Form einer anderen Schleife umschreiben.

Nun gibt es andere Sprachen, in denen diese while <-> forÄquivalenz nicht existiert. In Pascal können Sie beispielsweise mehr über die forSchleife annehmen . Dies bedeutet, dass Sie beim Schreiben einer forSchleife nicht jedes Konzept ausdrücken können , sondern mehr über den Codefluss beweisen können:

for i:=1 to n do
    instructions;

Hier nwird das am Anfang der Schleife gespeichert, sodass Änderungen nkeinen Einfluss auf die Anzahl der Iterationen haben und Sie iden Hauptteil der Schleife nicht ändern können . Dies bedeutet, dass Sie trivial beweisen können, dass diese Schleife irgendwann endet (wie nes endlich ist und Sie nicht ändern können i).

In der Floyd-Hoare-Logik , dem gebräuchlichsten formalen System zur Begründung der Richtigkeit von Computerprogrammen, gibt es die while-Regel .

Mit anderen Worten, wenn Sie eine Schutzklausel (den Ausdruck in Klammern in while()) haben, eine Variantenfunktion (ein Ausdruck mit diskreten Werten, von denen gezeigt werden kann, dass er bei jeder Ausführung der Schleife monoton abnimmt und immer positiv ist) und eine Schleifeninvariante (Eine logische Anweisung, die vor und nach jedem Ausführen der Schleife immer wahr ist), können Sie beweisen, dass die while-Schleife beendet wird (da die Variantenfunktion nicht weiter abnehmen kann) und dass die Schutzklausel schließlich falsch ist und die Schleife unveränderlich wahr sein.

Die Floyd-Hoare-Logik hat keine Regeln für forSchleifen oder was auch immer Konstrukte der tatsächlichen Sprachen haben mögen.

Wie andere Antworten erklären, können for-Schleifen immer als while-Schleifen geschrieben werden. Das bedeutet, dass sie begründet werden können, es erfordert nur ein wenig mehr Arbeit.

Wenn Ihr Lehrer Kurse an der Universität hatte, in denen er Korrektheitsnachweise für seine Programme vorlegen musste, schrieb er wahrscheinlich Programme nur mit while-Schleifen. Ich weiß, dass ich es getan habe. Und wenn Sie es gewohnt sind, in Wachen, Variantenfunktionen und Schleifeninvarianten zu denken, scheinen sie sehr natürlich zu sein. Übermäßiges Verwenden von Loops ist eine Gewohnheit, die Sie bei CS-Absolventen sehen. Ich musste lernen, dies in meinen ersten Monaten als professioneller Entwickler zu beenden.

Irgendwann auf der ganzen Linie hat Ihr Lehrer all dies falsch in Erinnerung gerufen, da "gute Programmierer while-Schleifen verwenden", während das, was wirklich passiert, eher so aussieht wie "einige CS-Absolventen verwandeln ihre Korrektheitsbeweis-Gewohnheiten in praktische Programmiergewohnheiten".

In gewissem Sinne ist das genaue Gegenteil der Fall.

Eine Sprache mit nur for-loops ist nicht Turing-vollständig, sie kann nur die primitiv-rekursiven Funktionen berechnen, nicht alle Turing-berechenbaren Funktionen. Da alle Berechnungen in einer Sprache mit nur for-loops immer beendet werden, treten das Halteproblem und alle anderen darauf basierenden Entscheidbarkeitsprobleme einfach nicht auf, sodass es möglich ist, mechanisch viel mehr statische Eigenschaften von Programmen als in einer Sprache mit zu bestimmen while-schleifen.

OTOH, eine Sprache mit nur natürlichen Zahlen, einer einzelnen Variablen und while-loops, ist Turing-vollständig. Daher ist es nicht möglich, selbst die einfachsten Eigenschaften zu bestimmen: Gibt dieses Programm ein Ergebnis zurück?

Ich möchte sagen, dass es in Wirklichkeit keinen Unterschied gibt. Ihre Frage ist irrelevant. Möglicherweise hat Ihr Lehrer beabsichtigt, while-Schleife zu verwenden, wenn nein. Die Anzahl der Iterationen ist vorher nicht bekannt. In vielen Fällen müssen wir eine while-Schleife verwenden, um Ziffern einer Nr. zu extrahieren. wenn der Benutzer die Nr. eingibt. die von beliebiger Länge sein kann. Technisch gesehen besteht die Ähnlichkeit zwischen der for & while-Schleife darin, dass beide eingangsgesteuerte Schleifen sind, bei denen der (Testausdruck / -bedingung) vor dem Eintritt in den Schleifenkörper bewertet wird. Dies ist die Unterscheidung zwischen while- und do-while-Schleifen.

Es stammt wahrscheinlich aus der frühen C-Programmierung, bei der Schleifen nach heutigen Normen häufig missbraucht und missbraucht wurden, insbesondere wenn die Bedingung geändert wurde. Als Programmierer begannen, die Auswirkungen bestimmter Programmierstile zu verstehen, gerieten der Missbrauch und der Missbrauch von Schleifenbedingungen in Ungnade, und die Aussage, die (wohl) einmal gültig war, enthält keine Wahrheit mehr.

Die Aussage ist absolut nicht wahr, wenn Sie sich nur die Sprachdefinition und -syntax ansehen und ignorieren, wie sie verwendet wurde.

Die Aussage selbst bietet jedoch eine wertvolle Lektion für jeden, der sie verstehen will, ihre Geschichte und warum sie nicht mehr als wahr angesehen wird. - Was ist der Ausdruck über Lernen, Fehler und deren Wiederholung?

Dein Lehrer ist richtig!

Der Grund ist der folgende ist gültig C.

for (int x = 1 ; x < 20 ; x++ ) {
   x = x + 9;
}

Sie können nicht garantieren, dass die Bedingungsvariablen nicht manipuliert wurden!