Programas Imperativos

Especificaciones (PI)

Terna de Hoare

Si tenemos dos predicados $P$ y $Q$ , y tenemos una sentencia $S$ , podemos preguntarnos si vale o no lo siguiente:
“Para todo estado inicial que cumple $P$ , la ejecución de $S$ termina en un estado final que satisface $Q$ ”, o también, $\; \{ P \} \; S \; \{ Q \}$

Este predicado puede ser True o False, y se denomina Terna de Hoare.

Por ejemplo:

\begin{aligned} &\{ \; P: \; x > 0 \; \} \\ &x := x + 1 \\ &\{ \; Q: \; x > 1 \; \} \end{aligned}

En este caso, $\; \{ P \} \; S \; \{ Q \} \equiv True$ , ya que si $x > 0$ , entonces $x + 1 > 1$ .

El predicado $P$ puede ser válido para cualquier estado, o puede ser válido para un conjunto de estados.

El predicado $\{ \; True \; \}$ es válido para cualquier estado, al igual que $\{ \; x > 0 \implies x \geq 0 \; \}$ .

$P_0$ es más fuerte que $P \iff (P_0 \implies P)$ .
$P_0$ es más débil que $P \iff (P \implies P_0)$ .

Podemos pensar en un estado débil si exige menos condiciones para cumplirse, y en un estado fuerte si exige más condiciones.
Por ejemplo, si $P_0 \equiv \{ \; x > 0 \; \}$ y $P \equiv \{ \; x \geq 0 \; \}$ , entonces $P_0$ es más fuerte que $P$ .

Weakest Precondition

Dada la sentencia $S$ y el predicado $Q$ , podemos preguntarnos cuál es el predicado más débil que garantiza que $Q$ se cumpla después de ejecutar $S$ . Este predicado se llama Weakest Precondition y se denota $wp.S.Q$ .

La relación entre la Terna de Hoare y la Weakest Precondition es la siguiente:

\{ P \} \; S \; \{ Q \} \equiv P \implies wp.S.Q

Derivaciones (PI)

A través de una especificación dada como una terna:

\begin{array}{c} \{\; P \; \} \\ S \\ \{\; Q \; \} \end{array}

Podemos derivar el programa incógnita $S$ con la precondición $P$ y la postcondición $Q$ dadas.
Para ello recurrimos a los predicados asociados a la Terna o a la definición de Weakest Precondition. De manera tal que se cumpla que $P \implies Q$ .

Skip

Si tenemos una especificación de la forma:

\begin{aligned} &\textnormal{Const} \; N : Int, \; A : array[p, N)ofInt; \\ &\textnormal{Var} \; pos, \; i : Int; \\ &\{ \; P: res=0 \land pos = 0 \; \} \\ &S \\ &\{ \; res = \bigl \langle \sum i : 0 \leq i < pos : A.i \; \bigr \rangle \; \} \end{aligned}

Podemos determinar si $S$ es un $\mathbf{skip}$ suponiendo $P$ y partiendo de la postcondición $Q$ :

\begin{array}{ll} \underline{Q} \\ \\ \equiv \{ \textnormal{ Definición de } Q \; \} \\ \\ \underline{res} = \bigl \langle \sum i : 0 \leq i < \underline{pos} : A.i \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Hipótesis de } P \; \} \\ \\ 0 = \bigl \langle \sum i : \underline{0 \leq i < 0} : A.i \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Aritmética } \} \\ \\ 0 = \bigl \langle \sum i : \underline{False} : A.i \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Rango vacío } \} \\ \\ \underline{0 = 0} \\ \\ \equiv \{ \textnormal{ Lógica } \} \\ \\ True \end{array}

En este caso sencillo, podemos determinar que $S$ es un $\mathbf{skip}$ , ya que $P \implies Q$ sin necesidad de ejecutar ninguna sentencia:

\begin{aligned} &\textnormal{Const} \; A : array[p, q)ofInt; \\ &\textnormal{Var} \; res, \; pos : Int; \\ &\{ \; P: res=0 \land pos = 0 \; \} \\ &\mathbf{skip}; \\ &\{ \; res = \bigl \langle \sum i : 0 \leq i < pos : A.i \; \bigr \rangle \; \} \end{aligned}

Asignación

Supongamos que $S$ no es un skip ( $P$ no implica $Q$ ) podemos probar tomando las variables del programa y asignarlas a incógnitas.

Tomemos el siguiente ejemplo:

\begin{aligned} &\textnormal{Const} \; A : array[p, q)ofInt; \\ &\textnormal{Var} \; res, \; pos : Int; \\ &\{ \; P: \bigl \langle \sum i : 0 \leq i < pos : A.i \; \bigr \rangle \land 0 \leq pos < N \; \} \\ &S \\ &\{ \; res = \bigl \langle \sum i : 0 \leq i < pos : A.i \; \bigr \rangle \; \} \end{aligned}

Por intuición sabemos que $pos$ puede ser $pos + 1$ . Sin embargo, debemos determinar el valor de $res$ . Podemos probar asignar $res$ a una incógnita $E$ y usar la definición de Weakest Precondition:

\begin{array}{ll} P \implies wp.(res, \; pos := E, \; pos + 1).(res = \bigl \langle \; \sum i : 0 \leq i < pos : A.i \; \bigr \rangle) \\ \; \\ \underline{wp.(res, \; pos := E, \; pos + 1).(res = \bigl \langle \; \sum i : 0 \leq i < pos : A.i \; \bigr \rangle)} \\ \\ \equiv \{ \textnormal{ Definición de wp para } := \; \} \\ \\ E = \bigl \langle \; \sum i : \underline{0 \leq i < pos + 1} : A.i \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Lógica } \; \} \\ \\ E = \bigl \langle \; \sum i : \underline{0 \leq i < pos \lor i = pos } : A.i \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Partición de Rango } \} \\ \\ E = \underline{\bigl \langle \; \sum i : 0 \leq i < pos : A.i \; \bigr \rangle} + \bigl \langle \; \sum i : i = pos : A.i \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Hipótesis de } res \; \} \\ \\ E = res + \underline{\bigl \langle \; \sum i : i = pos : A.i \; \bigr \rangle} \\ \\ \equiv \{ \textnormal{ Rango unitario } \} \\ \\ \underline{E = res + A.pos} \\ \\ \equiv \{ \textnormal{ Elijo } E = res + A.pos \; \} \\ \\ True \end{array}

