Beweisbarkeit von while-Schleife vs for-Schleife

8

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.

Vincent
quelle
17
Ihr Lehrer ist entweder völlig falsch oder Sie haben falsch berichtet, was er irgendwie gesagt hat. Diese Gründe für die Bevorzugung forüber whilemacht einfach keinen Sinn. Es mag einen geben, aber das ist es nicht.
Kilian Foth
7
Ich stimme Kilian zu. Es macht keinen Sinn, dass es einen Unterschied geben sollte, ebenso for (init; test; step) { body }wie eine triviale Abneigung gegen while: {init; while (test) { step; body }}.
1
Für (;;) {cout << "sie sind wirklich nicht so verschieden" << endl;}. Der größte Unterschied besteht darin, dass Sie für Schleifen einfach eine Variable (i) im Umfang der Schleife behalten können.
Nathan Cooper
2
@ MikeNakis im Gegenteil. Ein Cargo Culter würde die Frage nicht stellen, sondern nur Mythen verewigen. Vielleicht sogar andere dafür bestrafen, dass sie sich nicht an die Regel halten.
sehe
2
@ MikeNakis Ich weiß nicht, ob wir genug Informationen haben, um die Mentailität des Lehrers zu beurteilen.
sehe

Antworten:

13

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.

babou
quelle
1
@ VincentAdvocaat Nun, die Seite ist für alle Benutzer, nicht nur das Originalposter der Frage. Deshalb habe ich es getan. Ich habe auch meine eigene Antwort für den Moderator markiert, um sie zu stoppen, wenn sie nicht korrekt ist. Eigentlich war es eine interessante Frage, und ich brauchte einige Zeit, um zu meinem Schluss zu kommen ... in der Hoffnung, dass es die richtige ist. Lassen Sie uns wissen, wenn Sie es herausfinden.
Babou
Ich habe gerade erst bemerkt, dass Sie vor einer Stunde eine Änderung vorgenommen haben, die Ihre Antwort hier angibt. Dies ist in der Tat die bestmögliche Antwort auf meine Frage, und ich danke Ihnen dafür. Was die Aufmerksamkeit des Moderators betrifft, ist es eher meine Schuld, ein Duplikat zwischen mehreren SE-Sites zu erstellen. Aus diesem Grund sehe ich keinen Grund, diese Antwort zu löschen. Wenn etwas gelöscht werden sollte, müsste es die zweite Frage sein, die ich gestellt habe. Da Ihre Antwort dort jedoch gut formuliert ist und die hier gemachte Aussage ausführlich erklärt, halte ich sie nicht für sinnvoll um einen zu entfernen. es sei denn, Sie fügen die Informationen zu dieser Frage hinzu.
Vincent
1
Ich habe keine Ahnung, seltsame Dinge passieren, immer lustig, wenn die Leute keine Gründe dafür erklären.
Vincent
3
Wieder passiert: 1 hoch + 1 runter. Was mich stört ist, dass es die Seite mehr verletzt als mich. Ich versuche vollständige Antworten zu schreiben, die Menschen helfen. Wenn es ein Fehler ist, wäre es klüger, einen Kommentar abzugeben, um mir die Möglichkeit zu geben, ihn zu korrigieren. Wenn es sich um einen anderen Grund handelt, verringert dies lediglich die Attraktivität einer Antwort, die auf Kosten der Website nützlich sein könnte. Ich frage mich, ob das Ersetzen durch die erweiterte Antwort oder das Entfernen des Haftungsausschlusses am Ende etwas damit zu tun hat. Aber der Moderator schien mit der Situation einverstanden zu sein.
Babou
1
Als Moderator mag ich Ihre Antwort und habe etwas aus dem Lesen gelernt. Es ist eine gute Antwort
maple_shaft
12

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).

