<aside> ❗ La guarda del while en SmalLang no altera el estado

</aside>

Axioma 5 - Precondición más débil de un ciclo

while (B) do
	S 
endwhile;

Definición:

Definimos $H_k(Q)$ como el predicado que define el conjunto de estados a partir de los cuales la ejecución del ciclo termina en exactamente $k$ iteraciones, en un estado donde se cumple $Q$.

$$ H_0(Q) \equiv \text{def }(B) \land \lnot B \land Q $$

$$ H_{k+1}(Q) \equiv \text{def }(B) \land B \land \text{wp }\big(S, H_k(Q)\big) \quad \text{para } k\geq 0 $$

Axioma 5

$$ \text{wp } (\texttt {while...}, Q) \equiv (\exists_{i\geq 0})\big(H_i(Q)\big) $$

No podemos usar mecánicamente el Axioma 5 para demostrar la corrección de un ciclo con una cantidad no acotada a priori de iteraciones.

<aside> 💭 Recordamos: Teorema del Invariante

Si se cumple que:

1. $P_C \implies I$
2. $\{I \land B\} \space S \space \{I\}$
3. $I \land \lnot B \implies Q_C$

Entonces podemos decir que el ciclo es parcialmente correcto respecto de su especificación.

</aside>

Teorema del Invariante

Si $\text{def }(B)$ y existe un predicado $I$ tal que:

1. $P_C \implies I$
2. $\{I \land B\} \space S \space \{I\}$
3. $I \land \lnot B \implies Q_C$

y el ciclo termina, entonces la siguiente tripla de Hoare es válida

$$ \{P_C\} \space \texttt{while B do S endwhile} \space \{Q_C\} $$

Las condiciones 1, 2 y 3 garantizan la corrección parcial del ciclo, la hipótesis de terminación es necesaria para garantizar corrección.

Teorema de terminación de un ciclo

Sea $\mathbb V$ el producto cartesiano de los dominios de las variables del programa y sea $I$ un invariante del ciclo $\texttt{while B do S endwhile}$.

Si existe una función $f_V : \mathbb V \to \Z$ tal que

1. $\{I \land B \land v_0 = f_V\} \space \texttt{S} \space \{ f_V < v_0\}$
2. $I \land f_V \leq 0 \implies \lnot B$

entonces la ejecución del ciclo siempre termina.

• $f_V$ es la función variante y representa una cantidad que se va reduciendo a lo largo de las iteraciones.

Si juntamos los tres puntos del Teorema del Invariante y los dos puntos del Teorema de terminación de un ciclo tenemos el Teorema de Corrección de un Ciclo.