Entonces nuestro programa queda:

\begin{aligned} &\textnormal{Const} \; A : array[p, q)ofInt; \\ &\textnormal{Var} \; res, \; pos : Int; \\ &\{ \; P: \bigl \langle \; \sum i : 0 \leq i < pos : A.i \; \bigr \rangle \land 0 \leq pos < N \; \} \\ &res, \; pos := res + A.pos, \; pos + 1; \\ &\{ \; res = \bigl \langle \; \sum i : 0 \leq i < pos : A.i \; \bigr \rangle \; \} \end{aligned}

Condicional

Si por ejemplo quisieramos saber el máximo entre dos números sin usar el operador $\textnormal{max}$ , debemos descubrir la sentencia $S$ de:

\begin{aligned} &\textnormal{Var} \; x, \; y, \; res : Int; \\ &\{ \; P: x = X \land y = Y \} \\ &S \\ &\{ \; res = X \; \textnormal{max} \; Y \; \} \end{aligned}

(Tanto $X$ como $Y$ son variables de especificación)

No debemos usar $\mathbf{skip}$ , pero podemos probar asignando $res$ a una variable incógnita $E$ y aplicar la definición de Weakest Precondition:

\begin{array}{ll} P \implies wp.(res := E).(res = X \; \textnormal{max} \; Y) \\ \; \\ \underline{wp.(res := E).(res = X \; \textnormal{max} \; Y)} \\ \\ \equiv \{ \textnormal{ Definición de wp para } := \; \} \\ \\ E = X \; \textnormal{max} \; Y \end{array}

Siguiendo el enunciado no podemos usar el operador $\textnormal{max}$ , podemos resolver esto mediante un análisis por casos:

Caso 1: $x \geq y$

\begin{aligned} &E = \underline{X \; \textnormal{max} \; Y} \\ \\ &\equiv \{ \textnormal{ Hipótesis de } P \; \} \\ \\ &E = \underline{x \; \textnormal{max} \; y} \\ \\ &\equiv \{ \textnormal{ Caso 1: } x \geq y \; \} \\ \\ &\underline{E = x} \\ \\ &\equiv \{ \textnormal{ Elijo } E = x \; \} \\ \\ &True \end{aligned}

Caso 2: $x \leq y$

\begin{aligned} &E = \underline{X \; \textnormal{max} \; Y} \\ \\ &\equiv \{ \textnormal{ Hipótesis de } P \; \} \\ \\ &E = \underline{x \; \textnormal{max} \; y} \\ \\ &\equiv \{ \textnormal{ Caso 2: } x \leq y \; \} \\ \\ &\underline{E = y} \\ \\ &\equiv \{ \textnormal{ Elijo } E = y \; \} \\ \\ &True \end{aligned}

Derivando la asignación, llegamos a un análisis por casos, por lo que podemos usar $\mathbf{if}$ , donde cada caso es una guarda para determinar el programa final:

\begin{aligned} &\textnormal{Var} \; x, \; y, \; res : Int; \\ &\{ \; P: x = X \land y = Y \} \\ &\mathbf{if} \; x \geq y \rightarrow \\ &\quad res := x; \\ &\Box \; x \leq y \rightarrow \\ &\quad res := y; \\ &\mathbf{fi}; \\ &\{ \; res = X \; \textnormal{max} \; Y \; \} \end{aligned}

Cuando se utiliza el cuantificador de conteo $\textnormal{N}$ en una especificación, se puede terminar en un análisis por casos si se utiliza el rango unitario:

Por ejemplo:

\begin{aligned} &... \\ &E = res + \bigl \langle \; \textnormal{N} i : \underline{i = numero\_actual} : i \; \textnormal{mod} \; 6 = 0 \; \bigr \rangle \\ &\\ &\equiv \{ \textnormal{ Rango unitario } \} \\ &\\ &E = res + ( \\ &numero\_actual \; \textnormal{mod} \; 6 = 0 \rightarrow 1 \\ &\Box \; numero\_actual \; \textnormal{mod} \; 6 \not= 0 \rightarrow 0 \\ &) \end{aligned}

Tendríamos las dos posibilidades de que la variable $numero\_actual$ sea múltiplo de 6 o no.

Secuenciación

Muchas veces tenemos un problema principal y otro problema accesorio que resolver.
Por ejemplo, la siguiente especificación:

\begin{aligned} &\textnormal{Const} \; N : Int, \; A : array[0,N) of Int; \\ &\textnormal{Var} \; promedio : Float; \\ &\{ \; P: \; N \geq 0 \; \} \\ &S \\ &\{ \; Q: \; promedio = \bigl \langle \; \sum i : 0 \leq i < N : A.i \; \bigr \rangle \; / \; N \; \} \end{aligned}

Primero podemos resolver el problema principal (sumar todos los elementos), y dividirlos por $N$ (problema accesorio).
Cambiando un poco la estructura y agregando una variable $suma$ sería:

\begin{aligned} &\textnormal{Const} \; N : Int, \; A : array[0,N) of Int; \\ &\textnormal{Var} \; promedio : Float, \; suma : Int; \\ &\{ \; P: \; N \geq 0 \; \} \\ &S_1; \\ &\{ \; Q: \; suma = \bigl \langle \; \sum i : 0 \leq i < N : A.i \; \bigr \rangle \; \} \\ &S_2; \\ &\{ \; R: \; promedio = \bigl \langle \; \sum i : 0 \leq i < N : A.i \; \bigr \rangle \; / \; N \; \} \end{aligned}

