Quelltext anzeigen

Du bist nicht berechtigt, die Seite zu bearbeiten. Grund:

Du kannst den Quelltext dieser Seite betrachten und kopieren:

== Aufgabe (Klausur 24.02.2010) == <<math>\phi</math>> (Vorbedingung) <syntaxhighlight lang="java"> res = 0; sp = 1; k = 0; while (k < n) { sp = sp * 7; res = res + sp; k = k + 1; } </syntaxhighlight> <<math>\psi</math>> (Nachbedingung) == Vorgehen (Zuweisungen)== Zuerst betrachten wir nur die Zuweisungen über der Schleife. Um das Vorgehen deutlich zu machen, werde ich die Reihenfolge der Zeilen vertauschen! <<math>res=0 \and sp=1 \and { \color{red}k=0~.}..</math>(folgt aus der Zuweisung der Variablen, die Klammern NICHT schließen, da möglicherweise noch Zusicherungen für die Schleife mitgeschleppt werden müssen!) <syntaxhighlight lang="java">k = 0;</syntaxhighlight> <<math>res=0 \and { \color {blue}sp=1} \and { \color{red}0=0}~...</math> <syntaxhighlight lang="java">sp = 1;</syntaxhighlight> <<math>{ \color{green}res=0} \and { \color{blue}1=1} \and 0=0~...</math> <syntaxhighlight lang="java">res=0;</syntaxhighlight> <<math>{ \color{green}0=0} \and 1=1 \and 0=0~...</math> === Noch einmal in richtiger Reihenfolge: === <<math>{ \color{green}0=0} \and 1=1 \and 0=0~...</math> <syntaxhighlight lang="java">res=0;</syntaxhighlight> <<math>{ \color{green}res=0} \and { \color{blue}1=1} \and 0=0~...</math> <syntaxhighlight lang="java">sp = 1;</syntaxhighlight> <<math>res=0 \and { \color {blue}sp=1} \and { \color{red}0=0}~...</math> <syntaxhighlight lang="java">k = 0;</syntaxhighlight> <<math>res=0 \and sp=1 \and { \color{red}k=0~.}..</math> == Vorgehen (Schleifeninvariante)== <math> \begin{array}{|c|c|c|c|} Nr & sp & res & k\\ \hline 0 & 1 & 0 & 0\\ 1 & 7 & 7 & 1\\ 2 & 49 & 56 & 2\\ 3 & 343 & 399 & 3\\ \end{array} </math>

Zurück zur Seite Hoare Kalkül(Tutorial).