Betrachten sie das folgende Programm. Es verarbeitet als Eingabe \(n\) und speichert die Ausgabe in \(p\). Was berechnet das Programm vermutlich? Tragen Sie ihre Vermutung in der untersten Zeile als Nachbedingung ein und beweisen sie die Korrektheit mit dem Floyd-Hoare-Kalkül.
Die Eintragungen erfolgen in LaTeX-Math Notation. Beachten Sie, dass jede Zeile im Editor eine Umformung ist. Weitere Umformungen können Sie durch hinzufügen weiterer Zeilen ober- oder unterhalb einfügen. Die geschweiften Klammern und Zeilenumbrüche brauchen Sie nicht einzugeben.
x := 0;
p := 0;
while (x < n) {
p := p + 2 ∗ x + 1;
x := x + 1
}
Es werden keine Daten übertragen. Per Klick auf "Ergebnis speichern" kann eine Datei gespeichert werden, welche die eingegebenen Ergebnisse enthält. Diese Datei sendet ihr bitte rechtzeitig bis Dienstag 23:59:59 an martin (punkt) ring (klammeraffe) dfki (punkt) de. Ihr könnt eure Abgabe später auch wieder laden und ansehen indem ihr auf "Ergebnis laden" klickt.