Una vez realizado el trabajo de derivación en $S_1$ y $S_2$ , daremos con el programa final.

Repetición

Las repeticiones serán necesarias cuando necesitemos ejecutar una misma acción varias veces.
Por ejemplo, si queremos sumar los elementos de un arreglo, necesitaremos recorrerlo.

\begin{aligned} &\textnormal{Const} \; N : Int, \; A : array[0,N) of Int; \\ &\textnormal{Var} \; res, \; i : Int; \\ &\{ \; P: \; N \geq 0 \; \} \\ &S \\ &\{ \; Q: \; res = \bigl \langle \; \sum i : 0 \leq i < N : A.i \; \bigr \rangle \; \} \end{aligned}

Para poder determinar la inicialización y el cuerpo de ciclo, necesitamos primero proponer una invariante y la guarda.

El invariante debe cumplir las siguientes condiciones:

1) $P \implies I \;$ (El invariante debe ser verdadero al inicio)
2) $\{I \land B\} \; S \; \{I\} \;$ (El cuerpo de ciclo mantiene el invariante)
3) $I \land \neg B \implies Q \;$ (El invariante implica la postcondición al terminar el ciclo)
4) El ciclo debe terminar

El problema surge en como determinar el invariante. Para ello podemos hacer un reemplazo de constante por variable

Podemos reemplazar la constante $N$ por una variable $pos$ , y proponer un invariante $I$ :

I \equiv res = \bigl \langle \; \sum i : 0 \leq i < pos : A.i \; \bigr \rangle \; \land \; 0 \leq pos \leq N

Determinamos que $pos$ debe ser menor o igual a $N$ para no exceder el rango del arreglo.

Una guarda $B$ puede ser $pos < N$ , ya que queremos recorrer todos los elementos del arreglo.

En base a las condiciones anteriores de invariante y guarda, podemos proponer un ciclo:

\begin{aligned} &\textnormal{Const} \; N : Int, \; A : array[0,N) of Int; \\ &\textnormal{Var} \; res, \; pos : Int; \\ &\{ \; P: \; N \geq 0 \; \} \\ &S_1; \\ &\{ \; I \; \} \\ &\mathbf{do} \; pos < N \rightarrow \\ &\quad \{ \; I \land B \; \} \\ &\quad S_2; \\ &\quad \{ \; I \; \} \\ &\mathbf{do}; \\ &\{ \; Q: \; res = \bigl \langle \; \sum i : 0 \leq i < N : A.i \; \bigr \rangle \; \} \end{aligned}

Donde $S_1$ es la inicialización y $S_2$ es el cuerpo del ciclo. Ahora podemos derivar ambos para llegar al programa final.

Para $S_1$ , podemos probar con $pos, \; res := 0, \; E$ , la posición a indexar será por defecto $0$ :

\begin{array}{ll} P \implies wp.(pos, \; res := 0, \; E).I \\ \; \\ \underline{wp.(pos, \; res := 0, \; E).(res = \bigl \langle \; \sum i : 0 \leq i < pos : A.i \; \bigr \rangle \land 0 \leq pos \leq N)} \\ \\ \equiv \{ \textnormal{ Definición de wp para } := \; \} \\ \\ E = \bigl \langle \; \sum i : 0 \leq i < 0 : A.i \; \bigr \rangle \; \underline{\land \; 0 \leq 0 \leq N} \\ \\ \equiv \{ \textnormal{ Hipótesis de } P, \textnormal{ elemento neutro de} \; \land \; \} \\ \\ E = \bigl \langle \; \sum i : \underline{0 \leq i < 0} : A.i \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Aritmética, rango vacío } \} \\ \\ \underline{E = 0} \\ \\ \equiv \{ \textnormal{ Elijo } E = 0 \; \} \\ \\ True \end{array}

Tenemos que $S_1: pos, \; res := 0, \; 0$ . Ahora podemos derivar $S_2$ probando con $pos, \; res := pos + 1, \; E$ , queremos aumentar la posición a indexar:

\begin{array}{ll} P \implies wp.(pos, \; res := pos + 1, \; E).I \\ \; \\ \underline{wp.(pos, \; res := pos + 1, \; E).(res = \bigl \langle \; \sum i : 0 \leq i < pos : A.i \; \bigr \rangle \land 0 \leq pos \leq N)} \\ \\ \equiv \{ \textnormal{ Definición de wp para } := \; \} \\ \\ E = \bigl \langle \; \sum i : 0 \leq i < pos + 1 : A.i \; \bigr \rangle \; \underline{\land \; 0 \leq pos + 1 \leq N} \\ \\ \equiv \{ \textnormal{ Validez por hipótesis } 0 \leq pos \land pos < N, \textnormal{ elemento neutro de } \; \land \; \} \\ \\ E = \bigl \langle \; \sum i : \underline{0 \leq i < pos + 1} : A.i \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Lógica } \} \\ \\ E = \bigl \langle \; \sum i : \underline{0 \leq i < pos \lor i = pos} : A.i \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Partición de Rango } \} \\ \\ E = \underline{\bigl \langle \; \sum i : 0 \leq i < pos : A.i \; \bigr \rangle} + \bigl \langle \; \sum i : i = pos : A.i \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Hipótesis de } res \; \} \\ \\ E = res + \underline{\bigl \langle \; \sum i : i = pos : A.i \; \bigr \rangle} \\ \\ \equiv \{ \textnormal{ Rango unitario } \} \\ \\ \underline{E = res + A.pos} \\ \\ \equiv \{ \textnormal{ Elijo } E = res + A.pos \; \} \\ \\ True \end{array}

Por lo tanto, $S_2: pos, \; res := pos + 1, \; res + A.pos$ . Ahora podemos dar con el programa final:

