Abstract

We prove a relatively simple inductive theorem 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 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 in a restriction of Hoare and Jifeng's programming language of finitary relations into the greatest solutions of fixed-point equations expressed in terms of “total finitary” relations of an adequate restriction of their language