A Complete Axiomatic System for Proving Deductions About Recursive Programs
Denoting a version of Hoare's system for proving partial correctness of recursive programs by H, we present an extension D which may be thought of a H u {^,v,∃,∀} uH^-1, including the rules of H, four special purpose rules and inverse rules to those of Hoare. D is shown to be a complete system...
| Main Authors: | , , |
|---|---|
| Published: |
2023
|
| Online Access: | https://hdl.handle.net/1721.1/148924 |
| _version_ | 1826206463006081024 |
|---|---|
| author | Harel, David Pnueli, Amir Stavi, Jonathan |
| author_facet | Harel, David Pnueli, Amir Stavi, Jonathan |
| author_sort | Harel, David |
| collection | MIT |
| description | Denoting a version of Hoare's system for proving partial correctness of recursive programs by H, we present an extension D which may be thought of a H u {^,v,∃,∀} uH^-1, including the rules of H, four special purpose rules and inverse rules to those of Hoare. D is shown to be a complete system (in Cook's sense) for proving deductions of the form σ1.....σn ?σ over a language, the wff's of which are assertions in some assertion language L and partial correctness specifications of the form p{α}q. All valid formulae of L are taken as axioms of D. It is shown that D is sufficient for proving partial correctness, total correctness and program equivalence as well as other important properties of programs, the proofs of which are impossibel in H. The entire presentation is worked out in the framework of nondeterministic programs employing iteration and mutually recursive procedures. |
| first_indexed | 2024-09-23T13:30:09Z |
| id | mit-1721.1/148924 |
| institution | Massachusetts Institute of Technology |
| last_indexed | 2024-09-23T13:30:09Z |
| publishDate | 2023 |
| record_format | dspace |
| spelling | mit-1721.1/1489242023-03-30T03:37:48Z A Complete Axiomatic System for Proving Deductions About Recursive Programs Harel, David Pnueli, Amir Stavi, Jonathan Denoting a version of Hoare's system for proving partial correctness of recursive programs by H, we present an extension D which may be thought of a H u {^,v,∃,∀} uH^-1, including the rules of H, four special purpose rules and inverse rules to those of Hoare. D is shown to be a complete system (in Cook's sense) for proving deductions of the form σ1.....σn ?σ over a language, the wff's of which are assertions in some assertion language L and partial correctness specifications of the form p{α}q. All valid formulae of L are taken as axioms of D. It is shown that D is sufficient for proving partial correctness, total correctness and program equivalence as well as other important properties of programs, the proofs of which are impossibel in H. The entire presentation is worked out in the framework of nondeterministic programs employing iteration and mutually recursive procedures. 2023-03-29T14:09:40Z 2023-03-29T14:09:40Z 1978-02 https://hdl.handle.net/1721.1/148924 4802763 MIT-LCS-TM-096 application/pdf |
| spellingShingle | Harel, David Pnueli, Amir Stavi, Jonathan A Complete Axiomatic System for Proving Deductions About Recursive Programs |
| title | A Complete Axiomatic System for Proving Deductions About Recursive Programs |
| title_full | A Complete Axiomatic System for Proving Deductions About Recursive Programs |
| title_fullStr | A Complete Axiomatic System for Proving Deductions About Recursive Programs |
| title_full_unstemmed | A Complete Axiomatic System for Proving Deductions About Recursive Programs |
| title_short | A Complete Axiomatic System for Proving Deductions About Recursive Programs |
| title_sort | complete axiomatic system for proving deductions about recursive programs |
| url | https://hdl.handle.net/1721.1/148924 |
| work_keys_str_mv | AT hareldavid acompleteaxiomaticsystemforprovingdeductionsaboutrecursiveprograms AT pnueliamir acompleteaxiomaticsystemforprovingdeductionsaboutrecursiveprograms AT stavijonathan acompleteaxiomaticsystemforprovingdeductionsaboutrecursiveprograms AT hareldavid completeaxiomaticsystemforprovingdeductionsaboutrecursiveprograms AT pnueliamir completeaxiomaticsystemforprovingdeductionsaboutrecursiveprograms AT stavijonathan completeaxiomaticsystemforprovingdeductionsaboutrecursiveprograms |