\begin{aligned} &\textnormal{Const} \; N : Int, \; A : array[0,N) of Int; \\ &\textnormal{Var} \; res, \; pos : Int; \\ &\{ \; P: \; N \geq 0 \; \} \\ &pos, \; res := 0, \; 0; \\ &\mathbf{do} \; pos < N \rightarrow \\ &\quad pos, \; res := pos + 1, \; res + A.pos; \\ &\mathbf{do}; \\ &\{ \; Q: \; res = \bigl \langle \; \sum i : 0 \leq i < N : A.i \; \bigr \rangle \; \} \end{aligned}

Ejercicios resueltos - Derivaciones y evaluaciones (PI)

Ejecutar el programa para el arreglo $[1, 2, 3, 4]$ y mostrar los cambios de estado:

\begin{aligned} &\textnormal{Const} \; N : Int, \; A : array[0,N) of Int; \\ &\textnormal{Var} \; pos : Int; \\ &pos := 0; \\ &\mathbf{do} \; pos < N \rightarrow \\ &\quad A.pos := A.pos + 1; \\ &\quad pos := pos + 1; \\ &\mathbf{do}; \\ \end{aligned}

Debemos considerar el estado al inicio del programa, en los distintos pasos del ciclo y al finalizar el programa:

\begin{aligned} &\textnormal{Const} \; N : Int, \; A : array[0,N) of Int; \\ &\textnormal{Var} \; pos : Int; \\ &[\![ \sigma_0 : (A \mapsto [1, 2, 3, 4], \; N \mapsto 4, \; pos \mapsto 0) ]\!] \\ &pos := 0; \\ &\mathbf{do} \; pos < N \rightarrow \\ &[\![ \sigma_1^1 : (A \mapsto [1, 2, 3, 4], \; N \mapsto 4, \; pos \mapsto 0), \\ &\sigma_1^2 : (A \mapsto [2, 2, 3, 4], \; N \mapsto 4, \; pos \mapsto 1), \\ &\sigma_1^3 : (A \mapsto [2, 3, 3, 4], \; N \mapsto 4, \; pos \mapsto 2), \\ &\sigma_1^4 : (A \mapsto [2, 3, 4, 4], \; N \mapsto 4, \; pos \mapsto 3) ]\!] \\ &\quad A.pos := A.pos + 1; \\ &\quad pos := pos + 1; \\ &[\![ \sigma_2^1 : (A \mapsto [2, 3, 4, 4], \; N \mapsto 4, \; pos \mapsto 1), \\ &\sigma_2^2 : (A \mapsto [2, 3, 3, 4], \; N \mapsto 4, \; pos \mapsto 2), \\ &\sigma_2^3 : (A \mapsto [2, 3, 4, 4], \; N \mapsto 4, \; pos \mapsto 3), \\ &\sigma_2^4 : (A \mapsto [2, 3, 4, 5], \; N \mapsto 4, \; pos \mapsto 4) ]\!] \\ &\mathbf{do}; \\ &[\![ \sigma_3 : (A \mapsto [2, 3, 4, 5], \; N \mapsto 4, \; pos \mapsto 4) ]\!] \\ \end{aligned}

Dado un arreglo $A$ , derivar un programa que resuelva el problema:

\begin{aligned} &\textnormal{Const} \; N : Int, \; A : array[0,N) of Int; \\ &\textnormal{Var} \; res : Bool; \\ &\{ \; P: \; N \geq 0 \; \} \\ &S \\ &\{ \; Q: \; res = \langle \; \forall i : 0 \leq i \leq N : \bigl \langle \; \sum j : 0 \leq j < i : A.j \; \bigr \rangle \geq 0 \; \bigr \rangle \; \} \end{aligned}

Este problema involucra el uso de un ciclo. Para resolverlo podemos aplicar la técnica de reemplazo de constante por variable. Definimos una variable $pos$ que recorrerá el arreglo $A$ y definimos una invariante $I$ :

I \equiv res = \langle \; \forall i : 0 \leq i \leq pos : \; \bigl \langle \; \sum j : 0 \leq j < i : A.j \; \bigr \rangle \geq 0 \; \bigr \rangle \; \land \; 0 \leq pos \leq N

Nos interesa que $pos$ sea menor que $N$ para no exceeder el rango del arreglo.
Esa será nuestra guarda: $B \equiv pos < N$ .

Con esto podemos seguir la siguiente estructura:

\begin{aligned} &\textnormal{Const} \; N : Int, \; A : array[0,N) of Int; \\ &\textnormal{Var} \; res: Bool, \; pos : Int; \\ &\{ \; P: \; N \geq 0 \; \} \\ &S_1; \\ &\{ \; I \; \} \\ &\mathbf{do} \; pos < N \rightarrow \\ &\quad \{ \; I \land B \; \} \\ &\quad S_2; \\ &\quad \{ \; I \; \} \\ &\mathbf{do}; \\ &\{ \; Q: \; res = \langle \; \forall i : 0 \leq i \leq N : \; \bigl \langle \; \sum j : 0 \leq j < i : A.j \; \bigr \rangle \geq 0 \; \bigr \rangle \; \} \end{aligned}

Si queremos recorrer el arreglo, debemos partir de la posición $0$ . La inicialización $S_1$ sería: $pos, \; res := 0, \; E$