Milleniumbug
quelle
Das Umschreiben einiger "for" -Schleifen als "while" -Schleifen würde das Duplizieren von Code, das Hinzufügen von Flags oder das Hinzufügen erfordern goto. Wenn man Flags hinzufügt, können alle anderen Schleifen mit einem einzigen "while (1) ..." um eine Funktion emuliert werden, die bis zu einem "return" ausgeführt wird. Wenn man "goto" hinzufügt, können alle anderen Schleifen damit emuliert werden.
Supercat
Danke, dass du meinen Standpunkt bewiesen hast. Das Kopieren und Einfügen des Codefragments A ändert nichts an meiner Fähigkeit, darüber nachzudenken.
Milleniumbug
In der Tat ändert das Kopieren / Einfügen nichts an der Fähigkeit, über Code nachzudenken, aber es ist meiner Meinung nach ein wichtiger Grund, "für" nicht als überflüssiges Sprachkonstrukt zu betrachten, da eines der Entwurfsziele einer guten Programmiersprache darin bestehen sollte, zu minimieren die Notwendigkeit zum Kopieren / Einfügen.
Supercat
7

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".

RemcoGerlich
quelle
Dies scheint meiner eigenen Einschätzung zu entsprechen, wenn auch auf einer anderen Ansicht. Die Floyd-Hoare-Logik hatte keinen Grund, die forSchleife zu betrachten , die keine feste Definition hat und komplexer ist, ohne formal notwendig zu sein.
Babou
3

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?

Jörg W Mittag
quelle
1
Eine foreinzige Sprache kann ein äquivalentes whileVerhalten erzeugen, indem die Schleifenvariable (vorausgesetzt, die Sprache erlaubt dies) während Iterationen dekrementiert wird, die nicht zu einer Beendigung führen sollen. (ZB for n in 1 to 2 { if condition then n := n-1 })
Blrfl
Es gibt viele Möglichkeiten, wie eine for-Schleife für immer zu einer Schleife gemacht werden kann, natürlich abhängig von ihrer Definition in der jeweiligen Sprache. Und eine Endlosschleife reicht für die Vollständigkeit von Turing aus.
Babou
@babou: Die häufigste Interpretation einer for-Schleife ist eine Schleife, die über einen endlichen Bereich oder eine endliche Sammlung iteriert. Natürlich kann man in vielen Sprachen eine for-Schleife hacken, um sich wie eine while-Schleife zu verhalten, aber ich denke, das hatte Jörg nicht im Sinn.
Giorgio
0

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.

Jai Thakur
quelle
-1

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?

mattnz
quelle
-10

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!

James Anderson
quelle
2
Wie können whileLoops hier besser abschneiden?
Milleniumbug
7
Oh ja? Während Sie mit whileSchleifen tatsächlich garantieren können, dass die Bedingungsvariable nicht manipuliert wurde? Tatsächlich ist das Manipulieren der Bedingungsvariablen der einzige Weg, um aus einer whileSchleife auszubrechen ! Normalerweise verzichte ich auf Abstimmungen, aber für diese Antwort mache ich eine Ausnahme.
Mike Nakis
James, könnten Sie vielleicht näher erläutern, warum dies für while-Schleifen weniger ein Problem ist? Sie könnten sich auf etwas einlassen, aber die Leute scheinen im Fall von while-Schleifen nicht einverstanden zu sein
Vincent
1
@VincentAdvocaat Ich würde sagen, dass Sie bei einer while-Schleife erwarten , dass die Bedingungsvariable auf irgendeine Weise manipuliert wird, während bei einer for-Schleife erwartet wird, dass sie nur im Schrittteil des for-Schleifenkonstrukts selbst geändert wird. Dieses Prinzip des geringsten Erstaunens ist wichtiger, als viele in der Programmierung erkennen.
Gbjbaanb
3
@gbjbaanb wahr, aber was die Frage betrifft, ist es weit entfernt vom Prinzip des geringsten Erstaunens bis zur Beweisbarkeit.
Mike Nakis