Hoare Kalkül(Tutorial)

Aus Lerngruppe Informatik
Version vom 28. Dezember 2011, 16:44 Uhr von Test (Diskussion | Beiträge)
(Unterschied) ← Nächstältere Version | Aktuelle Version (Unterschied) | Nächstjüngere Version → (Unterschied)
Wechseln zu: Navigation, Suche

Inhaltsverzeichnis

Aufgabe (Klausur 24.02.2010)

<<math>\phi</math>> (Vorbedingung)

res = 0;
sp = 1;
k = 0;
 
while (k < n) {
 sp = sp * 7;
 res = res + sp;
 k = k + 1;
}

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

k = 0;

<<math>res=0 \and { \color {blue}sp=1} \and { \color{red}0=0}~...</math>

sp = 1;

<<math>{ \color{green}res=0} \and { \color{blue}1=1} \and 0=0~...</math>

res=0;

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

res=0;

<<math>{ \color{green}res=0} \and { \color{blue}1=1} \and 0=0~...</math>

sp = 1;

<<math>res=0 \and { \color {blue}sp=1} \and { \color{red}0=0}~...</math>

k = 0;

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

Meine Werkzeuge
Namensräume
Varianten
Aktionen
Navigation
Werkzeuge