Hasso-Plattner-Institut
Prof. Dr. Tobias Friedrich
 

WHILE Semantik

Wir halten fest: Gegeben ein WHILE-Programm \(P\), bezeichnen wir mit \(\textbf{WHILE}_P^k\) die partielle Funktion \(\mathbb{N}^k \rightarrow \mathbb{N}\), welche durch \(P\) berechnet wird. Dabei legen wir fest, dass die Eingabe am Anfang der Ausführung in \(x_1, x_2, \ldots, x_k\) steht (bei \(k\) Eingaben) und dass am Ende der Ausführung die Ausgabe in \(x_0\) steht. Wir nennen die Zeichenkette \(P\) die Syntax und die Funktion \(\textbf{WHILE}_P^k\) die Semantik. Insebsondere ist \(\textbf{WHILE}_P(a_1,\ldots,a_k)\) die Ausgabe von \(P\) bei Eingaben \(a_1,\ldots,a_k \in \mathbb{N}\) (undefiniert, falls \(P\) auf \(a_1,\ldots,a_k\) nicht terminiert).


Laufzeit

Hier geht es weiter zur Laufzeit von WHILE Programmen.