\begin{array}{ll} P \implies wp.(pos, \; res := 0, \; E).I \\ \; \\ \underline{wp.(pos, \; res := 0, \; E).(res = \langle \; \forall i : 0 \leq i \leq pos : \; \bigl \langle \; \sum j : 0 \leq j < i : A.j \; \bigr \rangle \geq 0 \; \bigr \rangle \land 0 \leq pos \leq N)} \\ \\ \equiv \{ \textnormal{ Definición de wp para } := \; \} \\ \\ E = \langle \; \forall i : 0 \leq i \leq 0 : \; \bigl \langle \; \sum j : 0 \leq j \leq 0 : A.j \; \bigr \rangle \geq 0 \; \bigr \rangle \; \underline{\land \; 0 \leq 0 \leq N} \\ \\ \equiv \{ \textnormal{ Hipótesis de } P, \textnormal{ elemento neutro de } \land \} \\ \\ E = \langle \; \forall i : \underline{0 \leq i \leq 0} : \; \bigl \langle \; \sum j : 0 \leq j \leq 0 : A.j \; \bigr \rangle \geq 0 \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Lógica } \} \\ \\ E = \langle \; \forall i : \underline{i = 0} : \; \bigl \langle \; \sum j : 0 \leq j \leq 0 : A.j \; \bigr \rangle \geq 0 \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Rango unitario } \} \\ \\ E = \langle \; \sum j : \underline{0 \leq j \leq 0} : A.j \; \bigr \rangle \geq 0 \\ \\ \equiv \{ \textnormal{ Aritmética } \} \\ \\ E = \langle \; \sum j : \underline{False} : A.j \; \bigr \rangle \geq 0 \\ \\ \equiv \{ \textnormal{ Rango vacío } \} \\ \\ E = \underline{0 \geq 0} \\ \\ \equiv \{ \textnormal{ Lógica } \} \\ \\ \underline{E = True} \\ \\ \equiv \{ \textnormal{ Elijo } E = True \; \} \\ \\ True \end{array}

Por lo tanto, $S_1: pos, \; res := 0, \; True$ . Ahora podemos derivar $S_2$ probando con $pos, \; res := pos + 1, \; E$ , queremos aumentar la posición a indexar:

\begin{array}{ll} P \implies wp.(pos, \; res := pos + 1, \; E).I \\ \; \\ \underline{wp.(pos, \; res := pos + 1, \; E).(res = \langle \; \forall i : 0 \leq i \leq pos : \; \bigl \langle \; \sum j : 0 \leq j < i : A.j \; \bigr \rangle \geq 0 \; \bigr \rangle \land 0 \leq pos \leq N)} \\ \\ \equiv \{ \textnormal{ Definición de wp para } := \; \} \\ \\ E = \langle \; \forall i : 0 \leq i \leq pos + 1 : \; \bigl \langle \; \sum j : 0 \leq j < i : A.j \; \bigr \rangle \geq 0 \; \bigr \rangle \; \underline{\land \; 0 \leq pos + 1 \leq N} \\ \\ \equiv \{ \textnormal{ Validez por hipótesis } 0 \leq pos \land pos < N, \textnormal{ elemento neutro de } \land \; \} \\ \\ E = \langle \; \forall i : \underline{0 \leq i \leq pos + 1} : \; \bigl \langle \; \sum j : 0 \leq j < i : A.j \; \bigr \rangle \geq 0 \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Lógica } \} \\ \\ E = \langle \; \forall i : \underline{0 \leq i \leq pos \lor i = pos} : \; \bigl \langle \; \sum j : 0 \leq j < i : A.j \; \bigr \rangle \geq 0 \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Partición de Rango } \} \\ \\ E = \underline{\langle \; \forall i : 0 \leq i \leq pos : \; \bigl \langle \; \sum j : 0 \leq j < i : A.j \; \bigr \rangle \geq 0 \; \bigr \rangle} \land \langle \; \forall i : i = pos : \; \bigl \langle \; \sum j : 0 \leq j < i : A.j \; \bigr \rangle \geq 0 \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Hipótesis de } res \; \} \\ \\ E = res \land \underline{\langle \; \forall i : i = pos : \; \bigl \langle \; \sum j : 0 \leq j < i : A.j \; \bigr \rangle \geq 0 \; \bigr \rangle} \\ \\ \equiv \{ \textnormal{ Rango unitario } \} \\ \\ E = res \land \langle \; \sum j : 0 \leq j < pos : A.j \; \bigr \rangle \geq 0 \\ \end{array}

La expresión no es programable. Pero podríamos definir una nueva variable $suma$ tal que:

suma = \langle \; \sum j : 0 \leq j < pos : A.j \; \bigr \rangle

Para hacer su uso debemos declarar esta nueva variable y fortalecer la invariante:

I' \equiv res = I \land suma = \langle \; \sum j : 0 \leq j < pos : A.j \; \bigr \rangle

Debemos volver a calcular la inicialización $S_1$ , partiendo de $pos, \; res, \; s := 0, \; E, \; F$ :

\begin{array}{ll} P \implies wp.(pos, \; res, \; suma := 0, \; E, \; F).I' \\ \; \\ \underline{wp.(pos, \; res, \; suma := 0, \; E, \; F).I'} \\ \\ \equiv \{ \textnormal{ Definición de wp para } := \; \} \\ \\ E = (\langle \; \forall i : 0 \leq i \leq 0 : \; \langle \; \sum j : 0 \leq j < pos : A.j \; \bigr \rangle \geq 0 \; \bigr \rangle \; \underline{\land \; 0 \leq 0 \leq N}) \land F = (\langle \; \sum j : 0 \leq j < 0 : A.j \; \bigr \rangle) \\ \\ \equiv \{ \textnormal{ Hipótesis de } P, \textnormal{ elemento neutro de } \land \; \} \\ \\ E = \langle \; \forall i : \underline{0 \leq i \leq 0} : \; \langle \; \sum j : 0 \leq j < pos : A.j \; \bigr \rangle \geq 0 \; \bigr \rangle \land F = \langle \; \sum j : 0 \leq j < 0 : A.j \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Lógica } \} \\ \\ E = \langle \; \forall i : \underline{i = 0} : \; \langle \; \sum j : 0 \leq j < pos : A.j \; \bigr \rangle \geq 0 \; \bigr \rangle \land F = \langle \; \sum j : 0 \leq j < 0 : A.j \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Rango unitario } \} \\ \\ E = \langle \; \sum j : \underline{0 \leq j < pos} : A.j \; \bigr \rangle \geq 0 \land F = \langle \; \sum j : \underline{0 \leq j < 0} : A.j \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Aritmética } \} \\ \\ E = \langle \; \sum j : \underline{False} : A.j \; \bigr \rangle \geq 0 \land F = \langle \; \sum j : \underline{False} : A.j \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Rango vacío } \} \\ \\ E = \underline{0 \geq 0} \land F = 0 \\ \\ \equiv \{ \textnormal{ Lógica } \} \\ \\ \underline{E = True} \land \underline{F = 0} \\ \\ \equiv \{ \textnormal{ Elijo } E = True, F = 0 \; \} \\ \\ True \end{array}

