Skip Navigation



Logic Journal of IGPL Advance Access published online on September 26, 2007
Logic Journal of IGPL, doi:10.1093/jigpal/jzm053
This Article
Right arrow Full Text (PDF)
Right arrow All Versions of this Article:
15/5-6/373    most recent
jzm053v1
Right arrow References
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 Alejandro Bohórquez, J.
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


  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 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.

1The 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.


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




Disclaimer:
Please note that abstracts for content published before 1996 were created through digital scanning and may therefore not exactly replicate the text of the original print issues. All efforts have been made to ensure accuracy, but the Publisher will not be held responsible for any remaining inaccuracies. If you require any further clarification, please contact our Customer Services Department.