Siguiente: Funciones computables Un nivel arriba: Semántica de los programas-while Anterior: Semántica de los programas-while

Reglas de transformación

$$\begin{array}{lcl} P\equiv[x_i++] &\Rightarrow& \forall j: y... ...p &\mbox{\rm en otro caso. } \end{array}\right. \end{array}$$

Escribiremos

$$\begin{eqnarray*}P(\mbox{\bf x})\uparrow &\Leftrightarrow& P(\mbox{\bf x})=\perp... ...{\bf x})\downarrow &\Leftrightarrow& P(\mbox{\bf x})\not=\perp \end{eqnarray*}$$

En el primer caso, diremos que el programa P converge apara los datos $\mbox{\bf x}$. En el segundo, naturalmente, diverge.