Ejercicio de la matriz concéntrica

Primera parte: analizar el problema y dar una solución en lenguaje de Lógica.

Primero voy a explicar que es una matriz concéntrica, mostrando que los números correspondientes a un anillo deben ser todos iguales, y que esta situación se debe cumplir para todos los anillos de la matriz.

Defino que el elemento marcado corresponderá a la posición (0,0) de la matriz, o sea M[0][0]=1.

Luego, como la matriz de ejemplo es de 5x5, muestro que hace falta verificar los anillos que contienen a la posición (0,0) y a la posición (1,1). El elemento del medio, que existe sólo en las matrices de tamaño impar, no hace falta chequearlo, porque siempre será igual a si mismo.

Llamo al anillo más exterior ‘Anillo 0', al próximo más interior ‘Anillo 1' y así sucesivamente. Entonces, para ver si la matriz es concéntrica, solo basta ver con que todos los anillos desde el 0 hasta dim(M)/2 exclusive, sean válidos. O sea:

Concéntrica (M) º ("i)(0 £ i < [dim(M)/2] Þ EsAnillo(M, i))

Ahora voy a definir el comportamiento del predicado EsAnillo, que debe ser TRUE cuando todos los elementos del i-ésimo Anillo sean iguales. La forma que se me ocurrió precisa solo de cuatro comparaciones, y funciona eligiendo el elemento encuadrado, y chequeando en dirección al elemento de la esquina superior derecha, que los elementos sombreados sean igual al primero. Luego, por propiedad transitiva, quedan todos los elementos del anillo comparados contra todos.

Como se ve en las figuras (que corresponden a dos iteraciones), el predicado es:

EsAnillo (M, i) º ("j)(i < j < dim(M)-i Þ LadoVálido(M, i, j))

El predicado verifica que los lados sean iguales, iterando más o menos veces dependiendo del tamaño del anillo. El predicado LadoVálido debe chequear que los lados sean iguales al elemento de referencia, o sea:

LadoValido (M, i, j)º M[i][j] = M[dim(M)-1-i][dim(M)-1-j] Ù

M[i][j] = M[dim(M)-1-j][i] Ù

M[i][j] = M[j][dim(M)-1-i] Ù

M[i][j] = M[i][j-1]

Con lo cual nos queda definido el estado final de la función.

Segunda parte: definir los invariantes y escribir la función en lenguaje Imperativo.

Muestro el código de la función para que se vea a que variables hacen referencia los invariantes.

function Concentrica (M:arreglo de arreglo de integer):bool

var

i: integer;

b: bool;

b := True;

i := 0;

while (i < dim(M)/2) do

b := b and EsAnillo(M, i);

i := i+1;

od

return b;

endfunction

Entonces el invariante y variante, queda:

I:{ 0 £ i £ [dim(M)/2] Ù  b=("h)(0 £ h < i Þ EsAnillo(M, h)) }

Fv = [dim(M)/2] - i

Ahora se muestra el código de la función auxiliar:

function EsAnillo(M:arreglo de arreglo de integer, i:integer):bool

var

b: bool;

j: integer;

b := True;

j := i+1;

while (j < dim(M)-i) do

b := b and M[i][j] = M[dim(M)-1-i][dim(M)-1-j]

and M[i][j] = M[dim(M)-1-j][i]

and M[i][j] = M[j][dim(M)-1-i]

and M[i][j] = M[i][j-1];

j := j+1;

od

return b

endfunction

El invariante y variante de la función, son:

I:{ i < j £ dim(M)-i Ù b=("h)(i < h < j Þ LadoVálido(M, i, h)) }

Fv = dim(M) - i

Que evidentemente son fáciles de deducir en base a los estados finales de los ciclos (que equivalen al estado funal de la función).

Tercera parte: escribir los estados luego de la ejecución de las sentencias.

Se incluyen los estados antes de ejecutar el cuerpo del ciclo, para verificar que si se cumple el invariante en ese estado, se cumple luego de ejecutar el cuerpo del ciclo,

Cuarta parte: verificar la exactitud de los estados, según el invariante.

Función Concéntrica:

El invariante es:

I: { 0 £ i £ [dim(M)/2] Ù  b=("h)(0 £ h < i Þ EsAnillo(M, h)) }

Aquí habría que ir reemplazando en el invariante y demostrando.

Eac: { b=True Ù i=0 }

{ 0 £ 0 £ [dim(M)/2] Ù  True=("h)(0 £ h < 0 Þ EsAnillo(M, h)) }

{ True Ù  True=True }

{ True }

Ef (vemos ¬B Ù I): { b=Concentrica(M0) }

 { 0 £ i £ [dim(M)/2] Ù  ¬(i < [dim(M)/2]) Ù

b=("h)(0 £ h < i Þ EsAnillo(M, h)) }

{ 0 £  i Ù i=[dim(M)/2] Ù

b=("h)(0 £ h < [dim(M)/2] Þ EsAnillo(M, h)) }

{ True Ù b=("h)(0 £ h < [dim(M)/2] Þ EsAnillo(M, h))}

{ True }

I en E1 e I en E2:

I en E1:

{0 £ I0 £ [dim(M)/2] Ù  B0=("h)(0 £ h < I0 Þ EsAnillo(M,h))}

I En E2 (reemplazo el B0 de E1):

{ 0 £ I0+1 £ [dim(M)/2] Ù  

(("h)(0 £ h < I0 Þ EsAnillo(M, h)) Ù EsAnillo(M0,I0+1))=("h)(0 £

h < I0+1 Þ EsAnillo(M, h)) }

{0 £ I0+1 £ [dim(M)/2] Ù  True } Juntando lo marcado

{ I0 < [dim(M)/2] }

   { True } por el estado inicial.

Función EsAnillo:

El invariante es:

I:{ i < j £ dim(M)-i Ù b=("h)(i < h < j Þ LadoVálido(M, i, h)) }

Eac:

{I0 <  I0+1 £ dim(M)-I0 Ù

True=("h)(I0 < h < I0+1 Þ  LadoVálido(M,i,j))}

{ 0 < 1 £ dim(M)-2*I0 Ù True=True }

{ 2*I0 < dim(M) }

{ I0 < dim(M)/2 }

{ True }

Por que el estado inicial dice que I0 < [dim(M)/2] y la parte entera de un número es menor o igual a ese número.

Ef (vemos ¬B Ù I):

{ I0 < j £ dim(M)-I0 Ù ¬(j < dim(M)-I0)

b=("h)(I0 < h < j Þ LadoVálido(M, I0, j)) } queda j = dim(M)-I0

{I0 < dim(M)-I0 Ù b=("h)(I0 < h < dim(M)-I0 Þ LadoVálido(M,I0,h))}

{ 2*I0 < dim(M) Ù b=("h)(I0 < h < dim(M)-I0 Þ LadoVálido(M,I0,h))}

{ I0 < dim(M)/2 Ù b=EsAnillo(M,I0,h)} lo primero True por Ei

I en E1 e I en E2:

En E1:

{I0 < J0 £ dim(M)-I0 Ù B0=("h)(I0 < h < J0 Þ LadoVálido(M,I0,h))}

En E2 (reemplazo el B0 de E1):

{ I0 < J0+1 £ dim(M)-I0

Ù ("h)(I0 < h < J0+1 Þ LadoVálido(M,I0,h)) = ("h)(I0 < h < J0 Þ

LadoVálido(M,I0,h)) Ù LadoVálido(M,I0,J0+1) }

{ I0 < J0+1 £ dim(M)-I0 Ù True}

{ I0 < J0 < dim(M)-I0 Ù True}

{ I0 < dim(M)-I0 Ù True} por la condición de la guarda

{ True } igual álgebra que en demostraciones anteriores