Skip Navigation


Logic Journal of IGPL Advance Access originally published online on September 26, 2007
Logic Journal of IGPL 2007 15(5-6):373-399; doi:10.1093/jigpal/jzm053
This Article
Right arrow Abstract Freely available
Right arrow Full Text (PDF)
Right arrow Alert me when this article is cited
Right arrow Alert me if a correction is posted
Services
Right arrow Email this article to a friend
Right arrow Similar articles in this journal
Right arrow Alert me to new issues of the journal
Right arrow Add to My Personal Archive
Right arrow Download to citation manager
Right arrowRequest Permissions
Google Scholar
Right arrow Articles by Bohórquez, J. A.
Right arrow Search for Related Content
Social Bookmarking
Add to CiteULike   Add to Connotea   Add to Del.icio.us  
What's this?

© The Author, 2007. Published by Oxford University Press. All rights reserved. For Permissions, please email: journals.permissions@oxfordjournals.org

An Inductive Theorem on the Correctness of General Recursive Programs

Jaime Alejandro Bohórquez 1

Ingeniería de Sistemas, Escuela Colombiana de Ingeniería, AK 45 # 205 - 59 (Autopista Norte), Bogotá, Colombia. E-mail: jbohorqu{at}escuelaing.edu.co

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 Formula 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 Formula language

Received for publication 11 July 2006.

The author thanks Diethard Michaelis, Roland Backhouse and Jorge R. Cuellar for their help pointing bibliographical sources, and their advise and suggestions for improving the presentation of this paper.



References

  1. Dijkstra EWD. "Guarded commands, nondeterminacy and the formal derivation of programs." Comm. of the ACM (1975) 18:453–457.[CrossRef]

  2. Dijkstra EWD. "A Discipline of Programming". (1976) Prentice-Hall. Preface.

  3. Dijkstra EW, Scholten CS. "Predicate calculus and program semantics". (1990) Springer-Verlag. 220.

  4. Dijkstra RM. "Relational calculus and relational program semantics". Technical Report CS-R9408 (1994) Department of Computing Science, University of Groningen. 99.

  5. Doornbos H, Backhouse R. "Mathematics of recursive program construction". 65. draft manuscript. http://citeseer.ist.psu.edu/doornbos01mathematics.html, (Jul. 2001).

  6. Gries D, Schneider F. "A logical approach to discrete math". (1993) Springer-Verlag. 497.

  7. Gritzner TF, Berghammer R. A relation algebraic model of robust correctness. Theor. Comput. Sci (1996) 159(2):245–270.[CrossRef]

  8. Hehner E. "A Practical Theory of Programming". (2004) 2nd ed. Springer-Verlag.

  9. Hesselink WH. "Programs, Recursion and unbounded choice". In: Cambridge Tracts in Theoretical Computer science 27 (1992) Cambridge university Press. 223.

  10. Hoare CAR. "An Axiomatic Basis for Computer Programming"(Reprint). Commun. ACM (1983) 26(1):53–56.

  11. Hoare CAR, Jifeng He. "The weakest prespecification I". Fundamenta Informaticae ((Mar 1986)) 9(1):51–84.

  12. Hoare CAR, Jifeng He. "The weakest prespecification I". Fundamenta Informaticae (1986) 9:217–252.

  13. Hoare CAR, Jifeng He. The Weakest Prespecification. Inf. Process. Lett (1987) 24(2):127–132.[CrossRef]

  14. Hoare CAR, Jifeng He. "Unifying theories of programming". In: Prentice Hall Series in Computer Science (1998) Prentice Hall. 300.

  15. Nelson G. "A generalization of Dijkstra's calculus". ACM Trans. Program. Lang. Syst. (1989) 11(4):517–561.

  16. Schmidt G, Ströhlein T. "Relations and graphs: discrete mathematics for computer scientists". (1993) Springer-Verlag. 301.

  17. Tarski A. "A lattice-theoretical fixpoint theorem and its applications". Pacific J. Math. (1955) 5:285–309.

  18. Tarski A. "On the calculus of relations." J. Symbolic Logic (1941) 6:73–89.[CrossRef]


Add to CiteULike CiteULike   Add to Connotea Connotea   Add to Del.icio.us Del.icio.us    What's this?



This Article
Right arrow Abstract Freely available
Right arrow Full Text (PDF)
Right arrow Alert me when this article is cited
Right arrow Alert me if a correction is posted
Services
Right arrow Email this article to a friend
Right arrow Similar articles in this journal
Right arrow Alert me to new issues of the journal
Right arrow Add to My Personal Archive
Right arrow Download to citation manager
Right arrowRequest Permissions
Google Scholar
Right arrow Articles by Bohórquez, J. A.
Right arrow Search for Related Content
Social Bookmarking
Add to CiteULike   Add to Connotea   Add to Del.icio.us  
What's this?