Hoare's Logic Is Not Complete When It Could Be
It is known (cf.[2]) that is the Hoare rules are complete for a first-order structure A, then the set of partial correctness assertions true over A is recursive in the first-order theory of A. We show that the converse is not true. Namely, there is a first-order structure C such that the set of part...
| Main Authors: | , , |
|---|---|
| Published: |
2023
|
| Online Access: | https://hdl.handle.net/1721.1/149036 |
| _version_ | 1826212313533775872 |
|---|---|
| author | Bergstra, J. Chielinksa, A. Tiuryn, J. |
| author_facet | Bergstra, J. Chielinksa, A. Tiuryn, J. |
| author_sort | Bergstra, J. |
| collection | MIT |
| description | It is known (cf.[2]) that is the Hoare rules are complete for a first-order structure A, then the set of partial correctness assertions true over A is recursive in the first-order theory of A. We show that the converse is not true. Namely, there is a first-order structure C such that the set of partial correctness assertions true over C is recursive in the theory of C, but the Hoare rules are not complete for C. |
| first_indexed | 2024-09-23T15:19:45Z |
| id | mit-1721.1/149036 |
| institution | Massachusetts Institute of Technology |
| last_indexed | 2024-09-23T15:19:45Z |
| publishDate | 2023 |
| record_format | dspace |
| spelling | mit-1721.1/1490362023-03-30T03:14:58Z Hoare's Logic Is Not Complete When It Could Be Bergstra, J. Chielinksa, A. Tiuryn, J. It is known (cf.[2]) that is the Hoare rules are complete for a first-order structure A, then the set of partial correctness assertions true over A is recursive in the first-order theory of A. We show that the converse is not true. Namely, there is a first-order structure C such that the set of partial correctness assertions true over C is recursive in the theory of C, but the Hoare rules are not complete for C. 2023-03-29T14:21:45Z 2023-03-29T14:21:45Z 1982-08 https://hdl.handle.net/1721.1/149036 10741982 MIT-LCS-TM-226 application/pdf |
| spellingShingle | Bergstra, J. Chielinksa, A. Tiuryn, J. Hoare's Logic Is Not Complete When It Could Be |
| title | Hoare's Logic Is Not Complete When It Could Be |
| title_full | Hoare's Logic Is Not Complete When It Could Be |
| title_fullStr | Hoare's Logic Is Not Complete When It Could Be |
| title_full_unstemmed | Hoare's Logic Is Not Complete When It Could Be |
| title_short | Hoare's Logic Is Not Complete When It Could Be |
| title_sort | hoare s logic is not complete when it could be |
| url | https://hdl.handle.net/1721.1/149036 |
| work_keys_str_mv | AT bergstraj hoareslogicisnotcompletewhenitcouldbe AT chielinksaa hoareslogicisnotcompletewhenitcouldbe AT tiurynj hoareslogicisnotcompletewhenitcouldbe |