An Inductive Theorem on the Correctness of General Recursive Programs

Abstract

We prove a relatively simple inductive theorem (analogous to Floyd and Dijkstra's Invariance Theorem for iterative programs) to verify the correctness of an ample class of non-deterministic general recursive programs. This result is based on Hoare and Jifeng's relational semantics. By considering the structure of its code and specification, we propose regularity conditions on the predicate transformer associated to the fixed-point equation of a general (non deterministic) recursive program to prove it correct by induction on a well founded ordering of a covering of the domain of its corresponding input-output relation. All fixed point solutions associated to a predicate transformer satisfying these regularity conditions coincide when restricted to the domain of its least fixed point solution. We find these conditions non unduly restrictive, since continuous operators defining deterministic programs as their corresponding least fixed-point solutions must fulfill them. We couch deterministic programs (viewed as least solutions of fixed-point equations) in a restriction of Hoare and Jifeng's P programming language of (partial) finitary relations into the greatest solutions of fixed-point equations expressed in terms of “total finitary” relations of an adequate restriction of their D language

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