Repaso: programación secuencial

Asumimos que tengamos solamente las operaciones aritméticas sumar y subtraer disponibles en un procesador fictívio y queremos multiplicar dos números positivos.

Un posible algoritmo sequencial que multiplica el número p con el número q produciendo el resultado r es:

Initially:  p is set to positive number
            q is set to positive number

a: set r to 0
b: loop
c:   if q equal 0 exit
d:   set r to r+p
e:   set q to q-1
f: endloop
g: ...

¿Cómo se comprueba si el algoritmo es correcto?

Primero tenemos que decir que significa correcto.

El algoritmo (secuencial) es correcto si

• una vez se llega a la instrucción g: el valor de la variable r contiene el producto de los valores de las variables p y q (se refiere a sus valores que han llegado a la instrucción a:)
• se llega a la instrucción g: en algún momento

Tenemos que saber que las instrucciones atómicas son correctas, es decir, sabemos exactamente su significado, incluyendo todos los efectos segundarios posibles.

Luego usamos el concepto de inducción para comprobar el bucle. Sean p_i, q_i, y r_i los contenidos de los registros p, q, y r, respectivamente.

La invariante cuya correción hay que comprobar con el concepto de inducción es entonces:

r_i + p_i ^. q_i = p ^. q