Por lo tanto, $S_1: pos, \; res, \; s := 0, \; True, \; 0$ . Derivamos $S_2$ probando con $pos, \; res, \; s := pos + 1, \; E, \; F$ aumentamos la posición a indexar:

\begin{array}{ll} P \implies wp.(pos, \; res, \; s := pos + 1, \; E, \; F).I' \\ \; \\ \underline{wp.(pos, \; res, \; s := pos + 1, \; E, \; F).I'} \\ \\ \equiv \{ \textnormal{ Definición de wp para } := \; \} \\ \\ E = (\langle \; \forall i : 0 \leq i \leq pos + 1 : \; \langle \; \sum j : 0 \leq j < pos + 1 : A.j \; \bigr \rangle \geq 0 \; \bigr \rangle \\ \underline{\land \; 0 \leq pos + 1 \leq N}) \land F = \langle \; \sum j : 0 \leq j < pos + 1 : A.j \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Validez por hipótesis } 0 \leq pos \land pos < N, \textnormal{ elemento neutro de } \land \; \} \\ \\ E = \langle \; \forall i : \underline{0 \leq i \leq pos + 1} : \; \langle \; \sum j : 0 \leq j < pos + 1 : A.j \; \bigr \rangle \geq 0 \; \bigr \rangle \land F = \langle \; \sum j : \underline{0 \leq j < pos + 1} : A.j \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Lógica } \} \\ \\ E = \langle \; \forall i : \underline{0 \leq i \leq pos \lor i = pos} : \; \langle \; \sum j : 0 \leq j < i : A.j \; \bigr \rangle \geq 0 \; \bigr \rangle \; \land \\ F = \langle \; \sum j : \underline{0 \leq j < pos \lor i = pos} : A.j \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Partición de rango, rango unitario } \} \\ \\ E = (\underline{\langle \; \forall i : 0 \leq i \leq pos : \; \langle \; \sum j : 0 \leq j < i : A.j \; \bigr \rangle \geq 0 \; \bigr \rangle} \land \underline{\langle \; \sum j : 0 \leq j < pos : A.j \; \bigr \rangle \geq 0}) \; \land \\ F = (\underline{\langle \; \sum j : 0 \leq j < pos : A.j \; \bigr \rangle} + \langle \; \sum j : j = pos : A.j \; \bigr \rangle) \\ \\ \equiv \{ \textnormal{ Hipótesis de } res \; \textnormal{y} \; suma \; \} \\ \\ E = (res \land suma \geq 0) \land F = (suma + \underline {\langle \; \sum j : j = pos : A.j \; \bigr \rangle}) \\ \\ \equiv \{ \textnormal{ Rango unitario } \} \\ \\ \underline{E = (res \land suma \geq 0)} \land \underline{F = (suma + A.pos)} \\ \\ \equiv \{ \textnormal{ Elijo } E = (res \land suma \geq 0), F = (suma + A.pos) \; \} \\ \\ True \end{array}

Por lo tanto, $S_2: pos, \; res, \; s := pos + 1, \; res \land suma \geq 0, \; suma + A.pos$ . Ahora podemos dar con el programa final:

\begin{aligned} &\textnormal{Const} \; N : Int, \; A : array[0,N) of Int; \\ &\textnormal{Var} \; res : Bool, \; pos, \; suma : Int; \\ &\{ \; P: \; N \geq 0 \; \} \\ &pos, \; res, \; suma := 0, \; True, \; 0; \\ &\mathbf{do} \; pos < N \rightarrow \\ &\quad pos, \; res, \; suma := pos + 1, \; res \land suma \geq 0, \; suma + A.pos; \\ &\mathbf{do}; \\ &\{ \; Q: \; res = \langle \; \forall i : 0 \leq i \leq N : \; \langle \; \sum j : 0 \leq j < i : A.j \; \bigr \rangle \geq 0 \; \bigr \rangle \; \} \end{aligned}

Dado un arreglo $A$ , derivar un programa que resuelva el problema:

\begin{aligned} &\textnormal{Const} \; N : Int, \; A : array[0,N) of Int; \\ &\textnormal{Var} \; r : Int; \\ &\{ \; P: \; N \geq 0 \; \} \\ &S; \\ &\{ \; Q: \; r = \langle \; \textnormal{N} i, \; j : 0 \leq i < j < N : A.i = A.j \; \bigr \rangle \; \} \end{aligned}

Este problema involucra un ciclo, ya que debemos recorrer el arreglo $A$ y comparar los elementos.

Podemos aplicar la técnica de reemplazo de constante por variable. Definimos una variable $n$ que sustituirá a $N$ , proponemos una invariante $I$ y nuestra guarda $B$ para el ciclo:

\begin{array}{ll} I \equiv r = \langle \; \textnormal{N} i, \; j : 0 \leq i < j < n : A.i = A.j \; \bigr \rangle \; \land \; 0 \leq n \leq N \\ B \equiv n < N \end{array}

La estructura que debemos seguir es la siguiente:

