Funcionamiento correcto

Generalmente se dice que un programa es correcto si dado una entrada el programa produce los resultados deseados.

Más formalmente:

Sea P(x) una propiedad de una variable x de entrada (aquí el símbolo x refleja cualquier conjunto de variables de entradas). Sea Q(x, y) una propiedad de una variable x de entrada y de una variable y de salida.

Se define dos tipos de funcionamiento correcto de un programa:

funcionamiento correcto parcial:

dado una entrada a, si P(a) es verdadero, y si se lanza el programa con la entrada a, entonces si el programa termina habrá calculado b y Q(a, b) también es verdadero.

funcionamiento correcto total:

dado una entrada a, si P(a) es verdadero, y si se lanza el programa con la entrada a, entonces el programa termina y habrá calculado b con Q(a, b) siendo también verdadero.

Un ejemplo es el cálculo de la raíz cuatrada, si x es un número flotante (por ejemplo en el estándar IEEE) queremos que un programa que calcula la raíz, lo hace correctamente para todos los números x$\ge$ 0. Para que los procesadores puedan usar una función total (que hoy día ya es parte de las instrucciones básicas de muchos procesadores), hay que incluir los casos que x es negativo; para eso el estándar usa la codificación de nan (not-a-number). Calcular la raíz de un número negativo (o de nan) resulta en nan.

Se distingue los dos casos sobre todo porque el problema si un programa, dado una entrada, se para, no es calculable. O en otras palabras, no podemos ``completar'' siempre la función por calcular.

Para un programa secuencial existe solamente un orden total de las instrucciones atómicas (en el sentido que un procesador secuencial siempre sigue el mismo orden de las instrucciones), mientras que para un programa concurrente puedan existir varios órdenes.

Por eso se tiene que exigir:

funcionamiento correcto concurrente:

un programa concurrente funciona correctamente si el resultado Q(x, y) no depende del orden de las instrucciones atómicas entre todos los órdenes posibles.

Entonces:

• Se debe asumir que los hilos pueden intercalarse en cualquier punto en cualquier momento.
• Los programas no deben estar basados en la suposición de que habrá un intercalado específico entre los hilos de parte del planificador.