Tema 3.2.2
La seleccion if-then-else, se utiliza para evaluar condiciones segun el sentido que le quiera dar el programador o el usuario.
Se interpreta en dos condiciones con la condicion If-then y la parte else.
Se utiliza la if-then para indicar si la instruccion es verdadera segun la condicion que se halla instalado.
Y el else se utiliza para evaluar la instruccion si no fuese verdadera.
Dependiendo la evaluacion de cada condicion se programa que es lo que se va a hacer con cada caso sea el del if-then o el del else.
| ⇐ | Tema Anterior: 3.2.1 Secuencias |
| ⇒ | Siguiente Tema: 3.2.3 Mientras While |
| Regresar al TEMARIO: Matematicas Computacion |
REGLA DE PRUEBA DE IF THEN
Sea una instrucción IF-THEN:
{P}
IF B THEN S
{Q}
Es decir la Instrucción
a) El lado Then: Que ocurre cuando B se cumple y, se ejecuta la instrucción S terminando el estado de las variables de acuerdo con Q. Esta parte tiene como precondición dada {P & B} la cual representa el estado de las variables antes de que S se ejecute. Una vez que S se ejecuta, se tiene como postcondición a {Q}, es decir la postcondición de toda la instrucción IF-THEN. Esto significa que una condición necesaria (pero no suficiente) para que sea correcta la instrucción {P} IF THEN S {Q} es que la instrucción {P & B} S {Q} sea correcta. Esto puede verificarse, siguiendo los tres pasos de la Regla de Prueba en Reversa (RPR). El primer paso de RPR es simple, ya que Pdada es simplemente {P&B}. La obtención de la precondición derivada Pder para el lado del Then, se obtiene entonces a partir del conjunto {S,Q}. La verificación de Pdada => Pder se puede realizar entonces usando una tabla de verdad o, por resolución.
b) El lado Falso: Que ocurre cuando B no se cumple. Esta parte los programadores, por lo general, no la consideran como parte del Then, no obstante que formalmente está presente. Puesto que el lado falso de la instrucción IF-THEN, no contiene ninguna instrucción, no tenemos fragmento de código a verificar. Sin embargo se debe cumplir la fórmula P & ~B =>Q. Esto se debe a que para que el control de ejecución tome el camino de lado falso se debe haber cumplido la fórmula P y luego la fórmula ~B; de esta forma durante el camino del lado falso se debe cumplir P & ~B. Una vez que se llega al final del Then se debe cumplir la postcondición Q, de modo que la implicación de P &~B => debe ser una fórmula válida.
En resumen, de acuerdo con lo anterior un IF-THEN se verifica de la siguiente manera
PASO1: VERIFICACION DEL LADO DEL THEN.
1-A: IDENTIFICACION Pdada:
Pdada == { P & B}
1-B: DETERMINACION DE Pder.
Pder se obtiene con Q y el fragmento de código S del lado del then.
Esto se expresa en la forma:
{Q, S} |- Pder
que significa que a partir de la postcondición Q y el fragmento de código S del lado del Then se deduce (o debe deducirse) la precondición derivada Pder del lado del Then (el símbolo |- se lee se “se deduce”).
1-C: VERIFICAR SI ES VALIDO:
Pdado |- Pder
PASO 2: VERIFICACION DEL LADO ELSE.
Cuando la condición B no se cumple, no se entra al lado then, de modo que se debe verificar si es válido:
(P & ~B) → Q
EJEMPLO
Verificar si el siguiente fragmento de código es correcto:
P = = { X = X’}
IF X < 0 then X = -X
Q= = { (X’ < 0 => X = - X’) & (X’ >= 0 => X = X’) }
SOLUCION
PASO 1:PRUEBA P1(VERIFICACION DEL LADO DEL THEN)
1-A
Pdada = = {P & B}
== { (X = X’ & X <0}
1-B:
Pder = = { (X’ < 0 => X = - X’) & (X’ >= 0 => X = X’) } [X := -X]
= = { (X’ < 0 => -X = - X’) & (X’ > =0 => -X = X’) }
1-C Verificar Pdada → Pder
Construimos una tabla de verdad con 1-A y con una 1-B:
(X = X’ & X <0) => (X’ < 0 =>-X = - X’) & (X’ >= 0 => -X = X’)
V V V V F
V V V
V V
V
PASO 2: VERIFICAR P & ~B => Q
X = X’ & ~( X <0) => (X’ < 0 => X = - X’) & (X’ >= 0 => X = X’)
V V F
V F V V V
V V V
V V
V
En consecuencia, este programa es correcto.
REGLA DE PRUEBA DE IF THEN ELSE
Dada una instrucción if-then-else, de la forma:
{P}
IF B THEN
S1
ELSE
S2
{Q}
Para verificar esta instrucción se deben realizar dos pruebas:
PASO1: VERIFICAR
{P & B } S1 {Q}
PASO 2: VERIFICAR
{P & ~B} S2 {Q}
EJEMPLO
{TRUE}
IF X>= Y THEN MAX := X ELSE MAX:= Y
{X >=Y & MAX = X) OR (X<Y & MAX = Y)
SOLUCION
PRUEBA 1:
Se debe probar si el siguiente programa es correcto:
{TRUE & X>= Y } MAX := X {X >= Y & MAX = X) OR (X<Y & MAX = Y)
donde:
Pdada =={ X>=Y}
y Pder se obtiene reemplazando X en lugar de MAX en la postcondición, es decir:
Pder = = {{X >= Y & X= X) OR (X<Y & X = Y)}
Ahora verificamos si Pdada => Pder es una fórmula válida. Para ello usamos la tabla de verdad:
[X>= Y ] => {X >= Y & X= X) OR (X<Y & X = Y}
V V V F
V V F
V V
V
En consecuencia el programa es correcto.
DETERMINACION DE UNA PRECONDICION DE UN IF-THEN-ELSE
Dada una instrucción IF-THEN-ELSE para la cual no contamos con su precondición:
{?} IF B THEN S1 ELSE S2 {Q}
La precondición se obtiene como sigue:
P= (P1 & B) OR (P2 & ~B)
Donde:
P1= precondición derivada del lado del then.
P2= precondición derivada del lado del else.
EJEMPLO:
{?} If x <0 then y := x else y := x-2 {−1 < = y < = 4}
Solución:
La precondición derivada del lado se obtiene reemplazando en la postcondición x por y para obtener P1 del lado del then, mientras que se reemplaza y por x-2 para obtener P2 del lado del else. Es decir:
P1 == {−1 < = y < = 4} [y:=x] =={−1 < = x < = 4}
P2 =={−1 < = y < = 4} [y:=x-2]
== {−1 < = x-2 < = 4}
== {1 < = x < = 6} De esta forma la precondición buscada es:
P =={−1 < = x < = 4} or {1 < = x < = 6}
EJERCICIO:
Verificar si es correcto el siguiente fragmento de programa:
3 < =
IF X <0 THEN Y := -X ELSE Y:= X
{2 < = Y < = 4}