\begin{aligned} &\textnormal{Const} \; N : Int, \; A : array[0,N) of Int; \\ &\textnormal{Var} \; r : Int, \; n : Int; \\ &\{ \; P: \; N \geq 0 \; \} \\ &S_1; \\ &\{ \; I \; \} \\ &\mathbf{do} \; n < N \rightarrow \\ &\quad \{ \; I \land B \; \} \\ &\quad S_2; \\ &\quad \{ \; I \; \} \\ &\mathbf{do}; \\ &\{ \; Q: \; r = \langle \; \textnormal{N} i, \; j : 0 \leq i < j < N : A.i = A.j \; \bigr \rangle \; \} \end{aligned}

Para la inicialización $S_1$ , partimos de $n, \; r := 0, \; E$ , queremos partir del primer elemento del arreglo:

\begin{array}{ll} P \implies wp.(n, \; r := 0, \; E).I \\ \; \\ \underline{wp.(n, \; r := 0, \; E).(r = \langle \; \textnormal{N} i, \; j : 0 \leq i < j < n : A.i = A.j \; \bigr \rangle \; \land 0 \leq n \leq N)} \\ \\ \equiv \{ \textnormal{ Definición de wp para } := \; \} \\ \\ E = \langle \; \textnormal{N} i, \; j : 0 \leq i < j < 0 : A.i = A.j \; \bigr \rangle \; \; \underline{\land \; 0 \leq 0 \leq N} \\ \\ \equiv \{ \textnormal{ Hipótesis de } P, \textnormal{ elemento neutro de } \land \; \} \\ \\ E = \langle \; \textnormal{N} i, \; j : \underline{0 \leq i < j < 0} : A.i = A.j \; \bigr \rangle \; \\ \\ \equiv \{ \textnormal{ Aritmética } \} \\ \\ E = \langle \; \textnormal{N} i, \; j : \underline{False} : A.i = A.j \; \bigr \rangle \; \\ \\ \equiv \{ \textnormal{ Rango vacío } \} \\ \\ \underline{E = 0} \\ \\ \equiv \{ \textnormal{ Elijo } E = 0 \; \} \\ \\ True \end{array}

Por lo tanto, $S_1: n, \; r := 0, \; 0$ . Ahora podemos derivar $S_2$ probando con $n, \; r := n + 1, \; E$ , queremos aumentar la posición a indexar:

\begin{array}{ll} P \implies wp.(n, \; r := n + 1, \; E).I \\ \; \\ \underline{wp.(n, \; r := n + 1, \; E).(r = \langle \; \textnormal{N} i, \; j : 0 \leq i < j < n : A.i = A.j \; \bigr \rangle \; \} \land 0 \leq n \leq N)} \\ \\ \equiv \{ \textnormal{ Definición de wp para } := \; \} \\ \\ E = \langle \; \textnormal{N} i, \; j : 0 \leq i < j < n + 1 : A.i = A.j \; \bigr \rangle \; \} \; \underline{\land \; 0 \leq n + 1 \leq N} \\ \\ \equiv \{ \textnormal{ Validez por hipótesis } 0 \leq n \land n < N, \textnormal{ elemento neutro de } \land \; \} \\ \\ E = \langle \; \textnormal{N} i, \; j : \underline{0 \leq i < j < n + 1} : A.i = A.j \; \bigr \rangle \; \} \\ \\ \equiv \{ \textnormal{ Lógica } \} \\ \\ E = \langle \; \textnormal{N} i, \; j : \underline{0 \leq i < n \lor i = n} : A.i = A.j \; \bigr \rangle \; \} \\ \\ \equiv \{ \textnormal{ Partición de rango } \} \\ \\ E = \underline{\langle \; \textnormal{N} i, \; j : 0 \leq i < n : A.i = A.j \; \bigr \rangle} \; + \langle \; \textnormal{N} i, \; j : i = n : A.i = A.j \; \bigr \rangle \; \\ \\ \equiv \{ \textnormal{ Hipótesis de } r \; \} \\ \\ E = r + \underline{\langle \; \textnormal{N} i, \; j : i = n : A.i = A.j \; \bigr \rangle } \\ \\ \equiv \{ \textnormal{ Rango unitario } \} \\ \\ E = r + \langle \; \sum j : 0 \leq j < n : A.n = A.j \; \bigr \rangle \end{array}

Hemos llegado a una expresión no programable, pero podemos definir una nueva variable $s$ tal que:

s = \langle \; \sum j : 0 \leq j < n : A.n = A.j \; \bigr \rangle

Analizando la expresión, esta calcula la cantidad de veces que se repite un elemento $A.n$ en el arreglo $A$ . Necesitamos un ciclo que incremente la constante $n$ y dentro de ese mismo ciclo, otro ciclo que recorra el arreglo $A$ y compare los elementos con $A.n$ , un ciclo anidado.

Antes de eso, podemos seguir derivando el cuerpo del ciclo $S_2$ :

\begin{array}{ll} ... \\ \\ E = r + {\langle \; \sum j : 0 \leq j < n : A.n = A.j \; \bigr \rangle} \\ \\ \equiv \{ \textnormal{ Definición de } s \; \} \\ \\ \underline{E = r + s} \\ \\ \equiv \{ \textnormal{ Elijo } E = r + s \; \} \\ \\ True \end{array}

Ahora si, para este ciclo anidado podemos aplicar la técnica de reemplazo de constante por variable. Donde la constante es $n$ y la nueva variable es $m$ . Definimos una invariante $I'$ y una guarda $B'$ :

\begin{array}{ll} I' \equiv r = \langle \; \textnormal{N} i, \; j : 0 \leq i < j < m : A.i = A.j \; \bigr \rangle \; \land \; 0 \leq m \leq n \\ B' \equiv m < n \end{array}

Nuestro problema ahora mismo radica en definir el valor de $s$ mediante un ciclo anidado. Tenemos un programa similar al siguiente:

