Publication:

An Inductive Theorem on the Correctness of General Recursive Programs

Probamos un teorema inductivo relativamente simple (análogo al teorema de invariancia de Floyd y Dijkstra para programas iterativos) para verificar la corrección de una amplia clase de programas recursivos generales no deterministas. Este resultado se basa en la semántica relacional de Hoare y Jifeng. Al considerar la estructura de su código y especificación, proponemos condiciones de regularidad sobre el predicado transformador asociado a la ecuación de punto fijo de un programa recursivo general (no determinista) para demostrar que es correcto por inducción sobre una ordenación bien fundamentada de una cobertura del dominio de su correspondiente relación input-output. Todas las soluciones de punto fijo asociadas a un transformador predicado que satisfacen estas condiciones de regularidad coinciden cuando se restringen al dominio de su solución de punto fijo mínimo. Encontramos estas condiciones no indebidamente restrictivas, ya que los operadores continuos que definen programas deterministas como sus correspondientes soluciones de punto fijo mínimo deben cumplirlas. Presentamos programas deterministas (considerados como soluciones mínimas de ecuaciones de punto fijo) en una restricción del lenguaje de programación P de Hoare y Jifeng de relaciones finitas (parciales) en las soluciones máximas de ecuaciones de punto fijo expresadas en términos de relaciones "totales finitarias" de una restricción adecuada de su lenguaje D