Funcionamiento correcto

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

Más formal:

Sea P(x) una propriedad de una variable x de entrada (aquí el símbolo x refleja cualquier conjunto de variables de entradas). Sea Q(x, y) una propriedad 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.

Para un programa secuencial existe solamente un orden total de las instrucciones atómicas, 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.