\begin{aligned} &\textnormal{Const} \; N : Int, \; A : array[0,N) of Int; \\ &\textnormal{Var} \; r : Int, \; n, \; s : Int; \\ &\{ \; P: \; N \geq 0 \; \} \\ &n, \; r := 0, \; 0; \\ &\mathbf{do} \; n < N \rightarrow \\ &\quad \{ \; I \land B \; \} \\ &\quad S_3; \\ &\quad \{ \; I' \; \} \\ &\quad \mathbf{do} \; m < n \rightarrow \\ &\quad \quad \{ \; I' \land B' \; \} \\ &\quad \quad S_4; \\ &\quad \quad \{ \; I' \; \} \\ &\quad \mathbf{do}; \\ &\quad n, \; r := n + 1, \; r + s; \\ &\mathbf{do}; \\ &\{ \; Q: \; r = \langle \; \textnormal{N} i, \; j : 0 \leq i < j < N : A.i = A.j \; \bigr \rangle \; \} \end{aligned}

Por la derivación anterior tenemos que $n, r := n + 1, r + s$ en el cuerpo de ciclo $S_2$ . Ahora nos interesa derivar la inicialización $S_3$ y el cuerpo del ciclo anidado $S_4$ .

Partimos de la inicialización $S_3$ con $m, \; s := 0, \; E$ , queremos partir del primer elemento del arreglo:

\begin{array}{ll} P \implies wp.(m, \; s := 0, \; E).I' \\ \; \\ \underline{wp.(m, \; s := 0, \; E).(r = \langle \; \textnormal{N} i, \; j : 0 \leq i < j < m : A.i = A.j \; \bigr \rangle \land 0 \leq m \leq n)} \\ \\ \equiv \{ \textnormal{ Definición de wp para } := \; \} \\ \\ E = \langle \; \textnormal{N} i, \; j : 0 \leq i < j < 0 : A.i = A.j \; \bigr \rangle \; \underline{\land \; 0 \leq 0 \leq n }\\ \\ \equiv \{ \textnormal{ Hipótesis de } P, \textnormal{ elemento neutro de } \land \; \} \\ \\ E = \langle \; \textnormal{N} i, \; j : \underline{0 \leq i < j < 0} : A.i = A.j \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Aritmética } \} \\ \\ E = \langle \; \textnormal{N} i, \; j : \underline{False} : A.i = A.j \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Rango vacío } \} \\ \\ \underline{E = 0} \\ \\ \equiv \{ \textnormal{ Elijo } E = 0 \; \} \\ \\ True \end{array}

Por lo tanto, $S_3: m, \; s := 0, \; 0$ . Ahora podemos derivar $S_4$ probando con $m, \; s := m + 1, \; E$ , queremos aumentar la posición a indexar:

\begin{array}{ll} P \implies wp.(m, \; s := m + 1, \; E).I' \\ \; \\ \underline{wp.(m, \; s := m + 1, \; E).(r = \langle \; \textnormal{N} i, \; j : 0 \leq i < j < m : A.i = A.j \; \bigr \rangle \land 0 \leq m \leq n)} \\ \\ \equiv \{ \textnormal{ Definición de wp para } := \; \} \\ \\ E = \langle \; \textnormal{N} i, \; j : 0 \leq i < j < m + 1 : A.i = A.j \; \bigr \rangle \; \underline{\land \; 0 \leq m + 1 \leq n} \\ \\ \equiv \{ \textnormal{ Validez por hipótesis } 0 \leq m \land m < n, \textnormal{ elemento neutro de } \land \; \} \\ \\ E = \langle \; \textnormal{N} i, \; j : \underline{0 \leq i < j < m + 1} : A.i = A.j \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Lógica } \} \\ \\ E = \langle \; \textnormal{N} i, \; j : \underline{0 \leq i < m \lor i = m} : A.i = A.j \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Partición de rango } \} \\ \\ E = \underline{\langle \; \textnormal{N} i, \; j : 0 \leq i < m : A.i = A.j \; \bigr \rangle} \; + \langle \; \textnormal{N} i, \; j : i = m : A.i = A.j \; \bigr \rangle \\ \\ \equiv \{ \textnormal{ Hipótesis de } s \; \} \\ \\ E = s + \underline{\langle \; \textnormal{N} i, \; j : i = m : A.i = A.j \; \bigr \rangle} \\ \\ \equiv \{ \textnormal{ Rango unitario } \} \\ \\ E = s + ( \\ A.i = A.j \rightarrow 1 \\ \Box \; A.i \not{=} A.j \rightarrow 0 \\ ) \end{array}

Hemos llegado a una expresión programable mediante el uso de bloques condicionales. Nuestro programa final sería el siguiente:

\begin{aligned} &\textnormal{Const} \; N : Int, \; A : array[0,N) of Int; \\ &\textnormal{Var} \; r : Int, \; n, \; s, \; m : Int; \\ &\{ \; P: \; N \geq 0 \; \} \\ &n, \; r := 0, \; 0; \\ &\mathbf{do} \; n < N \rightarrow \\ &\quad m, \; s := 0, \; 0; \\ &\quad \mathbf{do} \; m < n \rightarrow \\ &\quad \quad \mathbf{if} \; A.m = A.n \rightarrow \\ &\quad \quad \quad m, \; s := m + 1, \; s + 1; \\ &\quad \quad \Box \; A.m \not{=} A.n \rightarrow \\ &\quad \quad \quad m := m + 1; \\ &\quad \quad \mathbf{fi}; \\ &\quad \mathbf{do}; \\ &\quad n, \; r := n + 1, \; r + s; \\ &\mathbf{do}; \\ &\{ \; Q: \; r = \langle \; \textnormal{N} i, \; j : 0 \leq i < j < N : A.i = A.j \; \bigr \rangle \; \} \end{aligned}

Verificación (PI)

La verificación de un programa imperativo puede ser llevada a cabo mediante la Terna de Hoare o mediante la Weakest Precondition. Aplicando cualquiera de ambas, comprobamos si el programa cumple con las condiciones dadas.